Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_attractor

pub fn mk_formula_attractor(attractor_state: &str) -> String

Create HCTL formula describing that given sub-space (observation) must contain a state that is part of an attractor.

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

EXISTS x. JUMP x. ({state} & (AG EF ({state} & x)))

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