Symbolic

AbstractAutomatonList <: HybridSystems.AbstractAutomaton

Interface for the finite automaton backing a symbolic model: a set of transitions over integer states and input symbols. Transitions are stored and enumerated as (target, source, symbol) tuples (see TransitionKey).

Extending

Implement get_n_state, get_n_input, enum_transitions, add_transition!, pre, post and Base.empty!. Concrete implementations trade memory for pre/post speed: SortedAutomatonList (compact, sorted-set backed), IndexedAutomatonList (dict indices) and FastIndexedAutomatonList (dense vector indices).

AbstractExecutionBackend

Abstract type for execution backends used to compute the transition relation in grid-based symbolic abstraction.

An execution backend defines how the abstraction computation is executed:

• sequentially,
• multithreaded,
• distributed across Julia workers,
• or via SLURM array jobs.

AbstractLift

A composable, optional generalization applied to a base AbstractSymbolicModel: it adds one factor (an extra axis) to the abstraction. Concrete lifts:

• ClockLift — adds a monotone time axis t;
• a mode lift (planned) — adds the hybrid mode axis k.

The four abstractions x, (x,t), (x,k), (x,k,t) are obtained by applying zero, one, or both lifts to a base model. Each lift implements lift(l, model) (and, in a later phase, lift(l, spec) so specifications extend the same way).

AbstractSymbolicModel

Root of the symbolic-model hierarchy: anything that owns a finite automaton (get_automaton). Models with a single concrete state/input space of fixed dimension subtype SymbolicModel{N, M}; models whose spaces vary per mode (e.g. HybridSymbolicModel) subtype this root directly.

ClockAbstraction{N, T}

Symbolic abstraction of a 1-D monotone clock (the time axis of one mode of a timed hybrid system, or a standalone clock lifted onto a continuous model).

tsteps are the discretized time values; domain is the concrete time domain X; is_active distinguishes an evolving clock (ẋ = 1, matrix A = I) from a frozen one (A = 0).

ClockAbstraction(domain, tstep::Float64)

Build an active ClockAbstraction directly from a 1-D time domain (a box interval) discretized with step tstep. Used to lift a continuous model with a clock (no time subsystem required).

ClockAbstraction(sys::ConstrainedLinearContinuousSystem, tstep)

Build a ClockAbstraction from a linear time subsystem. The dynamics matrix A must be the identity (time evolves, discretized with step tstep over the box time domain) or zero (time frozen, a single step at 0.0).

ClockLift{C} <: AbstractLift

The time lift: augments a base abstraction with a monotone clock ClockAbstraction, turning a model of x into a model of (x, t). The same lift applies to a plain continuous model or (per mode) to a hybrid mode, so it is the single reusable mechanism for time-dependent abstractions.

ClockLiftedSymbolicModel{B, C, A} <: AbstractSymbolicModel

Result of lift(::ClockLift, base): the synchronized product of a base model with a clock. Abstract states are the flattened (base_state_id, time_id) pairs; the concrete coordinate is the augmented vector [x; t] (time is the trailing dimension). For an active clock a base transition q → q′ is replicated as (q, p) → (q′, p+1) across time steps; a frozen clock keeps p fixed.

Inputs pass through to base unchanged (the clock adds no inputs).

FastIndexedAutomatonList <: AbstractAutomatonList

Automaton with dense vector indices: postmap is keyed by the flattened (state, symbol) pair and premap by target state, so post/pre are direct array lookups. Fastest to query and densest in memory; best for large fixed automata. Call finalize! after bulk insertion to deduplicate.

FlatIndex{K}

Bijection between composite keys of type K (e.g. an augmented-state tuple) and a dense integer range 1:n. Backs the flattened integer numbering used by product/lifted symbolic models.

Both directions are O(1): id_to_key is a plain vector (id → key), key_to_id a hash map (key → id). Absence is encoded by the id 0, so callers can branch on flat_id(...) > 0 without a second lookup.

FlatIndex(keys::AbstractVector{K}) -> FlatIndex{K}

Build a FlatIndex from a vector of unique keys, numbering them 1:length(keys) in order.

GlobalInputMap

Bijection between per-mode local input ids and a single global input alphabet for a timed hybrid system. Continuous inputs (one block per mode) occupy continuous_range; switching inputs (one per hybrid-automaton transition) occupy switching_range.

Fields

• total_inputs, continuous_inputs, switching_inputs: counts.
• continuous_to_global / global_to_continuous: (mode_id, local_input_id) ↔ global_id.
• switching_to_global / global_to_switching: transition_id ↔ global_id.
• continuous_range, switching_range: the id ranges of each block.
• switch_labels: human-readable "SWITCH src -> tgt" label per switching input.

GlobalInputMap(mode_models, hs::HybridSystem)

Build the GlobalInputMap for a hybrid system from its per-mode symbolic models: continuous inputs are laid out mode by mode, then one switching input per hybrid-automaton transition.

GridBasedSymbolicModel{N,M} <: SymbolicModel{N,M}

Intermediate abstract type for symbolic models that rely on a grid-based or mapping-based discretization.

Semantics:

