Symbolic

Abstract Type: SymbolicModel{N, M}

Defines a generic symbolic model interface, where:

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

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
• source domain (Xset): states enumerated as sources
• retained domain (Rset): states allowed as targets

SymbolicModelList:

• XMapping / UMapping define universes and conversions
• Xset: states we build from (sources)
• Rset: allowed states as targets (superset; "relation universe allowance")
• Uset: inputs considered

LocalGridBasedSymbolicModel

Wrapper around a global symbolic model that overrides only the source-domain enumeration while keeping the same global state/input mappings and retained set.

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.

init_abstraction_workers!(procs, symmodel, concrete_system_approx; warmup=true)

Install heavy read-only data on each worker once. Optionally warm up the worker.

_install_distributed_abstraction_data!(symmodel, concrete_system_approx)

Install the heavy read-only abstraction objects in worker-local storage. This is meant to run on each worker process once.

_warmup_distributed_abstraction_worker!()

Cheap warm-up of the main abstraction code paths on the current worker. This helps separate compilation/setup from actual benchmark timings.

partition_source_state_ids(symmodel, nparts; strategy=:roundrobin)

Partition the source abstract states into nparts lists of state ids. This ships only integer ids to workers, not the whole symbolic model.

_run_local_partition_ids(state_ids; ...)

Run abstraction on the current worker for the source states listed in state_ids, using the worker-local persistent symbolic model and concrete approximation.

assign_states_to_workers(parts, procs)

Assign the partition list parts to workers in procs using round-robin, then merge the partitions assigned to the same worker into a single vector of state ids. Returns a vector of pairs (p, ids).

_make_local_symmodel_from_ids(state_ids)

Construct a local wrapper on the current worker using the worker-local parent symbolic model and the provided state ids.

_clear_distributed_abstraction_data!()

Clear worker-local persistent storage.

clear_abstraction_workers!(procs)

Clear worker-local persistent storage.