Function mikino_api::parse::script

source · [−]
pub fn script(txt: &str) -> Res<Block<Expr<'_>, Expr<'_>>>
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.