Re: [tlaplus] Re: Stuttering state when fairness specified

[Stephan Merz <stepha...@xxxxxxxxx>]

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. 

Stephan

On 29 Apr 2015, at 20:31, Chen Fu <chen...@xxxxxxxxx> wrote:

Thank you both very much for going out of you way to help me. I may have downloaded the wrong version. can you give me a link?

But this does not look right to me.

In each and every one of those state 16, 17, 18,  action Rcv in the Receiver process is enabled because msgC is not empty. Based on my understanding of fairness, if the states always loop in 16, 17 and 18, that action should always be enabled thus eventually happen. Once that action happen it leads to msg=2, and then subsequently next=3, and then this would enable the action where the receiver send the ack 3 to the sender and the process should finish.

What I am trying to say is that each state of the above loop enables an action that leads to some other state outside of the loop. while if the process goes into that loop and stays there, the action would be always enabled but never happen. doesn't it violate fairness?

As in an message above I wrote a much smaller spec where a process keep adding an message to msgC, and I want to check whether msgC eventually becomes none empty  (<>(msgC /= <<>>) and TLC told me no, the trace reported is initial state followed by stuttering.

Can you help out?

Thanks!

--algorithm dum
{
  variables msgC = <<>>;
 
  fair process (Sender = "S")

     variables toSend = 0; ack = 0;
  {
    l_send:

      while (toSend < 1) {
              msgC := Append(msgC, toSend);
      }
  }
}

--
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.