Module mikino_api::trans [−][src]
Expand description
Transition system structures and helpers.
A transition system is composed of
- an initial predicate,
- a transition predicate, and
- a list of named Proof Obligations (POs).
The initial predicate and the POs are stateless expressions expr::Expr. The transition
relation is a stateful expression expr::SExpr.
A system also contains declarations Decls for its state variables