Function biodivine_sketchbook::algorithms::eval_dynamic::prepare_graph::prepare_graph_for_dynamic_hctl

pub fn prepare_graph_for_dynamic_hctl(
    bn: &BooleanNetwork,
    dyn_props: &Vec<ProcessedDynProp>,
    unit: Option<(&Bdd, &SymbolicContext)>,
) -> Result<SymbolicAsyncGraph, String>

Prepare the symbolic context and generate the symbolic transition graph for evaluation of the dynamic properties.

Most of the properties are encoded as HCTL formulas. Therefore we just prepare symbolic variables to handle all variables in HCTL formulas. We always have at least one set of symbolic variables, as they can be used when computing trap spaces.

Note that some cases like trap spaces need different kind of symbolic context and graph, but this context is always the same and is easily handled during evaluation.

Arg unit is optional unit BDD with potentially different symbolic context (can have different symbolic variables, but has the same bn vars and colors).