Symbolic
This folder contains the data structures needed to encode the different abstractions.
Dionysos.Symbolic.SymbolicModel
— TypeAbstract Type: SymbolicModel{N, M}
Defines a generic symbolic model interface, where:
N
is the state space dimension.M
is the input space dimension.
Dionysos.Symbolic.GridBasedSymbolicModel
— TypeGridBasedSymbolicModel{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.
Dionysos.Symbolic.SymbolicModelList
— TypeSymbolicModelList{N, M, S1, S2, A} <: GridBasedSymbolicModel{N, M}
A classical symbolic model where the entire domain is partitioned into grid cells.
Dionysos.Symbolic.LazySymbolicModelList
— TypeLazySymbolicModel{N, M, S1, S2, A} <: GridBasedSymbolicModel{N, M}
A symbolic model using lazy abstraction where the automaton is computed only for a subset of the state space.
Dionysos.Symbolic.compute_symmodel_from_hybridcontrolsystem!
— Functioncompute_symmodel_from_hybridcontrolsystem!(symmodel::SymbolicModel{N}, transitionCost::AbstractDict, transitionCont::AbstractDict,
hybridsys::AbstractHybridSystem, W, L, U, opt_sdp, opt_qp)
Builds an abstraction symmodel
where the transitions have costs given in transitionCost
and are parameterized by affine-feedback controllers in transitionCont
. The concrete system is hybridsys
and W
, L
and U
are defined as in _has_transition
. An SDP optimizer opt_sdp
and a QP optimizer opt_qp
must be provided as JuMP optimizers.