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