Module liveness 

Liveness-to-Safety Reduction

Liveness properties (G(F(p)) — “p always eventually holds”) cannot be checked by BMC or k-induction directly. The Biere-Artho-Schuppan (2002) reduction:

1. Add a shadow copy of the state
2. Non-deterministically “freeze” the shadow at some point
3. Check that the property eventually holds after the freeze

If the safety property on the doubled state space holds → liveness holds. If violated → extract lasso-shaped counterexample (prefix + loop).

Enums

LivenessResult

Result of liveness checking.

Functions

check_liveness

Check a liveness property via bounded search.