Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_reachability_pair

source ยท 
pub fn mk_formula_reachability_pair(
    from_state: &str,
    to_state: &str,
    is_negative: bool,
) -> String
Expand description

Create HCTL formula describing that there is (not) a path between (any) states of two sub-spaces.

positive: EXISTS x. JUMP x. {from_state} & EF {to_state} negative: EXISTS x. JUMP x. {from_state} & !EF {to_state}

from_state and to_state are both formulae encoding particular sub-spaces. is_negative is true iff we want to encode non-existence of path.