subreachability

Function subreachability 

Source
pub fn subreachability(
    m: &ModalDblModel<Unital>,
    data: ReachabilityProblemData,
) -> bool
Expand description

The “Region Algebra for Petri Nets” algorithm from Ch 31 of (Clarke et al 2018): “Symbolic Model Checking in Non Boolean Domains”.