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

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

On Tuesday, 2 April 2019 05:50:36 UTC-4, Michael Chonewicz wrote:
Ah, so thats what it was! Thank you. I have modified ReceiveMsg to look like this:

ReceiveCallback(msg) ==
And used ReceiveCallback in the liveness instead of ReceiveMsg:

LivenessSpec ==
/\ \A msg \in Message :
\E result \in ResultssForMsg(msg) :
ReceiveCallback(msg) ~> ResultCallback(result)

The ResultCallback already looked like ReceiveCallback above. This fixed the compile issue. Then i removed the old LivenessSpec from my Spec completely(not even fairness is left):

If I'm understanding correctly, you're saying that `ReceiveCallback` and `ResultCallback` are _both_ just equivalent to TRUE?

If that's the case, then the temporal property is trivially satisfied for every behaviour. It comes down to `TRUE -> TRUE`.

Or have I misunderstood?

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.