Optim

AbstractDionysosOptimizer <: MOI.AbstractOptimizer

Shared supertype for Dionysos solvers, providing field-backed, validated handling of MOI.RawOptimizerAttribute (get/set), MOI.Silent, and MOI.SolveTimeSec.

A concrete subtype gets, for free: MOI.set/MOI.get on raw attributes (validated against the struct's fields — an unknown attribute raises MOI.UnsupportedAttribute instead of a raw setproperty! error), MOI.supports(::RawOptimizerAttribute), MOI.set(::MOI.Silent) backed by a print_level field, and MOI.get(::SolveTimeSec) backed by a solve_time_sec field. It still defines MOI.is_empty, MOI.optimize!, reset!, and any attribute with non-field semantics (which it can override — see set_field_attribute! to delegate back after validation).

Standard field-name conventions for subtypes: print_level::Int for verbosity, solve_time_sec for the last solve time.

AbstractLiftedControlOptimizer <: AbstractDionysosOptimizer

Supertype for a solver that lifts a concrete control problem onto a symbolic abstraction and delegates the synthesis to a discrete-system optimizer.

A subtype needs the fields concrete_problem, abstract_system, abstract_problem, abstract_optimizer, abstract_controller, success, print_level and abstract_problem_time_sec, and methods for:

• build_abstract_problem(concrete_problem, abstract_system) — lift the problem;
• abstract_optimizer_type(model) — the discrete optimizer to run;
• configure_abstract_optimizer!(model, abstract_optimizer) — forward extra options (optional);
• extract_results!(model, abstract_optimizer) — copy back the result sets (optional).

MOI.is_empty, MOI.get(::MOI.SolveTimeSec) and MOI.optimize! then come for free.

AbstractionControlOptimizer <: CompositeDionysosOptimizer

Template for the classical abstraction-based control pipeline: a composite optimizer holding an abstraction_solver (builds the symbolic model) and an optional control_solver (synthesizes the abstract controller), then concretizing the controller. It implements the whole MOI.optimize!/sub_solvers/ensure_sub_solvers!/is_abstraction_computed/MOI.is_empty orchestration once — including caching the abstraction across control-task switches — so each solver family only supplies its family-specific pieces.

A concrete subtype must have fields abstraction_solver, control_solver, concrete_controller, print_level, solve_time_sec, and implement:

• default_abstraction_solver: a fresh abstraction sub-solver;
• build_concrete_controller: concretize the abstract controller;
• set_concrete_problem! (the problem→sub-solver wiring, which differs per family).

Optional: configure_control_solver! to push extra attributes onto the control solver before it runs (e.g. a transition-cost closure).

CompositeDionysosOptimizer <: AbstractDionysosOptimizer

Supertype for high-level solvers that orchestrate sub-solvers (typically an abstraction solver plus a problem-specific control solver) and forward attributes to them transparently:

A raw attribute is resolved against the composite's own fields first, then against each sub-solver in the order returned by sub_solvers (skipping nothing entries); an attribute found nowhere raises MOI.UnsupportedAttribute.

Required methods: sub_solvers and set_concrete_problem!. Optional: ensure_sub_solvers! for lazy sub-solver creation.

The discrete-system optimizer type an AbstractLiftedControlOptimizer delegates to.

build_abstract_problem(concrete_problem, abstract_system) -> Problem.ProblemType

Lift a concrete control problem onto abstract_system. One method per (problem, abstraction) pair, defined next to the optimizer that runs it.

build_concrete_controller(model::AbstractionControlOptimizer, abstract_system, abstract_controller)

Concretize the synthesized abstract_controller into a controller on the original system. The hook may read additional results from model.control_solver / model.abstraction_solver.

Forward the options only this problem understands to the discrete optimizer. Optional.

configure_control_solver!(model::AbstractionControlOptimizer, control_solver, abstract_system)

Push extra attributes onto control_solver after the abstract system is attached but before it runs (default: no-op). Used e.g. by the ellipsoid family to forward a transition-cost closure.

default_abstraction_solver(model::AbstractionControlOptimizer)

Return a fresh abstraction sub-solver for model's family (called lazily by ensure_sub_solvers!).

ensure_sub_solvers!(model::CompositeDionysosOptimizer)

Hook called before any MOI.set on the composite; lazily instantiate sub-solvers whose settable attributes must be reachable before a problem is attached (e.g. the abstraction solver holding state_grid/time_step). Default: do nothing.

Copy the result sets only this problem produces back off the discrete optimizer. Optional.

get_field_attribute(model, attr::MOI.RawOptimizerAttribute)

Field-backed implementation of MOI.get for raw attributes: validates that Symbol(attr.name) is a field of typeof(model) (raising MOI.UnsupportedAttribute otherwise) and returns it.

is_abstraction_computed(model::AbstractionControlOptimizer)

Whether the abstraction has already been built (so switching the control task reuses it).

set_concrete_problem!(model::CompositeDionysosOptimizer, problem)

Attach a concrete problem specification to the composite, selecting the matching sub-solver by dispatch on the problem type — this is where MOI.set(model, RawOptimizerAttribute("concrete_problem"), p) lands. Each solver family adds one method per ProblemType it supports; an unsupported problem type errors.

set_field_attribute!(model, attr::MOI.RawOptimizerAttribute, value)

Field-backed implementation of MOI.set for raw attributes: validates that Symbol(attr.name) is a field of typeof(model) (raising MOI.UnsupportedAttribute otherwise) and assigns it. Leaf solvers that override MOI.set for extra validation (e.g. checking a problem type) should delegate here after their checks.

solver_success(control_solver) -> Bool

Whether a control sub-solver reports having covered the initial set. Solvers that report nothing are taken to have succeeded — there is no evidence otherwise.

sub_solvers(model::CompositeDionysosOptimizer)

Return the ordered tuple of sub-solvers that raw attributes are forwarded to. Entries may be nothing (not yet instantiated); they are skipped. Earlier entries take precedence on name clashes.

MOI.get(model::AbstractionControlOptimizer, ::MOI.TerminationStatus)

Abstraction-based synthesis reported through the standard MOI attribute.

Failure is LOCALLY_INFEASIBLE, never INFEASIBLE: the abstraction is sound but not complete, so "no controller was found" is a statement about this abstraction — a finer grid, a smaller time step or another approx_mode may still succeed. INFEASIBLE would assert something the method cannot prove.

A model with no control objective (an AlternatingSimulationProblem) is OPTIMAL once its abstraction is built: building it is the task.

AbstractCostTerm

One term of a rollout cost, evaluated ONLINE by the accumulator protocol:

• cost_init(term) — the term's initial accumulator (any value);
• cost_step(term, acc, x, u, k) — fold step k (1-based); x is the state BEFORE u is applied; returns the updated accumulator;
• cost_final(term, acc, xT) — fold the terminal state and return the term's scalar cost (a Real — terms whose accumulator is not already the cost MUST implement this).

Terms are summed by CompositeCost.

CompositeCost(terms...)

Sum of AbstractCostTerms, evaluated online during rollouts.

DomainPenaltyCost(X; w = 1000.0, wrap = identity)

Stage penalty w per state outside the domain X (wrap maps periodic states into the fundamental domain first). Every state of the rollout is charged — including the terminal one — so leaving the domain early is never cheap.

InputEffortCost(w = 1.0)

Stage cost w·Σₖ ‖uₖ‖².

InputSmoothnessCost(w_du = 1.0, w_ddu = 0.0)

Stage cost on input increments: w_du·‖Δuₖ‖² + w_ddu·‖Δ²uₖ‖². Smooth inputs are what the certifier's linearization boxes can absorb (plan.md §3.2-M2).

ReachObjectiveCost(target_set; w_distance = 100.0, hit_bonus = 1000.0, wrap = identity)

Reach shaping: w_distance · min_k dist(xₖ, target centers) minus hit_bonus / k for the first state inside the target (earlier hits earn more). Distances are to the centers of the target's members — a cheap online surrogate.

TerminalEllipsoidCost(E; w_outside = 1e6, w_center = 1e5)

Terminal cost pulling the endpoint into the ellipsoid E (typically the certifier's terminal ellipsoid): with d² = (x−c)ᵀP(x−c), w_outside·max(0, d²−1)² + w_center·d².

TerminalPullCost(center, radii; w = 1.0, wrap = identity, periods = nothing)

Endpoint pull in a scaled metric: w · Σᵢ (dᵢ / radiiᵢ)² with dᵢ = xT,ᵢ − centerᵢ taken modulo periods[i] when given (nearest-period difference — the wrap-aware pull that keeps a periodic endpoint engaged with a target straddling the seam). The reach shaping scores a trajectory's CLOSEST pass; this term is what drives the ENDPOINT to the target center, which is what lets a large box-centered terminal ellipsoid be inscribed (measured on the pendulum swing-up).

TrackingCost(reference, weights)

Stage cost Σₖ Σᵢ weights[i]·(x[i] − reference[k][i])² against a reference state sequence (hoisted once — never re-collected per sample). Steps beyond the reference length track its last state.

get_diagnostics(gen::AbstractTrajectoryGenerator)

Generator-specific diagnostics of the last generate! run, or nothing.

get_result(cert::AbstractTrajectoryCertifier)

The certifier's last result object (certifier-specific type), or nothing before certify!. Part of the certifier interface — the bidirectional handoff and the re-planning loop consume it generically.

get_seed(gen::AbstractTrajectoryGenerator)

The generator's current seed trajectory, or nothing.

set_horizon!(gen::AbstractTrajectoryGenerator, nstep::Int)

Re-target the generator at an nstep-step horizon (the prefix re-planning loop shortens the horizon to the failed prefix). Errors for generators without an adjustable horizon.

set_seed_trajectory!(gen::AbstractTrajectoryGenerator, traj)

Warm-start gen with a seed trajectory. Part of the generator interface so a composite (seed → refine) chain works with any refiner, not one hardcoded type.

set_stop_on_success!(gen, flag::Bool) -> Union{Nothing, Bool}

Set whether the generator stops at its first success, returning the PREVIOUS value so callers can restore it — or nothing when the generator has no such switch (the default: not every generator optimizes past success).

Optimizer{T} <: Dionysos.Optim.AbstractionControlOptimizer

A high-level abstraction-based solver that automatically orchestrates system abstraction and control synthesis. This wrapper follows the classical abstraction pipeline (e.g., as in SCOTS), where the state and input spaces are discretized into hyper-rectangular cells, independent of the specific control task.

It delegates responsibility to modular sub-solvers: one for abstraction and one for control, depending on the type of problem to be solved.

Structure and Sub-solvers

The optimizer internally manages two sub-solvers:

• abstraction_solver: OptimizerAlternatingSimulationProblem: Used to compute the symbolic abstraction of the system from its dynamics and domain.

• control_solver: One of the following control-specific optimizers, depending on the problem type:

  • OptimizerOptimalControlProblem: for reachability/optimal control problems.
  • OptimizerSafetyProblem: for safety problems.

Behavior

• The user sets the control task via: MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem) where my_problem is a subtype of ProblemType.

• The optimizer automatically dispatches to the appropriate control solver based on the problem type.

• If the abstraction has not yet been computed, it is automatically built before solving the control problem.

• Once computed, the abstraction is cached — switching the control problem (e.g., from safety to reachability) does not recompute it.

• The field solve_time_sec tracks the runtime of the last call to MOI.optimize!.

• The resulting controller and value function are stored and can be queried from the wrapper.

User-settable and access to subsolver fields

Via MOI.set(...), the user may configure abstraction_solver and control_solver parameters. Any field accessible in the sub-solvers (abstraction or control) can be transparently accessed via:

MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), grid)
MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.UniformGridAbstraction.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("time_step"), 0.1)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("solve_time_sec"))
value_fun = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))
controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))

