Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_exclusive_fixed_points

pub fn mk_formula_exclusive_fixed_points(steady_state_list: &[String]) -> String

Create HCTL formula describing that 1) each sub-space (observation) in a list must contain a steady state and 2) prohibits existence of any additional steady states outside of these sub-spaces.

Basically a conjunction of two formulas, see mk_formula_fixed_point_list and mk_formula_forbid_other_attractors for details.

FIXED_POINTS({states}) & NO_OTHER_FIXED_POINTS({states})

Arg steady_state_list is a vector of formulae, each encoding one state of interested.