1 2 3 4 5
\* Direct-TLC liveness check for DLV-0017 lifecycle termination. \* Run from specs/: java -jar tla2tools.jar -config LifecycleModel.cfg LifecycleModel.tla SPECIFICATION LifeSpec PROPERTY MessageTerminates INVARIANT LifeRetriesBounded