[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Stuttering state when fairness specified



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.