Understanding fairness can be tricky. When
SF_vars (Sender /\ (msgC' /= msgC))
is replaced by
WF_vars (Sender /\ (msgC' /= msgC))
execution of a Sender action changing the message queue is guaranteed to eventually happen if such an action is persistently enabled from some point on. However, notice in the counter-example that TLC produces that the Sender process alternates between positions l_send and l_depart, and that no Sender action changing msgC is enabled at label l_depart (since the corresponding statement leaves msgC unchanged). In fact, the claim in your message
That means "either" clause of "Sender" process is continuously enabled.
is not true since control is not continuously at the "either" clause. However, the action is infinitely often enabled, namely whenever the sender is at label l_send, and strong fairness implies that the action will occur.
Alternatively, you can remove the label l_depart (don't forget to regenerate the TLA+), and your property will hold and be checked by TLC with the above weak fairness condition. However, this means that you assume the entire Sender action to happen atomically, and whether this is realistic or not depends on the system that you have in mind.
Hope this helps,
Thank to you folks I made a little progress but I am still a little confused about fairness, especially weak fairness.
I downloaded the new version, added the following STRONG fairness to the spec (the original one, with both sender and receiver, ), and tlc reported no error
/\ SF_vars (Sender /\ (ackC' /= ackC ))
/\ SF_vars (Sender /\ (msgC' /= msgC))
/\ SF_vars (Receiver /\ (ackC' /= ackC ))
/\ SF_vars (Receiver /\ (msgC' /= msgC))
But when I changed the strong fairness to weak fairness, TLC report a state loop where ackC is repatedly filled with 0 by the Receiver and drained by the Sender, but msgC remains empty.
At all these states, toSend = 0. That means "either" clause of "Sender" process is continuously enabled. And I did say, WF_vars(Sender /\ (msgC' /= msgC)), which as my understanding means that if the send action is continuously enabled then it should eventually happen. But the state loop suggested other wise.
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+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at http://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout