Wrapper

Dionysos.Wrapper

The JuMP/MOI front-end: it compiles a JuMP model into a MathematicalSystems / HybridSystems object plus a Dionysos.Problem.ProblemType, then drives an existing solver with them. It owns no control semantics of its own.

The pipeline is one-directional:

JuMP model ──parse──▶ ModelIR ──lower──▶ (system, problem) ──▶ solver ──▶ controller

ModelIR is a plain, dependency-free description of what the user wrote, which is why this module lives in src/ rather than in an extension: parsing needs no Symbolics, only compiling a dynamics expression into a callable does (see AbstractDynamicsBackend).

See src/wrapper/README.md for the user guide.

AbstractDynamicsBackend

Strategy for turning the dynamics expressions of a ModelIR into a callable f(x, u). Implement compile_dynamics for a new backend.

Available:

• SymbolicADBackend — traces the expressions with Symbolics and emits a fused function; the production path, provided by DionysosMathOptSymbolicADExt.

AffineGuard

A multi-variable affine guard lower ≤ Σ aᵢ xᵢ ≤ upper, kept as raw coefficients because the state ordering is only known once roles are inferred. Lowered to one or two half-spaces.

Always(S)

Marks S as an invariant — □, the trajectory must never leave S: @constraint(model, x in Always(S)). On its own it lowers to a SafetyProblem; together with a Final set it becomes the safe_set of a reach-avoid OptimalControlProblem, read as safe U target.

This is not the same as x ∉ O: ∉ removes a region from the state space so it is never abstracted, whereas Always keeps it representable so synthesis can actively avoid it.

EventuallyAlways(S; stay_on_first_entry = false)

Marks S as a reach-and-stay target — ◇□, the trajectory must reach S and remain there: @constraint(model, x in EventuallyAlways(S)). Lowers to a ReachAndStayProblem.

stay_on_first_entry = true forbids the departures that plain ◇□ allows: the run must stay from the moment it first enters S, rather than being free to leave and return finitely often before settling. Stronger requirement, smaller winning set — see ReachAndStayProblem.

Final(S)

Marks S as a reach target — ◇, the trajectory must eventually enter S: @constraint(model, x in Final(S)). Lowers to an OptimalControlProblem.

Guard(S)

Marks S as the guard of a transition — the states from which the switch may be taken:

add_transition!(model, a => b) do t
    @constraint(t, [x, y] in Guard(LazySets.Ball2([0.0, 0.0], 1.0)))
end

S may be any bounded LazySet and must span the state vector, in declaration order. The marker is needed because JuMP has no parsing rule that would tell a bare set apart from a bound; it plays the same role as Final and Always do on a mode.

A guard can equally be written as ordinary inequalities — @constraint(t, x <= 1) per coordinate, or a multi-variable @constraint(t, x + y <= 1), which becomes a half-space. All of them intersect: a transition's guard is everything written on it, narrowed by the source mode's own state set.

Label(S; semantics = Mapping.INNER)

Name a region of the state space so a temporal formula can refer to it. The name is the constraint's own name, so no separate registration call is needed:

@constraint(model, goal,   x in Label(target))
@constraint(model, hazard, x in Label(obstacle; semantics = MP.OUTER))
@specification(model, ltl"F(goal) & G(!hazard)")

semantics says how the region is discretized: INNER keeps only cells fully inside it — the conservative reading for something you must reach — while OUTER keeps every cell touching it, the conservative reading for something you must avoid.

LabelEntry

One named region: the atomic proposition it defines, the set, how it is discretized, and the variables it is written over. name is filled in when JuMP forwards the constraint's name.

Mode

One discrete mode of a hybrid model: a scope carrying its own dynamics, its own state and input bounds, and its own specifications. Created with @mode or add_mode!.

ModeIR

