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.