[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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(resultaction 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.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.