Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_fixed_point

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

Create HCTL formula describing that given sub-space (observation) must contain a steady state (fixed-point).

This function works for sub-spaces in general, but if you have a singleton sub-space (a state), we recommend using mk_formula_fixed_point_specific - is more optimized).

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

Arg steady_state is a formula encoding the sub-space with the state of interest.