• state mapping: global abstract-state numbering / coordinate map
• input mapping: global abstract-input numbering / coordinate map
• state set (Xset): states enumerated as sources
• retained set (Rset): states allowed as targets

HybridBuildReport

What the hybrid composition had to discard while wiring the mode switches, per transition.

A switch is built by discretizing the guard INNER and quantizing the reset image of each guard cell into the target mode, and both steps can lose cells. Losing all of them is an error — a transition that survives into the automaton with no switch is a model the user did not write — but a partial loss is legitimate and was previously only warned about. Recording it makes it inspectable from the built model, and assertable from a test.

Fields

• dropped_resets: transition_id => (dropped, total) guard cells whose reset image fell outside the target mode's domain.
• inexact_resets: transition_id => offset, the largest relative distance between a reset image and the cell centre it was snapped to. A non-zero entry means the reset is not lattice-exact, and the abstraction may be unsound.

HybridSymbolicModel{Mods, A, G} <: AbstractSymbolicModel

Symbolic abstraction of a hybrid system, composed from one AbstractSymbolicModel per mode via a ModeLift. Each mode model is either a plain spatial abstraction (x) or a ClockLiftedSymbolicModel ((x, t)); the (local_state_id, mode_id) pairs are flattened to a single integer numbering and wired into one automaton, with inputs unified through a GlobalInputMap.

Fields

• mode_models: per-mode symbolic models.
• flat: FlatIndex bijection between the integer numbering and the (local_state_id, mode_id) pairs.
• automaton: the flattened transition automaton.
• input_mapping: the global input map.
• report: the HybridBuildReport of what the switch wiring discarded.

IndexedAutomatonList <: AbstractAutomatonList

Automaton that maintains dictionary indices (postmap, premap) alongside the transition list, giving O(1) post(q, u) and pre(q′) at the cost of extra memory. Suited to repeated fixed-point queries on a fixed automaton.

JuliaDistributedBackend(
    procs=nothing,
    nparts=nothing,
    partition_strategy=:roundrobin,
    threaded_per_worker=false,
)

Distributed execution over Julia worker processes. Each worker receives its share of the work in a single remotecall carrying the symbolic model and the approximation explicitly — there is no per-worker global state to install or clear, and workers JIT-compile in parallel inside their call.

Parameters

• procs: worker IDs (defaults to Distributed.workers()).
• nparts: number of partitions (defaults to number of workers).
• partition_strategy: how to split states (:roundrobin or :contiguous).
• threaded_per_worker: enable threading inside each worker.

LocalGridBasedSymbolicModel

Wrapper around a global symbolic model that overrides only the source domain. The state mapping, input mapping, retained domain and input domain remain global.

ModeLift{H, G} <: AbstractLift

The mode lift: composes one AbstractSymbolicModel per mode into a single HybridSymbolicModel, wiring the guarded, reset-coupled switches of the hybrid automaton hs and unifying inputs through input_mapping.

Unlike ClockLift — which lifts a single base model — ModeLift consumes a vector of per-mode base models (each plain or clock-lifted), so it is applied via lift(l, mode_models).

SequentialBackend()

Sequential execution (no parallelism).

SlurmArrayBackend(
    nchunks,
    chunk_id=nothing,
    outdir,
    partition_strategy=:contiguous,
    write_only=true,
)

Execution using SLURM array jobs (file-based parallelism).

SortedAutomatonList <: AbstractAutomatonList

Automaton backed by a sorted tuple set of (target, source, symbol) transitions. Compact and cheap to build; pre/post are answered by range queries on the sorted set. Good default when memory matters.

Abstract Type: SymbolicModel{N, M}

Defines a generic symbolic model interface, where:

• N is the state space dimension.
• M is the input space dimension.

SymbolicModelList:

• X: source states bundled with the state mapping (MP.MappedStateSet)
• R: allowed target states, same state mapping ("relation universe allowance")
• U: inputs considered, bundled with the input mapping

ThreadedBackend(progress_dt=0.2)

Multithreaded execution using all available Julia threads.

TransitionKey = NTuple{3, Int}

A transition, stored and enumerated as (target, source, symbol). Note the ordering flip vs. add_transition!(autom, source, target, symbol), whose arguments put the source first. Prefer the transition_target/transition_source/transition_symbol accessors over raw positional indexing at call sites.

abstract_switch_target(mode_model, reset_coord) -> Int

Local abstract state of a guarded-switch target in mode_model, from the concrete coordinate produced by the reset map (0 if out of range). For a clock-lifted mode the coordinate is [x; t] and the time is rounded up (the smallest clock step ≥ t); for a time-free mode it is just x.

add_inter_mode_transitions!(transition_list, hs, mode_models, input_mapping) -> HybridBuildReport

Add the guarded mode-switch transitions using each transition's guard and reset map.

A transition that ends up contributing no switch is an error, not a warning: the model declared a switch, the abstraction silently has none, and synthesis then answers for a disconnected system while reporting success. A partial loss is legitimate and is recorded in the returned report instead.

Embed each mode model's own transitions into the global list, relabelling inputs.

