Your fairness condition is on the entire Next action, so it just requires that some transition happens for as long as some transition is enabled, and this is true of the counter-example that TLC gave me. The condition that you seem to have in mind is a stronger one where the receiver makes a fair choice between sending an ack and receiving a message. You can express such conditions in TLA and even in PlusCal if you add labels identifying the sub-actions of the non-deterministic choice (at the expense of more intermediate states). You might even choose to remove the choice for the receiver and only let it send an ack when it actually receives a message. Whatever you do should be guided by the protocol that you intend to model and the fairness properties that the actual system ensures.
On 29 Apr 2015, at 20:31, Chen Fu <chen...@xxxxxxxxx> wrote: