| You could keep a history of messages that the system has seen at some point and add a precondition to the message input action that requires the message not to be an element of that message history.
However, I speculate (without having seen your spec) that this is not necessary for what you are trying to verify: presumably there is no fairness condition for inputting a new message (since it would constrain the environment rather than the system that you are specifying), so the execution in which m1 is input and then lost (and in which m1 never reappears) is a valid counter-example that should be found by TLC.
Stephan
Yes, thank you, it does help. I think i can implement this, but i still have one doubt.
As i mentioned before, technically, every Message is unique throughout the entire lifetime of the system. I dont know how to specify my model value messages like that. I suspect, that what might happen is for example: The system receives message m1, then looses it, which would violate the liveness property. But then after a while, TLC inputs m1 again, which this time is not lost, thus satisfying the liveness property in the end. Can i somehow prevent that from happening? Is that even an issue? On Tuesday, April 2, 2019 at 5:18:32 PM UTC+2, Stephan Merz wrote: Stepping back a bit, it appears to me that you'd like to check a property of the form
A ~> B
where A and B are both actions. Such a formula is not syntactically well-formed in TLA (although it is indeed stuttering invariant). TLA allows such a formula to be written only if A and B are temporal formulas, including state predicates. You can work around this limitation by adding variables done_A and done_B that are initialized to FALSE and set to true whenever A and B happen. Then check the property
done_A ~> done_B
(Since your actual actions take parameters the details are a bit more complicated and you may need to use functions but I think you get the idea.)
In practice, you won't actually need to introduce these helper variables because the system state probably already contains enough information to tell you when A and B occurred. The overall idea is to replace the actions by suitable state predicates.
Hope this helps, Stephan
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?
-- 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 tla...@googlegroups.com. To post to this group, send email to tla...@googlegroups.com. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.
-- 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.
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.
|