base_state_and_time(m::ClockLiftedSymbolicModel, id) -> (x, t)

Decompose a flattened id into the base concrete state x (unaugmented, keeping the base's coordinate type) and the clock value t. Used by the mode composition to build a hybrid coordinate without re-splitting the [x; t] vector.

build_all_transitions(hs, mode_models, input_mapping) -> (transitions, report)

Assemble every hybrid transition: intra-mode (each mode model's own transitions, which already encode any time advance) followed by inter-mode (guarded switches between modes). The HybridBuildReport records what the switch wiring had to discard.

build_symbolic_automaton(transition_list, mode_models, input_mapping) -> (flat, automaton)

Flatten the hybrid transitions into an IndexedAutomatonList, returning (flat, automaton) where flat is the FlatIndex between the integer numbering and the (local_id, mode_id) pairs.

ceil_time2int(tm::ClockAbstraction, t) -> Int

Index of the smallest time step ≥ t (always 1 when time is frozen).

Append the successors of (source, symbol) to targetlist in place.

determinize_symbolic_model(sym; AutomatonConstructor, convert_U_to_list)

Return a deterministic symbolic model by refining the input alphabet: each original input u is replaced by a pair (u_coord, target_state).

This is useful to turn nondeterministic transitions into deterministic ones by making the target part of the symbol.

Enumerate the local input ids of mode_id.

finalize!(autom::AbstractAutomatonList)

Compact the automaton after bulk transition insertion (e.g. deduplicate index entries). The generic fallback is a no-op; implementations that accumulate duplicates override it. Returns the automaton.

Flattened id of key, or 0 if the key is absent.

Key associated with flattened id id (bounds-checked by the caller).

floor_time2int(tm::ClockAbstraction, t) -> Int

Index of the largest time step ≤ t (always 1 when time is frozen).

Abstract a concrete input in mode_id to its global input id (0 if not found).

Abstract an augmented coordinate [x; t] to its flattened id (0 if absent).

get_abstract_state(model::HybridSymbolicModel, augmented_state) -> Int

Abstract a concrete augmented state ((x, t, mode) or (x, mode)) to its flattened index, or 0 if it is out of the abstraction's domain (unknown mode, or a spatial/time coordinate outside the grid). Callers that require a valid state (e.g. an initial state) should check for 0.

The HybridBuildReport of what building this model's mode switches discarded.

Concretize global input input_id in mode_id (nothing for switching inputs).

Concretize a flattened id to the augmented coordinate [x; t].

get_concrete_state(model::HybridSymbolicModel, state_index) -> (x[, t], mode_id)

Concretize a flattened state index to the augmented concrete state: (x, t, mode) for a clock-lifted mode, (x, mode) for a time-free mode.

Global input id of a local continuous input (mode_id, local_input_id) (0 if absent).

The GlobalInputMap unifying the modes' inputs and the mode switches.

get_local_input_info(gim::GlobalInputMap, global_id) -> (kind, info)

Classify a global input id: returns (:continuous, (mode_id, local_input_id)), (:switching, transition_id), or (:invalid, nothing).

Total number of global inputs (continuous + switching).

Number of (flattened) hybrid states.

get_states_from_set(m::ClockLiftedSymbolicModel, set, incl_mode)

Flattened states whose spatial part lies in the projection of set onto the base coordinates and whose time index lies in the projection onto the trailing (time) dimension. set is a box over [x; t].

get_switch_label(gim::GlobalInputMap, transition_id) -> String

The label a controller must emit to take hybrid transition transition_id.

Always ask for it rather than formatting one: the label is the control input of a mode switch, and its spelling is a contract between this map, the simulation that parses it back, and every controller that issues one. Rebuilding the string elsewhere silently breaks the day the format changes.

Global input id of the switching input for transition_id (0 if absent).

int2time(tm::ClockAbstraction, idx) -> Float64

Time value at index idx (always 0.0 when time is frozen).

Whether global_id is a continuous input.

Whether global_id is a switching input.

lift(l::AbstractLift, base::AbstractSymbolicModel) -> AbstractSymbolicModel

Apply the lift l to base, returning a symbolic model with one additional factor.

lift(l::ModeLift, mode_models) -> HybridSymbolicModel

Compose the per-mode mode_models (each plain or clock-lifted) into a hybrid symbolic model, assembling the intra-mode and guarded inter-mode transitions.

lift_per_slice(bases, clock) -> ClockLiftedSymbolicModel

Clock lift with per-time-slice dynamics: bases[p] is the spatial abstraction valid at clock step p — for time-varying dynamics f(x, u, t), the abstraction of f(·, ·, t_p). The transitions out of slice p come from bases[p], advancing the clock to p+1. All bases must share the same state/input grid (only their transitions differ), so any of them concretizes a (q, p) state.

For time-invariant dynamics, lift(ClockLift(clock), base) is the cheaper equivalent (one base replicated across every slice).

Number of flattened ids.

Clock-lifted model + base spec: matching base states at every time index.

Clock-lifted model + timed spec: matching base states within the time window.

Hybrid model + mode spec: per-mode local states mapped to global ids.

Abstract states of a base model satisfying a base state spec.