Function biodivine_sketchbook::algorithms::eval_dynamic::encode::mk_formula_reachability_chain

pub fn mk_formula_reachability_chain(states_sequence: &[String]) -> String

Create a formula describing the existence of path between any states of every two consecutive sub-spaces from the states_sequence, starting with the first one.

Basically, this can be used to describe a time series s0 -> s1 -> … -> sN

EXISTS x. JUMP x. ({state1} & EF ({state2} & EF( ... )))