GitHub

Symbolic

This folder contains the data structures needed to encode the different abstractions.

Dionysos.Symbolic.SymbolicModel — Type
Abstract Type: SymbolicModel{N, M}

Defines a generic symbolic model interface, where:

  • N is the state space dimension.
  • M is the input space dimension.
source
Dionysos.Symbolic.GridBasedSymbolicModel — Type
GridBasedSymbolicModel{N, M} <: SymbolicModel{N, M}

An intermediate abstract type for symbolic models that rely on a grid-based discretization.

  • N: Dimension of the state space.
  • M: Dimension of the input space.
source
Dionysos.Symbolic.SymbolicModelList — Type

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
source
Dionysos.Symbolic.determinize_symbolic_model — Function
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.

source