Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_exclusive_attractors

pub fn mk_formula_exclusive_attractors(
    attractor_state_list: &[String],
) -> String

Create HCTL formula describing that 1) each sub-space (observation) in a list must contain a state that is part of an attractor and 2) prohibits existence of any additional attractor that does not contain a state from some of these sub-spaces.

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

ALL_ATTRACTORS({states}) & NO_OTHER_ATTRACTORS({states})