Function is_well_founded 

pub fn is_well_founded(system: &TransitionSystem) -> bool

Is the system well-founded (acyclic — no infinite forward trajectory)? Equivalent, for a finite system, to “is a DAG”. Computed by Kahn’s algorithm: a full topological order exists iff there is no cycle.