OptimizerAlternatingSimulationProblem{T} <: Dionysos.Optim.AbstractDionysosOptimizer

A solver responsible for constructing a symbolic abstraction of the system dynamics, independently of any control specification.

This optimizer wraps everything needed to solve an AlternatingSimulationProblem, which is used to generate a symbolic model (abstraction) of either a continuous- or discrete-time system.

The optimizer supports several abstraction modes, optional implicit mappings/state sets, periodic mappings, multithreaded computation, and distributed partition-based abstraction.

Purpose

This optimizer builds a symbolic abstraction by discretizing the state and input spaces, constructing a state/input mapping, defining a source-state domain, and computing the abstract transition relation from a system approximation.

The abstraction method is selected via the approx_mode field. Depending on the chosen mode, the optimizer constructs either an over-approximation, an under-approximation, or a simulation-based abstraction.

The resulting abstract model can then be reused by higher-level control solvers (safety, reachability, co-safe LTL, etc.).

Abstraction semantics

The constructed symbolic model distinguishes between:

• XMapping: global mapping from concrete states to abstract states.
• Xset: set of source states that are enumerated when building transitions.
• Rset: set of retained / allowed states that may appear as transition targets.
• UMapping: mapping from concrete inputs to abstract inputs.
• Uset: admissible abstract-input set.

