Skip to main content

liveness_witness

logicaffeine_compile::spatial::certificate

Function liveness_witness 

Source 
pub fn liveness_witness(
    g: &MarkedGraph,
) -> Result<LivenessWitness, CertifyFault>
Expand description

Commoner’s condition on the unrolled net: a starved transition or a token-free cycle is a fault; else the topological order over token-free arcs is the witness.