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