In the standard non-distributed setting, Xset usually coincides with Rset. In distributed mode, the abstraction may be computed on local partitions of Xset, while retaining a common global Rset.

Parameters

Mandatory fields set by the user

• alternating_simulation_problem (required): An instance of AlternatingSimulationProblem containing the system to abstract and the target abstraction region.

• State discretization (required):

  • either state_grid
  • or h, from which the state grid is built internally.

• input_grid (required, unless UMapping is set directly): The discretization grid for the input space.

Optional mapping / set fields

• abstraction_region (optional): Concrete region used to define the abstraction domain. If not provided, the optimizer uses:

  1. alternating_simulation_problem.state_set, if available,
  2. otherwise alternating_simulation_problem.system.X.

• incl_mode (optional, default = MP.INNER): Inclusion mode used when constructing mappings or state sets.

• XMapping (optional): Pre-built abstract-state mapping. If not provided, it is constructed from the state grid.

• Xset (optional): Source abstract-state set. If not provided, it is built from abstraction_region.

• Rset (optional): Retained / allowed target-state set. If not provided, it defaults to copy(Xset).

• UMapping (optional): Pre-built abstract-input mapping.

• Uset (optional): Abstract-input set. If not provided, a default admissible set is built.

Grid / implicit representation settings

• state_grid (optional): Explicit state grid used for discretization.

• h (optional): Grid spacing vector used to construct the state grid if state_grid is not provided.

• use_implicit_mapping (optional, default = false): If true, constructs an implicit state mapping instead of an explicit one.

• mapping_region (required if use_implicit_mapping = true): Hyper-rectangle used as ambient region for the implicit mapping. It must enclose abstraction_region.

• use_implicit_stateset (optional, default = false): If true, builds Xset as an implicit state set rather than an explicit set of indices.

Periodic mapping settings

• use_periodic_mapping (optional, default = false): If true, wraps the state mapping as a periodic mapping.

When enabled, the following fields are required:

• periodic_dims: indices of periodic dimensions.
• periodic_periods: period length for each periodic dimension.
• periodic_start (optional): start point for each periodic dimension. Defaults to zero if not provided.

System approximation settings

• approx_mode (optional, default = GROWTH): Abstraction technique used to build the system approximation. Supported modes:

  • USER_DEFINED: Use a custom over-approximation map. Set overapproximation_map.

  • GROWTH: Use growth-bound based approximation. Set jacobian_bound, or directly growthbound_map. ngrowthbound controls the internal growth-bound discretization parameter. With neither supplied the bound is derived from the dynamics (needs Symbolics); jacobian_bound_precision — a JacobianBoundPrecision — chooses how tight, and jacobian_bound_nsplit how finely the state space is split for REGIONWISE_BOUND.

  • LINEARIZED: Use linearization and derivative bounds. Set DF_sys, bound_DF, and bound_DDF.

  • CENTER_SIMULATION: Simulate the center of each abstract cell only.

  • RANDOM_SIMULATION: Simulate randomly sampled points in each abstract cell. Set n_samples.

Continuous-time settings

• time_step (required for continuous-time systems): Sampling step used to discretize a continuous-time approximation.

• nsystem (optional, default = 5): Number of internal substeps used during continuous-time simulation/discretization routines.

Execution settings

• execution_backend (optional, default = SY.SequentialBackend()): Execution backend used to compute the transition relation.

Supported execution backends:

• SY.SequentialBackend() Sequential computation on the current Julia process.

• SY.ThreadedBackend(progress_dt) Multithreaded computation on the current Julia process.

• SY.JuliaDistributedBackend(procs, nparts, partition_strategy, threaded_per_worker) Distributed computation over Julia worker processes.

• SY.SlurmArrayBackend(nchunks, chunk_id, outdir, partition_strategy, write_only) SLURM-array execution. Each array task computes one chunk and writes it to disk.

Logging / progress settings

• print_level (optional, default = 1): Verbosity level:

  • 0: silent
  • 1: summary information
  • 2: detailed progress output

• progress_update_interval (optional, default = Int(1e5)): Number of source-state/input pairs processed between progress updates.

• progress_dt (optional, default = 0.2): Minimum wall-clock time between progress refreshes in threaded mode.

Internally computed fields (after MOI.optimize!)

• abstract_system: The resulting symbolic abstraction, of type SymbolicModelList.

• discrete_time_system: Internally constructed discrete-time system used to generate the abstraction.

• abstraction_construction_time_sec: Total abstraction-construction time in seconds.

Approximation objects derived from approx_mode

• continuous_time_system_approximation: A ContinuousTimeSystemApproximation, built automatically if the original system is continuous.

• discrete_time_system_approximation: A DiscreteTimeSystemApproximation, used by the abstraction kernel in all cases.

Typical workflow

1. Define the concrete empty problem and discretization parameters.
2. Build or infer the state/input mappings and state sets.
3. Construct the system approximation from approx_mode.
4. Compute the abstract transition relation, either:
   • sequentially,
   • multithreaded,
   • or distributed across source-state partitions.
