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

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

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,

Stephan

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

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

/\ Spec

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

Why?

On Wed, Apr 29, 2015 at 11:38 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:

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.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/BTqA3O-ipZo/unsubscribe.
To unsubscribe from this group and all its topics, 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.

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

--

Stephan Merz