Function mikino_api::parse::script
source · [−]Expand description
Parses a system, requires the parser
feature.
Comments are one-line rust-style: // ..\n
.
A system is composed of four { ... }
blocks each starting with a specific keyword:
-
svars { ... }
: the state variables of the system; -
init { ... }
: the initial predicate, i.e. a stateless (no'
prime) expression; -
trans { ... }
: the transition relation, i.e. a stateful ('
primes allowed) expression; -
candidates { ... }
: some candidates to prove over the systems.