Re: Stuttering state when fairness specified

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

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.