Yes, they are both TRUE. My understanding was that
ReceiveCallback(msg) ~> ResultCallback(result) assures that a call to the ReceiveCallback will eventually lead to ResultCallback. But it doesn't matter what i do with the message inside of these actions, so I just return TRUE. My thinking was that if ResultCallback never gets called, it cannot be TRUE, thus failing the liveness condition.
This does seem sketchy now that you have pointed it out, but I dont really know what i could put in there, since the only purpose of those actions was to use them in the LivenessSpec. Maybe you know how else i could solve this?
On Tuesday, April 2, 2019 at 3:43:29 PM UTC+2, Jay Parlar wrote:
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?