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

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

 

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