Stuttering state when fairness specified

[Chen Fu]

Hi

I am trying to check livens of a spec. I specified "--fair algorithm", but TLC report that the state machine stopping at a Stuttering state, where one of the actions appears to be enabled. Could someone please help me find out what I did wrong?

a spec (below) describing a sender send a list of packets (0..(PckCount-1) to a receiver. The receiver send back ack for flow control.  msgC and ackC are two tuples simulating the network channels

I assign 10 to constant PckCount, TLC reports that after the following  state it goes to Stuttering

/\ toSend = 10

/\ pc = [S |-> "l_send", R |-> "Done"]

But this state, isn't action l_send enabled? and since (toSend < PckCount) is false, pc["S"] should change to "Done"? Does this mean Next is enabled? Why it stops at Stuttering given weak fairness is there?

Thanks!

CONSTANT PckCount
ASSUME PckCount \in Nat \ {0}

--fair algorithm simple
{
  variables msgC = <<>>; ackC = <<>>;
 
  macro Send(m, chan) {
      chan := Append(chan, m)
  }
 
  macro Rcv(v, chan) {
      await chan /= <<>>;
      v := Head(chan);
      chan := Tail(chan);
  }
 
  process (Sender = "S")
      variables toSend = 0; ack = 0;
  {
    l_send:
      while (toSend < PckCount) {
          either {
              Send(toSend, msgC);
          }
          or {
              Rcv(ack, ackC);
            l_depart:
              \* if ack received, send next two packets
              if (ack = (toSend + 1)) {
                  toSend := ack;
              }
          }
      }
  }
 
  process (Receiver = "R")
      variables next = 0; msg = 0;
  {
    l_rcv:
      while (next < PckCount) {
          either {
              Send(next, ackC);
          }
          or {
              Rcv(msg, msgC);
            l_accept:
              if (msg = next) {
                  next := next + 1 ;
              }
          }
      };
     
    l_finish_rcv:
      Send(next, ackC);
  }

}

[Leslie Lamport]

Dear Chen Fu,

First of all, the current release of TLC has a known bug that can
cause it to produce an incorrect error trace when it finds a (real)
error.  It's possible that you've triggered this bug.  The bug will be
fixed in the next release, which should be out in a week or two.

Meanwhile, I don't have enough information to understand what you are
doing.  For one thing, you never said what liveness property you were
checking.  However, I doubt that there is any sensible liveness
property satisfied by your algorithm.  And it generates an infinite
number of states, so I don't know you were trying to model check it.
For example, there is a behavior that consists of nothing but the
Sender executing an infinite sequence of Send actions.  If you had
added fairness conditions to each process instead of just to the
entire algorithm, there would still be behaviors that consist of
nothing but the Sender and Receiver both executing an infinite
sequence of Send actions.

I suspect that you don't understand fairness, and that you seem to
think there is some sort of fairness condition on the choices in an
either/or construct.  You should understand that the following
piece of code allows a behavior that loops forever, generating an
infinite number of different states:

  a: x := 1 ;
  b: while (x # 0) {
      either x := 0 
      or     x := x+1;
     }

You probably need to study the meaning of fairness, either from
the Hyperbook or Specifying Systems.

Leslie

[Chen Fu]

Is the next version 1.4.9? I tried to download it from https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/, same result.

This is a modification of the Alternating Bit Protocol, except the sender only has finite number of messages (PckCount) to send, and the channels (msgC, ackC) are reliable, they can not lose messages.

The liveness  condition is <>(pc["R"]="Done"); i.e. the Receiver eventually receives all messages and finishes

The model checker should not generate infinite number of states for this spec, all the state variables are bounded: All the integer variables are bounded by range 0..PckCount. PckCount is a constant, and I give it a value 10 to the model checker. I also tell the model checker to restrict the length of the two tuples (msgC and ackC) to 10. element of those two tuples can only be in 0..(PckCount-1).

[Leslie Lamport]

I'm sorry, I cannot see why the while loop in this process must
terminate.  (Or the corresponding one for the Receiver.)

   process (Sender = "S")
         variables toSend = 0; ack = 0;
     {
       l_send:
         while (toSend < PckCount) {
             either {
                 Send(toSend, msgC);
             }
             or {
                 Rcv(ack, ackC);
               l_depart:
                 \* if ack received, send next two packets
                 if (ack = (toSend + 1)) {
                     toSend := ack;
                 }
             }
         }
     }

Yes, the new version is 1.4.9.

[Chen Fu]

I tried to reduce the size of the spec but still keep the error, now the spec is

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

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

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

Temporal formula I am trying to check is <>(msgC /= <<>>)

The error trace given is initial state followed by stuttering.

[Stephan Merz]

I just ran your original spec with smaller parameters and constraints: PckCount = 3 and state constraint

   Len(msgC) <= 3 /\ Len(ackC) <= 3

The counter-example that I obtain (using a pre-release version of the Toolbox and TLC that avoids the bug that Leslie mentioned) does not end in stuttering, but in a loop shown in the attached screenshot. As you can see, the receiver process acks the value of "next", the sender receives this ack message but doesn't increment toSend because it expects to receive an acknowledgement message with value 3.

This appears to be a legitimate counter-example to the termination property. (I didn't investigate your spec any further.)

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Chen Fu]

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!

[Markus Alexander Kuppe]

On 29.04.2015 20:31, Chen Fu 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?

Hi Chen Fu,

the location for the (yet unreleased) 1.4.9 Toolbox is at
http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/

Markus

[Stephan Merz]

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

[Chen Fu]

Could you help me take a look at the simplified spec, which basically only has one action, and why <>(msgC /= <<>>) can not be verified?

Thanks!

[Chen Fu]

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?

--
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...@googlegroups.com.

[Stephan Merz]

Dear Chen Fu,

I fail to reproduce your problem with the simplified specification. For complete reference, the TLA+ module that I used is attached to this message. The (only) temporal property verified is 

  <>(msgC /= <<>>)

deadlock checking is off, and I added a state constraint

  Len(msgC) <= 3

(without this constraint, the model has an infinite state space and TLC will take a long time enumerating states; it may eventually do liveness checking on the partially constructed state space but I didn't have the patience to wait for this to happen). TLC tells me "No errors", for a model with 4 distinct states.

Regards,

Stephan

[Stephan Merz]

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

--

Stephan Merz

[Chen Fu]

Thank you very much for the detailed explanation. And yes this solved all my problems (so far :-)).  Really appreciate the help from all you guys.