Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_attractor_specific

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

Create HCTL formula describing that given specific state is part of an attractor.

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

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