One discrete mode: its own dynamics, its own bound overrides (a mode may restrict the state or input set — the thermostat's heater is off in one mode and throttled in the other), its own specifications, and its own solver options.

ModeScope

Marks a constraint as belonging to mode id.

ModelIR

Dependency-free description of a parsed JuMP model: variables and their inferred roles, the per-variable dynamics expressions, obstacles, and the objective.

Fields are populated by parse.jl as JuMP hands constraints over, then validated in one pass by infer_roles! before lowering.

NonlinearEvaluatorBackend <: AbstractDynamicsBackend

Evaluate the dynamics expressions directly with MOI.Nonlinear, needing no optional dependency at all.

This is the test and fallback path, not the production one: evaluation is interpreted and allocates on every call, and the abstraction calls it millions of times. Its purpose is to make the front-end loadable, testable and documentable without Symbolics — SymbolicADBackend is what you want for real problems.

Optimizer <: MOI.AbstractOptimizer

The JuMP entry point to Dionysos: Model(Dionysos.Optimizer).

MOI.optimize! compiles the model in four steps — infer variable roles, compile the dynamics through the AbstractDynamicsBackend, lower to a (system, problem) pair, and hand it to the solver chosen by select_solver.

Raw attributes not consumed by the wrapper itself are forwarded to that solver, so every option of the underlying optimizer is reachable with set_attribute. They are also recorded, so that choosing a different solver — explicitly through set_attribute(model, "solver", …) or by inference — replays them onto it rather than losing them.

See src/wrapper/README.md for the modelling guide.

OuterSet{S} <: MOI.AbstractVectorSet

Marks the complement of inner: @constraint(model, x ∉ O) wraps O in an OuterSet, and the lowering carves it out of the state space X.

inner may be an MOI.HyperRectangle — which can be written over a subset of the coordinates, spanning the variable bounds on the rest — or any bounded LazySet, which must span the whole state vector.

ScopedSet(inner, scope)

A scalar set tagged with the mode or transition it was written on.

ScopedVectorSet(inner, scope)

A vector set — a specification marker or an obstacle — tagged with its mode or transition.

SpecEntry

One specification set as written by the user: its temporal role, the set itself, and the variables it constrains.

SpecKind

Which temporal role a specification set plays: the initial set (START), a reach target (FINAL), an invariant (ALWAYS), or a reach-and-stay target (EVENTUALLY_ALWAYS).

Start(S)

Marks S as the initial set: @constraint(model, x in Start(S)).

S may be any bounded LazySet and must span the whole state vector. The @variable(model, x, start = v) keyword is the singleton special case.

SymbolicADBackend <: AbstractDynamicsBackend

Compile the dynamics by tracing them symbolically and building a fused Julia function with common-subexpression elimination. Requires Symbolics and MathOptSymbolicAD to be loaded; the implementation lives in DionysosMathOptSymbolicADExt.

TimeDomain

Whether the model was written with continuous-time (∂, CONTINUOUS) or discrete-time (Δ, DISCRETE) dynamics. UNKNOWN until the first dynamics constraint fixes it; mixing the two is an error.

Transition

A switch from one mode to another: a scope carrying the guard (which states enable it) and the reset map (where the state lands). Created with add_transition!.

TransitionIR

One switch: what enables it and the reset map applied when it is taken.

The enabling condition accumulates from three sources, all intersected: per-coordinate bounds (guard_lower/guard_upper), multi-variable affine constraints (affine_guards), and whole sets written with Guard (guard_sets).

TransitionScope

Marks a constraint as belonging to the transition id from mode source to mode target. The switching type rides along so a transition is fully described by any one of its constraints.

VariableInfo

Everything the front-end knows about one JuMP variable: its bounds, the initial/target intervals declared for it, its inferred VariableRole, its position within that role group, and its JuMP name (used to make error messages nameable).

VariableRole

What a declared JuMP variable turns out to be, inferred by infer_roles!:

• STATE — carries ∂/Δ dynamics;
• INPUT — appears on some dynamics right-hand side and is not a state;
• CLOCK — a state whose dynamics is exactly ∂(t) == 1 (running) or ∂(t) == 0 (frozen);
• PARAMETER — fixed and inlined rather than discretized;
• DISTURBANCE — an exogenous input, only ever set explicitly.

add_mode!(model, name = :mode) -> Mode

Declare a discrete mode. Write its dynamics, bounds and specifications on the returned scope:

off = add_mode!(model, :off)
@constraint(off, ∂(T) == -α * (T - Ta))
@constraint(off, u == 0)

@mode is the same thing with the name taken from the variable.

add_transition!(f, model, source => target; switching = AutonomousSwitching())

Declare a switch from source to target and populate it with a do-block:

add_transition!(model, off => on) do t
    @constraint(t, T <= 19)        # guard: which states enable the switch
    @constraint(t, Δ(T) == T)      # reset map (identity if omitted)
end

A constraint containing ∂/Δ is the reset map; anything else is a guard. Several transitions may share the same (source, target) pair — each is its own object, so their guards and resets never get mixed up.

A transition needs at least a guard; an always-enabled switch is written with a guard covering the whole state set.

A switch is an input the synthesis chooses. The guard says where the switch is available, not that it is taken: from a state inside the guard the abstraction offers both the switch and the mode's own dynamics, and the controller picks. So a guard is a permission, and "stay put" remains available everywhere.

Environment-forced switching — a fault, an impact, a threshold the physics obliges — is therefore not expressible today: a controller synthesized here assumes it may decline any switch. Only HybridSystems.AutonomousSwitching() is accepted, as the default placeholder value; that name is HybridSystems' and does not describe the semantics implemented here.

build_hybrid_problem(ir, backend; time_step = nothing) -> Problem.ProblemType

Assemble the hybrid control problem: a HybridSystem, an augmented initial state (x, mode), and a mode-indexed specification.

build_hybrid_system(ir, backend) -> HybridSystems.HybridSystem

Assemble the hybrid automaton: one system per mode, and one GuardedResetMap per transition.

build_problem(ir::ModelIR, backend; time_step = nothing) -> Problem.ProblemType

Lower the model, compiling its dynamics through backend. A model with modes goes to build_hybrid_problem; everything else is monolithic.

build_system(ir::ModelIR, f) -> MathematicalSystems.AbstractSystem

Assemble the concrete system: the state box X (minus the obstacles), the input box U, and the compiled dynamics f. ir.time_domain selects a continuous- or discrete-time system.

An Always set is not folded in here — it travels as the safe_set of the lowered problem, so it stays representable and the synthesis can reason about it. Only ∉ obstacles are carved out of X.

check_time_domain(ir::ModelIR)

Refuse to lower a model whose time domain is unknown.

∂ and Δ say which one a model is in. Dynamics supplied as a Julia function say nothing — f(x, u) is equally readable as a vector field ẋ = f(x, u) or as a one-step map x⁺ = f(x, u), and the two describe different plants. Guessing produced a model that lowered happily and simulated the wrong system, so the front-end asks instead.

clock_index(ir) -> Union{Nothing, Int}

The clock variable, or nothing for a time-free model.

clock_system(ir, mode, index) -> MathematicalSystems.ConstrainedLinearContinuousSystem

The clock subsystem of one mode: ẋ = 1 where the clock runs, ẋ = 0 where the mode freezes it, over the time domain given by the clock variable's bounds.

compile_dynamics(backend, ir::ModelIR, dynamics = ir.dynamics) -> f

Compile dynamics — one expression per variable, nothing for the non-states — into a callable f(x, u) returning the state derivative (continuous time) or the successor state (discrete time). x and u follow the orders given by state_indices and input_indices.

The dynamics are passed explicitly rather than read from ir, because a hybrid model compiles one function per mode, and a transition's reset map goes through the same path.

default_dynamics_backend()

The backend used when the user sets none.

describe(v::VariableInfo, i::Int) -> String

How to refer to variable i in a user-facing message: its JuMP name when JuMP gave it one, otherwise its MOI index.

detect_clock!(ir::ModelIR) -> Union{Nothing, Int}

Find the clock (rule I2) and mark it CLOCK, returning its variable index.

A variable is a clock when every equation declared for it is the constant 1 (running) or 0 (frozen), at least one of them is 1 — a clock has to run somewhere — and it drives no other state. That last condition is what separates a clock from an ordinary state that merely happens to be held constant.

dynamics_function(ir, backend, expressions, supplied) -> f

The callable f(x, u) for one scope: the Julia function the user supplied, if any, otherwise the compiled expressions.

has_set_guard(t::TransitionIR) -> Bool

Whether the transition carries anything beyond per-coordinate bounds, i.e. whether its guard is more than a box.

has_user_dynamics(ir) -> Bool

Whether any dynamics were supplied as a Julia function rather than written as equations.

infer_roles!(ir::ModelIR)

Assign a VariableRole to every variable and validate the model as a whole.

Rules (src/wrapper/README.md §3): a variable carrying ∂/Δ dynamics is a STATE (I1); any other variable appearing on a dynamics right-hand side is an INPUT (I3); a variable that appears nowhere is an error (I4), because it would otherwise be silently discretized as an input and enlarge the abstraction.

input_indices(ir) -> Vector{Int}

MOI indices of the input variables, in declaration order.

is_hybrid(ir) -> Bool

Whether the model declared any mode.

lower(model) -> Problem.ProblemType

Compile the model into its (system, problem) pair without solving it: fold in the options, infer the variable roles, and lower. model may be the JuMP model or the underlying Optimizer.

This is the first half of optimize!, exposed so a model can be inspected — or tested — without paying for an abstraction.

mode_ids(ir) -> Vector{Int}

Mode identifiers in declaration order. They index the HybridSystems automaton directly, so they must be 1:n; infer_roles! checks that.

obstacle_sets(ir, x_idx) -> Vector{LazySets.LazySet}

The obstacles of ir as sets over the state coordinates x_idx, ready to be removed from the state space.

An MOI.HyperRectangle may be written over a subset of the coordinates and is extruded across the variable bounds on the rest; any other bounded LazySet is taken as written and must span the whole state vector.

select_solver(system, problem) -> optimizer type

The solver family to use for a lowered (system, problem) pair when the user set no "solver" attribute. Add a method to support a new family.

set_role!(x, role)

Declare what x is, instead of letting the wrapper infer it. x may be a single variable or an array of them, and role one of Dionysos.STATE, Dionysos.INPUT, Dionysos.CLOCK.

Needed when the dynamics are supplied as a Julia function rather than written as equations — there are no expressions to infer from, so the states have to be named:

set_role!(x, Dionysos.STATE)
set_attribute(model, "dynamics", (x, u) -> [x[2], -sin(x[1]) + u[1]])

Variables left undeclared are inputs.

simulate(model, x0; nsteps = 100, stopping = nothing) -> System.Trajectory

Run the synthesized controller in closed loop from x0 for at most nsteps steps.

model is the JuMP model (or the underlying Optimizer) after optimize!. The stopping criterion defaults to the one implied by the specification — reaching the target, or leaving the safe set — and can be overridden with stopping.

When the solver was configured with use_periodic_mapping, the closed loop folds the state into the same period the abstraction used, and the specification sets are compared in those coordinates. Without it the state would leave the controller's domain after one revolution.

Returns the channelled Dionysos.System.Trajectory; read it with System.states, System.inputs, … or plot it directly.

state_box(ir, x_idx) -> LazySets.Hyperrectangle

The state box declared by the variable bounds, before obstacles are carved out.

state_indices(ir) -> Vector{Int}

MOI indices of the state variables, in declaration order — this is the order of x in the lowered system.

supports_problem(solver_type, problem_type) -> Bool

Whether solver_type can solve problem_type. Declared per family so an unsupported combination is reported by the front-end, naming both, instead of failing deep inside a sub-solver.

to_stepper(specification)

Turn what the user attached with @specification into the automaton the co-safe solver steps. A stepper passes through unchanged; DionysosSpotExt adds the method that compiles a Spot.SpotFormula.

set_attribute(mode::Mode, name::String, value)

Set a solver option for this mode alone — each mode of a hybrid model is abstracted by its own sub-solver, so state_grid, input_grid and time_step are per-mode:

set_attribute(off, "state_grid", MP.GridFree(SVector(0.0), SVector(0.1)))

Options set on the model itself apply to every mode unless a mode overrides them.

SpecSet

Any of the specification markers Start, Final, Always, EventuallyAlways.

final(x)

The value of x at the end of the trajectory, used to declare a reach target: @constraint(model, final(x[1]) in MOI.Interval(a, b)).

start(x)

The value of x at the beginning of the trajectory, used to declare an initial set: @constraint(model, start(x[1]) in MOI.Interval(a, b)). The @variable(model, x, start = v) keyword is the singleton special case.

Δ(x)

Discrete-time successor of the state x: @constraint(model, Δ(x[1]) == x[1] + u[1]). Mixing Δ and ∂ in one model is an error.

∂(x)

Continuous-time derivative of the state x, used to declare dynamics: @constraint(model, ∂(x[1]) == u[1]). A variable carrying a ∂ (or Δ) constraint is a state; see infer_roles!.

@mode(model, name)

Declare a mode. Like @variable, this binds name in the calling scope and registers the mode in the model's object dictionary — no assignment needed:

@mode(model, off)
@constraint(off, ∂(T) == -α * (T - Ta))     # `off` is already bound
model[:off] === off                          # and registered

The macro also returns the mode, so off = @mode(model, off) works too; it is simply redundant. add_mode! is the function form, for a name computed at runtime.

@specification(model, formula)

Attach the temporal formula the trajectory must satisfy, over the regions named with Label:

@specification(model, ltl"F(goal) & G(!hazard)")

formula may be a Spot.SpotFormula (with using Spot) or any Optim.DiscreteSystems.AbstractSpecStepper — a hand-written monitor, for instance. A model carrying a formula lowers to a CoSafeLTLProblem.