5. Store the resulting symbolic abstraction in abstract_system.

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerAlternatingSimulationProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("alternating_simulation_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("time_step"), 0.1)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)
MOI.set(optimizer, MOI.RawOptimizerAttribute("approx_mode"), GROWTH)
MOI.set(optimizer, MOI.RawOptimizerAttribute("jacobian_bound"), my_jacobian_bound)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstraction_construction_time_sec"))
abstract_system = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_system"))
discrete_time_system = MOI.get(optimizer, MOI.RawOptimizerAttribute("discrete_time_system"))

OptimizerCoSafeLTLProblem{T} <: AbstractLiftedControlOptimizer

Abstraction-based solver for co-safe LTL control problems.

This optimizer:

1. lifts a concrete CoSafeLTLProblem to an abstract automaton problem,
2. calls the generic automaton-level co-safe LTL optimizer in SY,
3. stores the resulting abstract controller and solve status.

OptimizerOptimalControlProblem{T} <: AbstractLiftedControlOptimizer

An optimizer that solves reachability or reach-avoid optimal control problems using symbolic abstractions of the system.

This solver takes as input a concrete problem (typically an instance of OptimalControlProblem) and a symbolic abstraction of the system (i.e., an abstract_system). It then solves the abstract version of the control problem.

Key Behavior

• Lifts the concrete problem to the symbolic abstraction space (abstract_system) and constructs the corresponding abstract_problem.
• Computes the controllable_set — the largest set of abstract states from which reachability can be guaranteed.
• Synthesizes an abstract_controller that brings the system to the target set under worst-case dynamics.
• Computes the abstract_value_function that maps each state (cell) to the worst-case number of steps needed to reach the target.
• The solver is successful if the field success is true after MOI.optimize!.

Parameters

Mandatory fields set by the user

• concrete_problem (required): An instance of OptimalControlProblem that defines the reach-avoid task (system, initial set, target, costs, horizon).

• abstract_system (required): The symbolic abstraction of the system, usually obtained from an abstraction optimizer such as OptimizerAlternatingSimulationProblem.

Optional user-tunable parameters

• early_stop (optional, default = false): If true, the fixpoint algorithm stops early when the initial set is fully contained in the controllable set. If false, it computes the entire maximal controllable set.

• sparse_input (optional, default = false): If true, uses a sparse representation of the transition table, reducing memory usage when the number of inputs is large but only few are admissible per state (e.g., in determinized abstractions, with new_input = (input, target)).

• print_level (optional, default = 1): Controls verbosity:

  • 0: silent
  • 1: default
  • 2: detailed logging

Internally computed fields

These fields are generated automatically during MOI.optimize!.

• abstract_problem: The lifted version of the concrete problem over the abstract system.
• abstract_problem_time_sec: Time taken to solve the abstract problem.
• abstract_controller: A controller mapping abstract states to control inputs.
• controllable_set: Set of abstract states from which the target is reachable.
• uncontrollable_set: Complementary states with no admissible reachability strategy.
• value_fun_tab: Tabular value function over abstract states (e.g., cost-to-go or step count).
• abstract_value_function: Functional form of the abstract value function.
• concrete_value_function: Functional form of the value function mapped back to the original system.
• success: Boolean flag indicating whether the solver completed successfully.

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerOptimalControlProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("abstract_system"), abstract_system)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_problem_time_sec"))
controllable_set = MOI.get(optimizer, MOI.RawOptimizerAttribute("controllable_set"))
abstract_value_function = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))
concrete_value_function = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_value_function"))
concrete_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))

OptimizerReachAndStayProblem{T} <: AbstractLiftedControlOptimizer

An optimizer for solving reach-and-stay control problems over symbolic system abstractions.

This solver takes as input a ReachAndStayProblem and a symbolic abstraction of the system (e.g., a SymbolicModel), and computes a controller that drives the system into the target set and keeps it there thereafter.

Key Behavior

• Lifts the concrete reach-and-stay problem to the abstract domain and builds an abstract_problem.
• Computes the winning set, i.e., the largest set of abstract states from which the reach-and-stay specification can be enforced.
• Synthesizes an abstract_controller that guarantees the specification under worst-case transitions.
• The optimization is successful if success == true after calling MOI.optimize!.

Parameters

Mandatory fields set by the user

• concrete_problem (required): An instance of ReachAndStayProblem specifying the system, initial set, target set, safe set, and time horizon (finite or infinite).

• abstract_system (required): A symbolic abstraction of the system, typically produced by OptimizerAlternatingSimulationProblem.

Optional user-tunable parameters

• early_stop (optional, default = false): Stops the fixed-point computation as soon as all abstract initial states belong to the winning set. This may significantly reduce computation time when only the feasibility of the given initial set is of interest.

• print_level (optional, default = 1): Controls verbosity:

  • 0: silent
  • 1: default (progress information)
  • 2: verbose debug output

Internally computed fields

These fields are automatically filled in by MOI.optimize!.

• abstract_problem: The lifted reach-and-stay problem over the symbolic abstraction.
• abstract_optimizer: The discrete reach-and-stay optimizer used to solve the abstract problem.
• abstract_controller: A symbolic controller satisfying the reach-and-stay specification.
• winning_set: The maximal set of abstract states from which the specification can be enforced.
• winning_set_complement: The complement of the winning set.
• success: Boolean flag indicating whether all abstract initial states belong to the winning set.
• abstract_problem_time_sec: Time taken to solve the abstract reach-and-stay problem.

OptimizerSafetyProblem{T} <: AbstractLiftedControlOptimizer

An optimizer for solving safety control problems over symbolic system abstractions.

This solver takes as input a SafetyProblem and a symbolic abstraction of the system (e.g., a SymbolicModelList), and computes a controller that ensures the system remains within a safe set over a time horizon or indefinitely.

Key Behavior

• Lifts the concrete safety problem to the abstract domain and builds an abstract_problem.
• Computes the invariant set, i.e., the largest set of abstract states from which all trajectories can be safely controlled.
• Synthesizes an abstract_controller that guarantees safety under worst-case transitions.
• The optimization is successful if success == true after calling MOI.optimize!.

Parameters

Mandatory fields set by the user

• concrete_problem (required): An instance of SafetyProblem that specifies the system, initial set, safe set, and horizon.

• abstract_system (required): A symbolic abstraction of the system, e.g., obtained from OptimizerAlternatingSimulationProblem.

Optional user-tunable parameters

• print_level (optional, default = 1): Controls verbosity:
  • 0: silent
  • 1: default (info)
  • 2: verbose debug output

Internally computed fields

These fields are automatically filled in by MOI.optimize!.

• abstract_problem: The lifted version of the safety problem in the symbolic domain.
• abstract_problem_time_sec: Time taken to solve the safety problem over the abstract system.
• abstract_controller: A controller mapping abstract states to admissible inputs that keep the system safe.
• invariant_set: The largest subset of abstract states from which safety can be maintained.
• invariant_set_complement: States from which safety cannot be guaranteed.
• success: Boolean flag indicating whether a valid invariant set and controller were found.

Example

using Dionysos,
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerSafetyProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("abstract_system"), abstract_system)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_problem_time_sec"))
invariant_set = MOI.get(optimizer, MOI.RawOptimizerAttribute("invariant_set"))
abstract_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_controller"))

control_solver_for(problem)

