Stuttering state when fairness specified

[Chen Fu <chen...@xxxxxxxxx>]

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);
  }

}