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:
And used ReceiveCallback in the liveness instead of ReceiveMsg:
/\ \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?