On Monday, 1 April 2019 06:15:17 UTC-4, Michael Chonewicz wrote:
Spec ==
/\ Init
/\ LivenessSpec
/\ [][Next]_variables
There are generally two separate parts to liveness checking, and I think you might be conflating them.
First, you must specify appropriate fairness conditions (via WF_ and/or SF_). This determines which parts of your specification are fair, and the particular kind of fairness.
The second is specifying temporal properties that you want TLC to check. When you specify a temporal property, you add it to the "Properties" listing in the model checker.
If you don't specify a temporal property, then TLC won't check for liveness, and thus you won't see any violations.
Your second version of the code places a `~>` inside of `LivenessSpec`, which really throws me for a loop, and it's where I'm getting the idea that you might be conflating the two things. If you want LivenessSpec to have a `~>` in it, then don't add it as a conjunct to the `Spec`.