Return a fresh control sub-solver matching the type of the concrete problem. Supporting a new ProblemType in this solver family means adding one method here.

get_abstract_safe_set(abstract_system, concrete_safe_set)

Lift the optional safe set of a reach-avoid problem to abstract states, keeping only cells lying entirely inside it (MP.INNER) — a cell straddling the boundary contains unsafe points, so it cannot be certified safe. nothing passes through, meaning the whole domain.

lift_bounded_input_variation(abstract_system, constraint)

Express a concrete-input OPDS.BoundedInputVariation on abstract input symbols: the distance reads the symbols' concrete inputs, and the boundary inputs are quantized with SY.get_abstract_input.

Optimizer{T} <: Dionysos.Optim.AbstractionControlOptimizer

Abstraction-based solver using a uniform partition of ellipsoidal cells: it builds the ellipsoidal abstraction, synthesizes an abstract controller (forwarding the transition-cost closure), and concretizes it into a RefinedStaticController. Follows the shared AbstractionControlOptimizer pipeline.

control_solver_for(problem)

Return a fresh control sub-solver matching the type of the concrete problem. Supporting a new ProblemType in this solver family means adding one method here.

Optimizer{T} <: Dionysos.Optim.AbstractDionysosOptimizer

Abstraction-based solver using a lazy abstraction method with ellipsoidal cells (RRT-based).

Optimizer{T} <: Dionysos.Optim.AbstractionControlOptimizer

Abstraction-based solver for timed hybrid systems: it builds the HybridSymbolicModel abstraction, solves the abstract control problem, and concretizes the controller into a HybridQuantizedStaticController. Follows the shared AbstractionControlOptimizer pipeline.

OptimizerOptimalControlProblem{T} <: Dionysos.Optim.AbstractLiftedControlOptimizer

Reach(-avoid) sub-solver of the hybrid family: lifts an OptimalControlProblem over a hybrid system onto the HybridSymbolicModel abstraction and solves it with the discrete OptimizerOptimalControlProblem.

A transition cost given over concrete augmented states is translated by get_abstract_transition_cost; mode switches reach it as their switching label.

Set "concrete_problem" and "abstract_system"; read back "abstract_controller", "controllable_set", "uncontrollable_set" and "abstract_value_function".

OptimizerReachAndStayProblem{T} <: Dionysos.Optim.AbstractLiftedControlOptimizer

Reach-and-stay sub-solver of the hybrid family: lifts a ReachAndStayProblem over a hybrid system onto the HybridSymbolicModel abstraction and solves it with the discrete OptimizerReachAndStayProblem.

Both the target and the safe set are mode-indexed (HybridSpec), so "settle in the target" may mean a different region in each mode. stay_on_first_entry carries through from the concrete problem and picks which reading of and stay is enforced.

Set "concrete_problem" and "abstract_system"; read back "abstract_controller", "winning_set" and "winning_set_complement".

OptimizerSafetyProblem{T} <: Dionysos.Optim.AbstractLiftedControlOptimizer

Safety sub-solver of the hybrid family: lifts a SafetyProblem over a hybrid system onto the HybridSymbolicModel abstraction and computes the maximal controlled-invariant set on it.

The safe set is mode-indexed (HybridSpec); a mode the specification says nothing about is bounded by its own state set rather than forbidden.

Set "concrete_problem" and "abstract_system"; read back "abstract_controller", "invariant_set" and "invariant_set_complement".

build_dynamical_symbolic_model(system; optimizer_factory, optimizer, optimizer_kwargs)

Abstract a single mode's spatial dynamics via the uniform-grid abstraction optimizer, returning its SymbolicModel. An explicit optimizer or an optimizer_factory may be supplied; otherwise a default optimizer is used.

build_mode_symbolic_models(hs, optimizer_list, optimizer_kwargs_dict; shared_abstraction = nothing)

Build one symbolic model per mode of hs: abstract the physical dynamics, then lift it with the mode's clock (SY.ClockLift), one optimizer configuration per mode.

Several modes often share one dynamics — the same plant seen under different guards, or the two stance phases of a walking robot. Abstracting each of them is the dominant cost, so a mode may reuse another's abstraction:

• shared_abstraction[i] = j (with j < i) declares that mode i is abstracted by mode j's model. The two modes must agree on what is checkable — state set, input set, dimensions and optimizer configuration; that their dynamics agree is the caller's assertion, since two closures cannot be compared.
• shared_abstraction[i] = nothing (the default) builds mode i, unless an earlier mode was built from the very same system object with an equal configuration, in which case its abstraction is reused automatically.

Only the abstraction is shared: each mode still gets its own clock lift.

parallel_modes abstracts the modes that must actually be built on separate threads. Abstracting a mode dominates the wall clock of a hybrid build — the composition and the synthesis that follow are comparatively free — and the modes are independent, so this is close to a linear speed-up in the number of distinct modes. It is opt-in: a mode's own optimizer may itself use one of the threaded build backends in Symbolic, and nesting the two oversubscribes the machine rather than going faster.

build_timed_hybrid_symbolic_model(hs, optimizer_list, optimizer_kwargs_dict)

Top-level entry point: abstract and clock-lift every mode, then compose them into a SY.HybridSymbolicModel via a SY.ModeLift.

channelled_trajectory(aug_x_traj, u_traj) -> Dionysos.System.Trajectory

Decompose a hybrid closed-loop result — the (aug_x_traj, u_traj) pair returned by get_closed_loop_trajectory, whose augmented states are (x[, t], mode) — into a channelled Trajectory with states = the continuous state, inputs = the applied inputs, modes = the active mode, and (for clock-lifted modes) times = the clock value. This is the self-describing form consumed by Dionysos.animate_trajectory_dashboard.

control_solver_for(problem)

Return a fresh control sub-solver matching the type of the concrete problem. Supporting a new ProblemType in this solver family means adding one method here.

get_abstract_transition_cost(abstract_system, concrete_transition_cost)

Lift a transition cost written over concrete augmented states onto the abstraction, or nothing if the problem carries no cost.

The returned closure is called by the discrete solver with (abstract_state, abstract_input) and concretizes both before delegating: a continuous input becomes the input of the state's own mode, while a mode switch becomes its switching label, so cost((x, mode), "SWITCH 1 -> 2") is how a model prices changing mode.

get_closed_loop_trajectory(hs::HybridSystem, controller, tsteps, aug_state_0, nstep; stopping = x -> false)

