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

[Jay Parlar <parlar@xxxxxxxxx>]

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) ==
    TRUE


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.