Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_fixed_point_specific

pub fn mk_formula_fixed_point_specific(steady_state: &str) -> String

Create HCTL formula describing that given state is a steady state (fixed-point).

EXISTS x. JUMP x. ({state} & AX {state})

Arg steady_state is a formula encoding the state of interest. The state must be fully specified (conjunction of literals for EACH proposition).