Simulate the hybrid closed loop for at most nstep steps and return the raw (aug_x_traj, u_traj) pair, where each augmented state is (x[, t], mode). It reuses the generic System.get_closed_loop_trajectory engine; pass the result to channelled_trajectory to obtain a channelled Trajectory.

reached(problem, aug_state) -> Bool

Whether the augmented state (x[, t], mode) has arrived in problem's target. Both reach and reach-and-stay ask the same question of the same field, so they share the method.

gamma_cover_set(piece::PCLF.PolyhedralPiece, X::LazySets.HPolytope)

Return the smallest τ such that

X ⊆ P_piece(τ)

for

P_piece(τ) = {x : -τ w <= Gx <= τ w}.

GaussianMPPINoise(σ)

Zero-mean diagonal Gaussian exploration noise with per-dimension standard deviations σ (an SVector keeps the sampling loop allocation-free). Enables the importance-sampling cross term (α < 1) and σ-annealing (anneal).

AdaptiveLinearizationBoxOptions(; kwargs...)

Options of the adaptive linearization-box search (backward direction only): grow the box on :lmi_infeasible, grow to the required radii on :inconsistent_box, then select among box scales according to objective.

• enabled — turn the adaptive search on (false = fixed-box mode using ChainOptions.linearization_δx/δu);
• ΔX_initial/ΔX_min/ΔX_max, ΔU_initial/ΔU_min/ΔU_max — per-axis state/input box radii: the starting box and its clamp bounds (required);
• growth — multiplicative box growth on :lmi_infeasible;
• safety — inflation factor over the required radii on :inconsistent_box;
• max_iters — cap on adaptive iterations per step;
• atol — box-consistency tolerance;
• search_scales — box scales tried around the first consistent box (:max_volume only);
• objective — :first_consistent (accept the first consistent box — cheapest) or :max_volume (re-solve on every search_scales entry and keep the largest certified ellipsoid — ~length(search_scales)× the SDPs per step).

BackwardCertifier(affine_provider, backend, options::ChainOptions)

Ellipsoidal backward trajectory certifier: chains one ST.solve_transition_backward SDP per transition, from the terminal ellipsoid back to the trajectory start, gating every step for soundness (see ChainOptions).

CertificationResult

Outcome of a certification chain.

• success — every step certified and every enabled gate passed (including terminal containment when checked);
• failed_k — first failing step index, or nothing. Backward chains fail AT step failed_k (states failed_k+1..K+1 stay certified — see FunnelData); forward chains fail at step failed_k with states 1..failed_k certified; failed_k == K + 1 is a complete chain whose terminal gate failed;
• steps — forward-ordered StepRecords;
• controller — the per-step affine controllers κ_1..κ_K on success, else nothing;
• terminal_contained — whether the terminal ellipsoid lies inside the problem's target set (nothing when the check is disabled);
• initial_coverage — max of (v − c₁)ᵀP₁(v − c₁) over the initial set's vertices (≤ 1 means the entry funnel covers the initial set; nothing if unavailable);
• state_domain_checked — whether the reach-avoid gate could run on this domain type;
• lmi_data — the FunnelData.

ChainOptions(; kwargs...)

Options of the ellipsoidal certification chain.

• maxδx, maxδu — caps on the synthesized state/input deviations (passed to ST.solve_transition_backward);
• λ — cost-vs-volume trade-off of the backward SDP objective (min λ·J − (1−λ)·volume); the default 0.01 is volume-dominated — λ = 1.0 would remove the volume incentive entirely and let funnels collapse;
• terminal_shape — LazySets shape matrix Q of the terminal ellipsoid, or nothing to inscribe an ellipsoid in the problem's target set around the trajectory endpoint, shrunk by terminal_shrink;
• transition_cost — PSD [x; u; 1] cost matrix or UT.QuadraticStateControlFunction (identity when nothing);
• linearization_δx/δu — fixed linearization-box radii (fixed mode);
• adaptive_boxes — AdaptiveLinearizationBoxOptions or nothing;
• objective — size term of the SDP objective: :maximin (largest smallest semi-axis — collapse-proof, the default), :logdet (true volume), or :trace;
• domain_cap — make the synthesis domain- and box-aware: cap every funnel inside the state domain AND inside the current linearization box by construction (per-step SOC slabs, source_cap of ST.solve_transition_backward). Without it a size-maximizing objective grows funnels past X (state-domain gate rejects a posteriori) or past the box (state-side inconsistency drives the adaptive search into ever-bigger boxes whose Hessian bounds kill the LMI); with it, box scales become a clean line-search dial for the largest certifiable funnel.

Soundness gates (plan.md §4.2):

• r_min — minimum admissible semi-axis of every funnel ellipsoid (collapse gate; 0 disables);
• check_state_domain — require every funnel ellipsoid inside the system domain X and provably disjoint from its holes (reach-avoid gate);
• check_terminal — require the terminal ellipsoid inside the problem's target set.

ForwardCertifier(affine_provider, backend, options::ForwardOptions)

Ellipsoidal forward trajectory certifier: propagates a certified tube from the entry ellipsoid along the nominal trajectory (see ForwardOptions). Success requires every step certified, every enabled gate passed, and — when check_terminal — the final tube inside the problem's target set. The result reports the per-step contraction profile.

ForwardOptions(; kwargs...)

Options of the forward certification chain.

