[tlaplus] Re: [noob] Liveness property not violated as expected

Thank you for your answer!

I see. So if i understand this correctly, fairness conditions are not liveness properties that are checked for (which actually makes sense now that i think about it). So my LivenessSpec doesn't actually do any liveness checking. To do that, I have to add the actual liveness property (the second version of my LivenessSpec) to the model. But one question remains, whats wrong with my second version? I don't understand the error. How could i make the ReceiveMsg(msg) ~> ResultCallback(result) action into a temporal formula or a state predicate?

On Monday, April 1, 2019 at 3:46:27 PM UTC+2, Jay Parlar wrote:

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`.

Jay P.