Constant NONMONOTONE_SEMANTICS 

pub const NONMONOTONE_SEMANTICS: &str = "Synchronous iteration per SCC; if a fixpoint is reached, use it; if a cycle is detected, use the intersection of all states in the cycle (skeptical tuples only); if the iteration budget is exceeded, use the intersection across all visited states (conservative).";

Bounded semantics for non-monotone SCC evaluation inside MC sampling.