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

Ah, so thats what it was! Thank you. I have modified ReceiveMsg to look like this:

ReceiveCallback(msg) ==
    TRUE


ReceiveMsg(msg) ==
    /\ MsgQueue!Push(msg)
    /\ UNCHANGED <<proc1Queue, resultQueue>>
    /\ 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):

Spec ==
    /\ Init
\*    /\ FairnessSpec
    /\ [][Next]_variables 

and lastly added the LivenessSpec (the version with the leads-to operator) as a property of the model in TLC. My hopes were that the spec would crash this time. It did check the liveness, but unfortunately, still no crash.

Could it be that during model checking, even though a message M is lost during the BrokenCallback step, M at some point will be put into the system again and processed correctly, leading to the liveness condition being satisfied in the end? Technically every message should be unique (ReceiveMsg is only called once for a message during the entire life of the system), but I'm not entirely sure if the model checker violates this rule.

On Monday, April 1, 2019 at 11:29:17 PM UTC+2, Jay Parlar wrote:

On Monday, 1 April 2019 16:44:51 UTC-4, Michael Chonewicz wrote:

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.

Yep!

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?

I can't say for certain, because you didn't include your entire original spec, but my guess is that either `ReceiveMsg` or `ResultCallback` are actions, i.e., they used primed variables.

Jay P.