• target_mode — :free (target shape Q₂ is a decision variable, trace objective, conditioning sandwich q_min/q_max) or :fixed (shape follows the entry ellipsoid's, only the scale α is free — its per-step value is the contraction profile);
• α_max — fail-fast guard: a step whose tube scale — tr(Q_{k+1})/tr(Q₁), relative to the ENTRY shape in both target modes — exceeds this is rejected (Inf disables);
• entry_shape — LazySets shape matrix of the entry ellipsoid E₁, or nothing to circumscribe the problem's initial set (centered at the trajectory start);
• maxδu, λ, transition_cost, linearization_δu as in ChainOptions. The two target modes want OPPOSITE λ regimes (measured on a linear system): in :fixed mode α is dimensionless, and λ ≪ 1 polishes the min-α solution onto the strict-PSD boundary where the solver tolerance eats the ε margin and the a-posteriori validation rejects a "solved" step — use λ ≈ 0.5; in :free mode the trace term is in absolute tube units, and a large λ lets the cost term buy input effort by drifting the tube off the nominal until input feasibility dies — keep λ small (the 0.01 default) and instead set q_min near the entry scale, since at the loose default floor the trace objective needle-collapses the tube and the next step dies of source conditioning;
• linearization_δx_margin ≥ 1 inflates the (known) state box handed to the Hessian bound, buying u-side slack;
• remainder_model — :vertices or :ball (:john_ball is backward-only);
• gates: r_min, check_state_domain, check_terminal as in ChainOptions.

FunnelData

The (possibly partial) certified funnel of a chain, forward-ordered.

• ellipsoids — funnel ellipsoids. On SUCCESS they cover states 1..K+1. On a BACKWARD failure at failed_k they cover states failed_k+1 .. K+1 — i.e. ellipsoids[1] is the funnel at state failed_k + 1 (failed_k doubles as the index offset; bidirectional_certify! and prefix_replan_certify! rely on this). On a FORWARD failure at failed_k they cover states 1..failed_k;
• kappas — the matching controllers (|ellipsoids| = |kappas| + 1 whenever at least one step certified);
• reason — why the chain could not even start (no terminal/entry ellipsoid, endpoint gate failure), or nothing.

StepRecord

Outcome of one chain step: index k, status (:ok, :infeasible, or a gate failure), transition-cost bound, certified ellipsoid, controller kappa, and the diagnostics summary NamedTuple.

bidirectional_certify!(forward_cert::ForwardCertifier,
                       backward_cert::BackwardCertifier,
                       problem, traj)
    -> (; success, k_handoff, controller, forward_result, backward_result)

Certify traj with both directions and hand off at the first state s where the forward tube is contained in the backward funnel (UT.is_included, exact ellipsoid kernel). On success controller is the spliced ST.FunnelController; k_handoff is the 1-based state index of the handoff (nothing on failure). Either chain may have failed partway — only the overlap of their certified ranges is searched.

inflation_stress(f, kappas, ellipsoids, target; alphas, n_samples, rng,
                 input_set = nothing, project_input = identity,
                 domain = nothing) -> Vector{NamedTuple}

Replay the certified feedback chain on the plant map f((x, u) -> x⁺) from samples of the entry ellipsoid ellipsoids[1] inflated by each α ∈ alphas, and report the outcome decomposed by FAILURE MODE. All arguments live in the frame the chain was certified in (pass the z-frame map and sets when the chain is normalized).

• kappas — the chain's affine feedbacks, forward-ordered (length K);
• ellipsoids — the funnel ellipsoids, forward-ordered (length K + 1, ellipsoids[k] is the validity region of kappas[k]);
• target — endpoint membership set;
• alphas — inflation factors (1.0 is forced in and sampled over the full ellipsoid; each α > 1 is sampled over the shell between it and its predecessor, so the rates are per-annulus, not cumulative);
• input_set — when given, the RAW feedback output κ(x) is checked against it before project_input is applied (an input violation means the certificate's feedback demanded more authority than the plant has);
• domain — when given, every visited state is checked against it.

Returns one row per α: (; alpha, n, success_rate, certified_rate, tube_exit_rate, domain_violation_rate, input_violation_rate, target_miss_rate, first_exit_median) where success = endpoint in target with no domain or input violation, certified additionally requires never leaving the funnel chain, tube_exit counts rollouts that left their ellipsoid at some step (first_exit_median locates where), and the two violation rates split the constraint failures. At α = 1 the certificate guarantees certified_rate == 1.0 (up to solver/sampling roundoff); every α > 1 row is an empirical measurement, NOT a certificate.

prefix_replan_certify!(gen, cert, failed_result;
                       gen_problem, seed = nothing,
                       prepare = identity, backmap = identity,
                       retarget_cost! = E -> nothing,
                       margin = 5, terminal_shrink = 0.5, max_rounds = 3)

Recover a failed backward certification by re-planning its prefix.

• failed_result — the failed CertificationResult (its lmi_data holds the certified suffix, entry ellipsoid first);
• gen_problem — the generator-frame problem; the prefix problem reuses its initial set but targets the suffix entry (mapped through backmap, e.g. a de-normalization);
• seed — warm-start trajectory for the prefix (typically the failed trajectory; the generator trims it to the prefix horizon);
• prepare — generator-frame → certifier-frame trajectory transform (the same hook the driver uses);
• retarget_cost! — caller hook to re-aim the generator's shaping terms at the new (generator-frame) target ellipsoid, e.g. mutating a TerminalEllipsoidCost's arrays in place;
• margin — extra steps granted to the prefix beyond failed_k;
• terminal_shrink — the prefix chain's terminal is the entry ellipsoid scaled by this factor, centered at the prefix endpoint; the splice gate then requires it to lie inside the entry ellipsoid (UT.is_included, exact kernel).

Returns (; success, controller, k_prefix, rounds, prefix_result) — on success controller is the spliced ST.FunnelController covering the whole horizon.

print_inflation_stress(rows; io = stdout)

Print the inflation_stress rows as a fixed-width table, one line per inflation factor.

get_result(cert) -> Union{Nothing, CertificationResult}

The last CertificationResult, or nothing before certify!.

BoundedInputVariation(input_distance, max_variation; target_input = nothing, initial_input = nothing)

Input slew-rate constraint for compute_bounded_input_variation_controller: consecutive inputs must satisfy input_distance(u⁻, u) ≤ max_variation. target_input additionally constrains the last input before entering the target (e.g. the rest input, so velocities ramp down), initial_input the first one; nothing leaves them free.

At the discrete level inputs are abstract symbols (Int); the UniformGridAbstraction front-end accepts the same struct expressed on concrete inputs and lifts it with SY.get_concrete_input / SY.get_abstract_input.

OptimizerCoSafeLTLProblem{T} <: AbstractDionysosOptimizer

Co-safe LTL synthesis on a finite automaton: given a CoSafeLTLProblem whose system is an AbstractAutomatonList, build the synchronous product of the abstraction with a deterministic monitor over the atomic propositions, then run the reachability solver on that product with the monitor's accepting states as target.

The monitor is an interface, not a fixed type: any object answering step, an initial state and a set of accepting states will do. Loading Spot supplies one by translating an LTL formula.

Because the strategy depends on the monitor state and not on the abstract state alone, the returned controller is dynamic — tabulated at construction time, so it stays plain serializable data even when the monitor is a closure.

Set "problem", optionally "early_stop", "sparse_input"; read back "controller", "controllable_set" and "uncontrollable_set".

OptimizerOptimalControlProblem{T} <: AbstractDionysosOptimizer

Reach-avoid synthesis on a finite automaton: given an OptimalControlProblem whose system is an AbstractAutomatonList, compute the controllable set and a controller reaching the target without leaving the safe set.

Which algorithm runs depends on the cost: unit cost sweeps backward in breadth-first layers, a general nonnegative cost uses a priority queue. Setting "bounded_input_variation" instead routes the synthesis to compute_bounded_input_variation_controller, which constrains consecutive inputs and returns a dynamic controller.

Set "problem", optionally "early_stop", "sparse_input", "bounded_input_variation"; read back "controller", "controllable_set", "uncontrollable_set" and "value_function".

OptimizerReachAndStayProblem{T} <: AbstractDionysosOptimizer

Reach-and-stay synthesis on a finite automaton: given a ReachAndStayProblem whose system is an AbstractAutomatonList, compute the winning set and a memoryless controller.

The problem's stay_on_first_entry picks the algorithm. false is ◇□ in the literal sense and runs the nested μ/ν fixed point of Li & Liu; true forbids leaving the target once entered, and reduces to one invariance solve followed by one reachability solve.

Set "problem", optionally "early_stop"; read back "controller", "winning_set" and "winning_set_complement".

OptimizerSafetyProblem{T} <: AbstractDionysosOptimizer

Safety synthesis on a finite automaton: given a SafetyProblem whose system is an AbstractAutomatonList, compute the maximal controlled-invariant subset of the safe set.

Set "problem"; read back "controller", "invariant_set" and "invariant_set_complement". The controller keeps every surviving input at each state, not one, so downstream code is free to choose among them.

compute_bounded_input_variation_controller(
    autom::SY.AbstractAutomatonList,
    target_set,
    constraint::BoundedInputVariation;
    initial_set = SY.enum_states(autom),
    safe_set = nothing,
    cost_function = nothing,
)

Optimal reach(-avoid) controller under the input slew-rate constraint (consecutive inputs at most max_variation apart in input_distance).

Dijkstra on the pair graph: the value of (q, u) is the optimal cost-to-target from q when playing u now, subject to every later consecutive pair — and the final input, when target_input is set — being compatible. The returned controller is dynamic (memory = previously played input; closure-backed, not serializable): at q with memory u⁻ it plays the compatible input of least value.

Only deterministic automata are supported for now — the exact-lattice abstractions this constraint is designed for are deterministic by construction.

Returns (controller, controllable_set, uncontrollable_set, value_fun_tab) with value_fun_tab[q] = min_u value(q, u) (unconstrained start at q).

compute_optimal_controller(
    autom::SY.AbstractAutomatonList,
    target_set;
    initial_set = SY.enum_states(autom),
    safe_set = nothing,
    cost_function = nothing,
    sparse_input::Bool = false,
)

Implementation for compute_worst_case_cost_controller supporting any cost_function returning nonnegative values. safe_set is the optional avoid part of a reach-avoid specification; see compute_worst_case_cost_controller. If the cost function returns the same value across all x and u, consider calling the specialized function compute_worst_case_uniform_cost_controller instead.

compute_worst_case_cost_controller(
    autom::SY.AbstractAutomatonList,
    target_set;
    initial_set = SY.enum_states(autom),
    safe_set = nothing,
    cost_function = nothing,
    sparse_input::Bool = false,
)

Compute controller for optimal control problem assuming worst case for uncertainty. This means, if there are several states x⁺ that can be the next state from state x with control u, we consider the maximum cost among all those x⁺ states. If the cost_function is nothing, we interpret this as a constant cost function of 1 for each transition.

safe_set restricts the synthesis to a reach-avoid specification: only states in it may enter the controllable set. nothing means the whole state space.

This function redirects to compute_worst_case_uniform_cost_controller if the cost_function is nothing and compute_optimal_controller otherwise.

function compute_worst_case_uniform_cost_controller(
    autom::SY.AbstractAutomatonList,
    target_set;
    initial_set = SY.enum_states(autom),
    safe_set = nothing,
    sparse_input = false,
)

Implementation for compute_worst_case_uniform_cost_controller supporting for a cost function that is 1 for any state x and input u. Consider using compute_optimal_controller for a more general cost function. But for this particular case of cost, this implementation is more efficient than compute_optimal_controller as it does not rely on a PriorityQueue.

covers_initial_set(predicate, initial_set) -> Bool

Whether every abstract initial state satisfies predicate — the success criterion of a control solver.

Unlike a bare all, an empty initial_set yields false. An empty set means the specification's initial region is not represented in the abstraction at all (a degenerate grid, a region outside the abstracted domain, …), so nothing was verified; reporting success there is a vacuous truth that reaches the user as a spurious MOI.OPTIMAL.

Optimizer{T} <: Dionysos.Optim.AbstractDionysosOptimizer

Bemporad Morari solver: Optimal control of hybrid systems via a predictive control scheme using mixed integer quadratic programming (MIQP) online optimization procedures.

julia_function_to_moi(f, args::AbstractVector...)

Convert a Julia function f into a vector of MOI scalar functions by exploiting JuMP's operator overloading.

Each element of args is a vector that may contain MOI.VariableIndex (decision variables) or concrete values (e.g., Float64 for fixed parameters). The function works as follows:

1. A lightweight JuMP model is created.
2. Every MOI.VariableIndex in args is wrapped into a JuMP.VariableRef; concrete values are left unchanged.
3. f is called with the wrapped arguments. Thanks to Julia's operator overloading the arithmetic inside f builds JuMP expression trees (e.g. NonlinearExpr, AffExpr, …).
4. Each element of the result is converted back to an MOI function with JuMP.moi_function, yielding MOI.ScalarNonlinearFunction, MOI.ScalarAffineFunction, etc.

Example

f(x, u) = [x[1]^3 + u[1], x[2] + u[2]]
x = [MOI.VariableIndex(1), MOI.VariableIndex(2)]
u = [MOI.VariableIndex(3), MOI.VariableIndex(4)]
moi_exprs = julia_function_to_moi(f, x, u)
# moi_exprs is a Vector of MOI.ScalarNonlinearFunction / ScalarAffineFunction

Optimizer{T} <: Dionysos.Optim.AbstractDionysosOptimizer

Branch and bound solver: Optimal control of hybrid systems via a predictive control scheme combining a branch and bound algorithm that can refine Q-functions using Lagrangian duality.