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, buy my guess is that either `ReceiveMsg` or `ResultCallback` are actions, i.e., they used primed variables.