1


The service: Transfer of binary signals between two points
The service: the transfer of data over one hop with sufficient error and flow control for efficient operation of the Transport Layer (4)
The service: Routing and data transfer between network nodes.
End to end error and flow control
The Service: Connection and synchronisation of dialogues from the Presentation Layer
The control of information syntax and semantics between two applications.
Reference: . Holzmann, ``Design and Validation of Computer Protocols'', Prentice Hall, 1991, ISBN 0135399254: also available at http://cm.belllabs.com/cm/cs/what/spin/Doc/Book91.html
There are many different protocol modeling languages. In this course we shall initially use a simple statetransition language developed here at INRS and later, Holzmann's Promela/Spin system. Our simple system uses


Informal Protocol Specification

The ascii notation for specification of the FSMs is
/* This is the notation for a comment ... as in C qs 1 sets the length of the input queue to 1 qd b indicates that the other process blocks when the input queue is full */ fsm p_0(qd b,qs 1) { s_0>s_1 [/a:p_1]; s_0>s_2 [a/b:p_1]; s_1>s_2 [a/b:p_1]; s_1>s_2 [b/:]; } fsm p_1(qs 1,qd b) { s_0>s_1 [/a:p_0]; s_0>s_2 [a/b:p_0]; s_1>s_2 [a/b:p_0]; s_1>s_2 [b/:]; }
A multiprocess system evolves from an initial state by sending and receiving messages. It is essential that at least one processus be able to send a message from the initial state without the reception of message (why?). We call the system that is exchanging messages the ``composite system''. This system is also an FSM, but the state of the composite FSM is the ``explicit state'' (ie s_?) of each process plus the message sequence in each input queue. This composite state can be represented as a vector (cartesian product) of the individual process states.
To find the composite system,
This is guaranteed to converge if the number of explicit states in each process is finite and bounded, the number of different messages is finite and bounded, and each input queue is finite and bounded. What is the maximum number of states under these conditions? The reachable set of states may be as small as one or as large as the maximum number of states.
For this example, the initial state is {p_0:s_0(),p_1:s_0()}. In this state s_0, the transition s_0 > s_1 is executable, but the transition s_0 > s_2 is not executable. The same transition is executable in p_0 and p_1. The first two composite transitions are
{p_0:s_0(),p_1:s_0()}>{p_0:s_1(),p_1:s_0(a )} [p_0:/a:p_1]; {p_0:s_0(),p_1:s_0()}>{p_0:s_0(a ),p_1:s_1()} [p_1:/a:p_0];The new states are {p_0:s_1(),p_1:s_0(a )} et {p_0:s_0(a ),p_1:s_1()}. Note that {p_0:s_1(),p_1:s_0(a )} has two transitions which are executable in p_1:
{p_0:s_1(),p_1:s_0(a )}>{p_0:s_1(a ),p_1:s_1(a )} [p_1:/a:p_0]; {p_0:s_1(),p_1:s_0(a )}>{p_0:s_1(b ),p_1:s_2()} [p_1:a/b:p_0]; }
The complete composite system (p_0, p_1) is

The ascii notation for this system is
/* p_0 qs:1 qd:b  p_1 qs:1 qd:b  */ fsm comp(qs 1, qd r) { {p_0:s_0(),p_1:s_0()}>{p_0:s_1(),p_1:s_0(a )} [p_0:/a:p_1]; {p_0:s_0(),p_1:s_0()}>{p_0:s_0(a ),p_1:s_1()} [p_1:/a:p_0]; {p_0:s_0(a ),p_1:s_1()}>{p_0:s_1(a ),p_1:s_1(a )} [p_0:/a:p_1]; {p_0:s_0(a ),p_1:s_1()}>{p_0:s_2(),p_1:s_1(b )} [p_0:a/b:p_1]; {p_0:s_2(),p_1:s_1(b )}>{p_0:s_2(),p_1:s_2()} [p_1:b/:]; {p_0:s_1(),p_1:s_0(a )}>{p_0:s_1(a ),p_1:s_1(a )} [p_1:/a:p_0]; {p_0:s_1(),p_1:s_0(a )}>{p_0:s_1(b ),p_1:s_2()} [p_1:a/b:p_0]; {p_0:s_1(b ),p_1:s_2()}>{p_0:s_2(),p_1:s_2()} [p_0:b/:]; }
This model does not satisfy the specification  there are deadlock states
{p_0:s_1(a ),p_1:s_1(a )}  deadlock (why) {p_0:s_2(),p_1:s_1(b )}  deadlock (why) {p_0:s_1(b ),p_1:s_2()}  deadlock (why) }
An examination of the deadlock in Version I indicates that there needs to be a change to the model.

The composite system (p_0, p_1) is

This is not a solution.  why?
This is almost a solution but 
We add a read of b in s_2

The new composite system (p_0, p_1) is

Finally, a system that satisfies the specification.
This software computes the composite system from a specification and produces a series of encapsulated PostScript, *.eps files that can be viewed with Ghostview. It also computes several *.fsm files.
An example session
C:\temp>dir Volume in drive C has no label Volume Serial Number is 21511BD6 Directory of C:\temp . <DIR> 100400 4:07a . .. <DIR> 100400 4:07a .. FZ2B FSM 342 081699 10:31a fz2b.fsm 1 file(s) 342 bytes 2 dir(s) 862.45 MB free C:\temp>syscomp fz2b C:\temp>echo off Deadlock or Unspecified Reception  see .err file Number of states: 17 Unused transitions  see .err file Unused transitions  see .err file C:\temp>dir Volume in drive C has no label Volume Serial Number is 21511BD6 Directory of C:\temp . <DIR> 100400 4:07a . .. <DIR> 100400 4:07a .. FZ2B FSM 342 081699 10:31a fz2b.fsm FZ2B ERR 296 080901 7:46p fz2b.err FZ2B_I FSM 342 080901 7:46p fz2b_i.fsm FZ2B_C FSM 1,527 080901 7:46p fz2b_c.fsm FZ2B_0 EPS 7,573 080901 7:46p fz2b_0.eps FZ2B_1 EPS 7,573 080901 7:46p fz2b_1.eps FZ2B_V EPS 5,335 080901 7:46p fz2b_v.eps FZ2B_C EPS 17,093 080901 7:46p fz2b_c.eps 8 file(s) 40,081 bytes 2 dir(s) 858.40 MB free C:\temp>more fz2b.err States and deadlocked processes  fz2b.fsm p_0: qs:2 qd:b  p_1: qs:2 qd:b  "; Unspecified receptions and deadlocked processes: Complete deadlock: p_0  s_3  q: p_1  s_3  q: Nomber of States: 17 Unused transitions: p_0: s_2 > s_2 [a/:]; p_1: s_2 > s_2 [a/:]; ******** this state is a final state ********** ********* an example of a syntax error ************* C:\temp>ceng fz2b.fsm xxx s_1< parse error: LineNo: 5 Error snd_id: <p_1> in tr #: 0 Deadlock or Unspecified Reception  see .err file Number of states: 1 Unused transitions  see .err file C:\temp>ceng fz2b.fsm xxx s_1< parse error: LineNo: 5 Error snd_id: <p_1> in tr #: 0 Deadlock or Unspecified Reception  see .err file Number of states: 1 Unused transitions  see .err file C:\temp>more xxx_i.fsm fsm p_0(qd b,qs 2) { s_0>s_1 [/a:p_1]; s_0>s_2 [a/b:p_1 C:\temp>more fz2b.fsm fsm p_0(qd b,qs 2) { s_0>s_1 [/a:p_1]; s_0>s_2 [a/b:p_1 s_1>s_2 [a/b:p_1]; s_1>s_3 [b/b:p_1]; s_2>s_2 [a/:]; s_2>s_3 [b/b:p_1]; s_3>s_3 [b/:]; } fsm p_1(qs 2,qd b) { s_0>s_1 [/a:p_0]; s_0>s_2 [a/b:p_0]; s_1>s_2 [a/b:p_0]; s_1>s_3 [b/b:p_0]; s_2>s_2 [a/:]; s_2>s_3 [b/b:p_0]; s_3>s_3 [b/:]; }
The most general model of a communication channel between processes p_a and p_b use a process p_c for the channel.

/* an example of p_a > p_b with a channel */ fsm p_a (qs 1, qd b){ s0 > s1 [/a:p_c]; s1 > s1 [b/a:p_c]; } fsm p_c (qs 1, qd b){ s0>s0 [a/a:p_b]; s0>s0 [b/b:p_a]; } fsm p_b (qs 1, qd b){ s0 > s0 [a/b:p_c]; }
Note that the channel must have an explicit transition for each different message. The composite system is

Here there are 5 states.
In order to reduce the number of states, it is possible to have a direct connection between p_a and p_b as follows: ab.fsm:
/* an example of p_a > p_b */ fsm p_a (qs 1, qd b){ s0 > s1 [/a:p_b]; s1 > s1 [b/a:p_b]; } fsm p_b (qs 1, qd b){ s0 > s0 [a/b:p_a]; }
The composite system is

Now there are only three states  why?
Message Loss
The key to modeling message loss is to have a nondeterministic choice between two transitions. This will occur if there are two transitions leaving a state that are enabled by exactly the same event. In p_c, shown below, the reading of a message simultaneously enables two transitions, one where the reply message is sent and the appropriate state transition is made and the other where the message is read, the transition goes to the appropriate state but no message is sent. Since p_c only one state, this is the same state.

If we add the lossy channel to our system we get acbp.fsm,
/* an example of p_a > p_b ... perte dans le canal */ fsm p_a (qs 1, qd b){ s0 > s1 [/a:p_c]; s1 > s1 [b/a:p_c]; } fsm p_c (qs 1, qd b){ s0>s0 [a/a:p_b]; s0>s0 [b/b:p_a]; s0>s0 [a/:]; /* la perte de a */ s0>s0 [b/:]; /* la perte de b */ } fsm p_b (qs 1, qd b){ s0 > s0 [a/b:p_c]; }
The composite system is

Note that there is a new deadlock state and the previous 5 other states.
Since we are using nondeterministic transtions to model loss, we can just as easily include the loss in the original two processes. There are two possibilities for modeling the loss. The first is to have the transmitter send the message to the receiver and to have the receiver model the loss by reading the message and doing nothing. The second way is for the transmitter, after reading a message has two transitions to the same state, one which sends the appropriate message and the other that sends nothing. This latter method is preferred because messages that may be lost do not use up space in the receive queue.

The composite system is

Now there are a total of 4 states, one of which is a deadlock. This deadlock is a result of both processes waiting for a message that will never come.
Timers and Timeouts for lost messages
When a message is lost, the event that corresponds to its reception is also lost. The expiration of a timer resulting in a timeout message is designed to replace that lost event. If the message arrives before the timer expires, the timeout is cancelled. We model the cancellation by allowing the protected message to replace the timeout message in the input queue. This works well if there is only one message type, and the queue is of length 1. If either is false, more complicated modeling is required.
/* an example of a loss p_a <> p_b ... ( no transmission) */ /* add messages ta and tb coresponding to a timeout */ fsm p_a (qs 1, qd r){ s0 > s1 [/a:p_b,ta:p_a]; s0 > s1 [/ta:p_a]; /* loss a>b of first message */ s1 > s1 [b/a:p_b,ta:p_a]; s1 > s1 [b/ta:p_a]; /* loss a>b */ s1 > s1 [ta/a:p_b,ta:p_a]; s1 > s1 [ta/ta:p_a]; /* loss a>b */ } fsm p_b (qs 1, qd r){ s0 > s0 [a/b:p_a,tb:p_b]; s0 > s0 [a/tb:p_b]; /* loss b>a */ s0 > s0 [tb/b:p_a,tb:p_b]; s0 > s0 [tb/tb:p_b]; /* loss b>a */ }

In this chapter we will design a sequence of Data Link Protocols (DLP) for sending a stream of octets from a sender process Ps to a receiver process Pr over a lossy channel. This chapter will also introduce basic models and methods for proving the correctness of protocol systems. Future chapters will examine the mathematics in detail.
The key service requirement of the Data Link Protocol (DLP) is
In general data from L3 is put in L2 frames and delivered to L1. For L2, the unit of transmission is usually referred to as a ``frame''.
In general, there will be additional functional and performance requirements that surface as the design progresses. Some additional requirements for a DLP may be
Initially we will be concerned only with the correctness of the delivery of the data.
This gives us wide range of models, even for simple protocols. In this section we will introduce the complications slowly.
/* model 1 */ fsm Ps(qs 1, qd b) { s_d > s_a [/D:Pr]; s_a > s_d [A/:]; } fsm Pr(qs 1, qd b) { s_d > s_a [D/:]; s_a > s_d [/A:Ps]; }
This results in the two state diagrams

The composite system is

The use of a single data value D does not allow for the checking if there is a loss of a message, an error, or a change of order of the messages (why?). To do this we must use more complex data sequences. Ideally we need an infinite arbitrary sequence but in this chapter we will consider a much simpler sequence (D0,D1,D2,D0,D1,D2,...). This may be written using ``regular expressions'' as (D0 D1 D2)^{w}. We use the Dg to generate the sequence and Dr to receive the sequence. We will examine a series of models where the errorfree channel between the Dg and Dr becomes more and more complicated
In this case we have a direct connection between Dg and Dr where Dr has an input queue of size 1 (qs 1). The code is
/* L3  Model 1 */ fsm Dg(qs 1, qd b) { s0 > s1 [/D0:Dr]; s1 > s2 [/D1:Dr]; s2 > s0 [/D2:Dr]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; }
These two FSMs are identical to Dg and Dr in Model 2 except that Dg sends directly to Dr rather than to Ps. The composite system is

This is a nice simple single cycle which is quite similar to the single cycles of Dg and Dr themselves.
This model is identical to L31 except that the input queue is now of length 2. The composite system is

This is no longer a simple cycle. The (qs 2) queue of Dr allows different interleaving orders of Dg and Dr. In L31, there was only one order of execution of Dg and Dr, (Dg,Dr,Dg,Dr,...) but here there are an infinite number of different interleavings and hence sequences (why infinite?)
In this model we connect Dg and Dr by an ideal channel with (qs 1, qd b). When the channel input queue is full, it causes Dg to block
The code for L33 is
/* L3 with ideal channel */ fsm Dg(qs 1, qd b) { s0 > s1 [/D0:Ch]; s1 > s2 [/D1:Ch]; s2 > s0 [/D2:Ch]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ch(qs 1, qd b) { s_d > s_d [D0/D0:Dr]; s_d > s_d [D1/D1:Dr]; s_d > s_d [D2/D2:Dr]; }
The composite system is

Although this is similar to L32, the additional Ch process increases the interleaving again leading to a more complicated behaviour.
This model controls the flow between the channel and Dg via a poll. The channel is identical to that in L33 except for the extra state where it sends a Poll to Dg. The code for L34 is
/* L3 with ideal channel and Poll */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ch]; s1 > s2 [P/D1:Ch]; s2 > s0 [P/D2:Ch]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ch(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_0 [D0/D0:Dr]; s_d > s_0 [D1/D1:Dr]; s_d > s_0 [D2/D2:Dr]; }
The composite system is

The FSM code is
/* model 2 */ fsm Dg(qs 1, qd b) { s0 > s1 [/D0:Ps]; s1 > s2 [/D1:Ps]; s2 > s0 [/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_d > s_a [D0/D0:Pr]; s_d > s_a [D1/D1:Pr]; s_d > s_a [D2/D2:Pr]; s_a > s_d [A/:]; } fsm Pr(qs 1, qd b) { s_d > s_d [D0/D0:Dr,A:Ps]; s_d > s_d [D1/D1:Dr,A:Ps]; s_d > s_d [D2/D2:Dr,A:Ps]; } visible{Dg,Dr}
The expression ``visible{Dg,Dr}'' causes ``cfr'' to compute a homomorphic projection of the composite system that includes Dg, Dr, and a reduced version of the other processes that hides all internal messaging. Thus only messages sent from Ps and Pr to Dg and Dr are included. Messages exclusively between Ps and Pr are excluded. We will study the mathematics of transition homorphisms in future chapters.
The FSMs for the for Model 2 are


The composite system is

An examination of this system shows that there are several deadlock states. These states are also shown in m2.err.
States and deadlocked processes  m2.fsm Dg: qs:1 qd:b  Dr: qs:1 qd:b  Ps: qs:1 qd:b  Pr: qs:1 qd:b  "; Unspecified receptions and deadlocked processes: Unspecified reception: Ps Dg  s2  q: Dr  s2  q: D2 Ps  s_a  q: D1 Pr  s_d  q: D0 Unspecified reception: Ps Dg  s1  q: Dr  s2  q: Ps  s_a  q: D0 Pr  s_d  q: D2 Deadlock: the input buffers are full Dg  s1  q: Dr  s2  q: Ps  s_a  q: D0 Pr  s_d  q: D2 Unspecified reception: Ps Dg  s1  q: Dr  s1  q: D1 Ps  s_a  q: D0 Pr  s_d  q: D2 Unspecified reception: Ps Dg  s0  q: Dr  s1  q: Ps  s_a  q: D2 Pr  s_d  q: D1 Deadlock: the input buffers are full Dg  s0  q: Dr  s1  q: Ps  s_a  q: D2 Pr  s_d  q: D1 Unspecified reception: Ps Dg  s0  q: Dr  s0  q: D0 Ps  s_a  q: D2 Pr  s_d  q: D1 Unspecified reception: Ps Dg  s2  q: Dr  s0  q: Ps  s_a  q: D1 Pr  s_d  q: D0 Deadlock: the input buffers are full Dg  s2  q: Dr  s0  q: Ps  s_a  q: D1 Pr  s_d  q: D0 Nomber of States: 30 Unused transitions:
The deadlock states are also shown very clearly in the ``visible{Dg,Dr}''FSM.

Deadlock: the input buffers are full Dg  s2  q: Dr  s0  q: Ps  s_a  q: D1 Pr  s_d  q: D0
The reason for the deadlock states is that Dg fills the input queue of Ps with a new message and blocks the Ack from Pr. This is a classic problem in system design. A solution is to only allow Dg to send new data when Ps is ready for it. This is normally done with a Poll message from L2 to L3.
The modified system is
/* model 2  poll */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a [D0/D0:Pr]; s_d > s_a [D1/D1:Pr]; s_d > s_a [D2/D2:Pr]; s_a > s_d [A/P:Dg]; } fsm Pr(qs 1, qd b) { s_d > s_d [D0/D0:Dr,A:Ps]; s_d > s_d [D1/D1:Dr,A:Ps]; s_d > s_d [D2/D2:Dr,A:Ps]; } visible{Dg,Dr}
The FSMs for the system are


The composite system is

Even this very simple protocol is rather messy.
The visible system projection for Dg and Dr is

An examination of this diagram shows that it is identical to that of L34. this means that the environment of (Ps,Pr) is equivalent to an ideal channel with a Poll.
This model now adds channel errors with notification to the model. This done as follows:
/* model 31  poll  errors Ps > Pr with notification*/ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a [D0/D0:Pr]; s_d > s_a [D0/Err:Pr]; s_d > s_a [D1/D1:Pr]; s_d > s_a [D1/Err:Pr]; s_d > s_a [D2/D2:Pr]; s_d > s_a [D2/Err:Pr]; s_a > s_d [A/P:Dg]; } fsm Pr(qs 1, qd b) { s_d > s_d [D0/D0:Dr,A:Ps]; s_d > s_d [D1/D1:Dr,A:Ps]; s_d > s_d [D2/D2:Dr,A:Ps]; s_d > s_d [Err/NAK:Ps]; }
Each transmission, an ``error with notification'' requires a second transition with exactly the same initial and final states but Ps sends an Err message rather than the actual data. If there were an actual channel process in our model, the channel process would send the Err message.
The model of a channel ``error with notification'' is accomplished by having Ps send an Err message to Pr. Pr responds to the error by sending a NAK. The key question now is what Ps should do when it receives the NAK. The model above will deadlock when Ps receives a NAK because there is no transition that will accept a NAK. It is also clear that there is not enough information when Ps is in s_a to resend the last message. We need a separate waiting for an ack state for each message. The new system is as follows:
/* model 31  poll  Ps > Pr errors with notification*/ /* model 32  add response for Err in Ps */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a0 [D0/D0:Pr]; s_d > s_a0 [D0/Err:Pr]; s_d > s_a1 [D1/D1:Pr]; s_d > s_a1 [D1/Err:Pr]; s_d > s_a2 [D2/D2:Pr]; s_d > s_a2 [D2/Err:Pr]; s_a0 > s_d [A/P:Dg]; s_a0 > s_a0 [NAK/D0:Pr]; s_a0 > s_a0 [NAK/Err:Pr]; s_a1 > s_d [A/P:Dg]; s_a1 > s_a1 [NAK/D1:Pr]; s_a1 > s_a1 [NAK/Err:Pr]; s_a2 > s_d [A/P:Dg]; s_a2 > s_a2 [NAK/D2:Pr]; s_a2 > s_a2 [NAK/Err:Pr]; } fsm Pr(qs 1, qd b) { s_d > s_d [D0/D0:Dr,A:Ps]; s_d > s_d [D1/D1:Dr,A:Ps]; s_d > s_d [D2/D2:Dr,A:Ps]; s_d > s_d [Err/NAK:Ps]; }
This system violates the separation of layers because the control structure depends on data from Layer 3. The state diagram for the new Ps is

The composite system is

Although we split the s_a into s_a0, s_a1, s_a2, the composite system is very similar, and not too much more complicated than that of Model 2  ( why?)
The visible system projection for Dg and Dr is

A careful examination of this diagram shows that it is identical to that of L34. this means that the environment of (Ps,Pr) is equivalent to an ideal channel with a Poll. The potential liveness problems in the environment are hidden.
This model adds errors, with notification, in P_r > P_s. The new model is
/* model 41  errors with notifications Ps <> Pr treat Err as a NAK */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a0 [D0/D0:Pr]; s_d > s_a0 [D0/Err:Pr]; s_d > s_a1 [D1/D1:Pr]; s_d > s_a1 [D1/Err:Pr]; s_d > s_a2 [D2/D2:Pr]; s_d > s_a2 [D2/Err:Pr]; s_a0 > s_d [A/P:Dg]; s_a0 > s_a0 [NAK/D0:Pr]; s_a0 > s_a0 [NAK/Err:Pr]; s_a0 > s_a0 [Err/D0:Pr]; s_a0 > s_a0 [Err/Err:Pr]; s_a1 > s_d [A/P:Dg]; s_a1 > s_a1 [NAK/D1:Pr]; s_a1 > s_a1 [NAK/Err:Pr]; s_a1 > s_a1 [Err/D1:Pr]; s_a1 > s_a1 [Err/Err:Pr]; s_a2 > s_d [A/P:Dg]; s_a2 > s_a2 [NAK/D2:Pr]; s_a2 > s_a2 [NAK/Err:Pr]; s_a2 > s_a2 [Err/D2:Pr]; s_a2 > s_a2 [Err/Err:Pr]; } fsm Pr(qs 1, qd b) { s_d > s_d [D0/D0:Dr,A:Ps]; s_d > s_d [D0/D0:Dr,Err:Ps]; s_d > s_d [D1/D1:Dr,A:Ps]; s_d > s_d [D1/D1:Dr,Err:Ps]; s_d > s_d [D2/D2:Dr,A:Ps]; s_d > s_d [D2/D2:Dr,Err:Ps]; s_d > s_d [Err/NAK:Ps]; }
The composite system is

It is clear that the treatment of an Err as a NAK in Model 4 is an error. It is also clear that a message should only be repeated if a NAK is received for that message. This means that each different message needs its own NAK. Since we have 3 messages, we need NAK0, NAK1, and NAK2. Ps will resend a message only if it receives the appropriate NAK.
The new system is
/* model 51  errors with notifications Ps <> Pr add NAK0, NAK1, NAK2 for each data value */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a0 [D0/D0:Pr]; s_d > s_a0 [D0/Err:Pr]; s_d > s_a1 [D1/D1:Pr]; s_d > s_a1 [D1/Err:Pr]; s_d > s_a2 [D2/D2:Pr]; s_d > s_a2 [D2/Err:Pr]; s_a0 > s_d [A/P:Dg]; s_a0 > s_a0 [NAK0/D0:Pr]; s_a0 > s_a0 [NAK0/Err:Pr]; s_a0 > s_a0 [NAK1/Err:Pr]; s_a0 > s_a0 [NAK2/Err:Pr]; s_a0 > s_a0 [Err/Err:Pr]; s_a1 > s_d [A/P:Dg]; s_a1 > s_a1 [NAK1/D1:Pr]; s_a1 > s_a1 [NAK0/Err:Pr]; s_a1 > s_a1 [NAK1/Err:Pr]; s_a1 > s_a1 [NAK2/Err:Pr]; s_a1 > s_a1 [Err/Err:Pr]; s_a2 > s_d [A/P:Dg]; s_a2 > s_a2 [NAK2/D2:Pr]; s_a2 > s_a2 [NAK0/Err:Pr]; s_a2 > s_a2 [NAK1/Err:Pr]; s_a2 > s_a2 [NAK2/Err:Pr]; s_a2 > s_a2 [Err/Err:Pr]; } fsm Pr(qs 1, qd b) { s_d0 > s_d1 [D0/D0:Dr,A:Ps]; s_d0 > s_d1 [D0/D0:Dr,Err:Ps]; s_d1 > s_d2 [D1/D1:Dr,A:Ps]; s_d1 > s_d2 [D1/D1:Dr,Err:Ps]; s_d2 > s_d0 [D2/D2:Dr,A:Ps]; s_d2 > s_d0 [D2/D2:Dr,Err:Ps]; s_d0 > s_d0 [Err/NAK0:Ps]; s_d0 > s_d0 [Err/Err:Ps]; s_d1 > s_d1 [Err/NAK1:Ps]; s_d1 > s_d1 [Err/Err:Ps]; s_d2 > s_d2 [Err/NAK2:Ps]; s_d2 > s_d2 [Err/Err:Ps]; } visible{Dg,Dr}
Dg and Dr are unchanged from the other models. The new Ps and Pr are


The composite system is

The entry occurs when the transition s_d0 > s_d1 [D0/D0:Dr,Err:Ps] is executed. Since model M51 treats the Err as a NAK0, it resends D0, even though it has been already passed up to Dr. this causes Dr to deadlock, but Ps is expecting a NAK0 but it receives a NAK1 so it replies with an Err. When Pr receives the Err, it returns the NAK1 indicating that it is missing D1, and not D0. This a permanent livelock. The problem in the design is quite fundamental. When Pr receives an Err, it knows immediately that it is missing the next data message. Thus the NAKi that it sends is a NAK for Di, but more importantly, an ACK for all the messages before Di. Although this looks like a NAK protocol, when the channel gives errors with notification, it behaves like an ACK based protocol.
In addition to the livelock there are also several transitions that are not used.
The visible system projection for Dg and Dr is

An examination of this diagram shows that it is identical to that of L34. this means that the environment of (Ps,Pr) is equivalent to an ideal channel with a Poll. Unfortunately, the problems in the environment are hidden.
Model 52 treats the NAK(i+1) as an ACK for the previous data. The new system is
/* model 51  errors with notifications Ps <> Pr add NAK0, NAK1, NAK2 and remove s_a0 > s_a0 [NAK2..Err:Pr]; s_a1 > s_a1 [NAK0..Err:Pr]; s_a2 > s_a2 [NAK1..Err:Pr]; model 52  treat a NAK as an ACK */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_d [/P:Dg]; s_d > s_a0 [D0/D0:Pr]; s_d > s_a0 [D0/Err:Pr]; s_d > s_a1 [D1/D1:Pr]; s_d > s_a1 [D1/Err:Pr]; s_d > s_a2 [D2/D2:Pr]; s_d > s_a2 [D2/Err:Pr]; s_a0 > s_d [A/P:Dg]; s_a0 > s_d [NAK1/P:Dg]; /* comme un A */ s_a0 > s_a0 [NAK0/D0:Pr]; s_a0 > s_a0 [NAK0/Err:Pr]; s_a0 > s_a0 [Err/Err:Pr]; s_a1 > s_d [A/P:Dg]; s_a1 > s_d [NAK2/P:Dg]; /* comme un A */ s_a1 > s_a1 [NAK1/D1:Pr]; s_a1 > s_a1 [NAK1/Err:Pr]; s_a1 > s_a1 [Err/Err:Pr]; s_a2 > s_d [A/P:Dg]; s_a2 > s_d [NAK0/P:Dg]; /* comme un A */ s_a2 > s_a2 [NAK2/D2:Pr]; s_a2 > s_a2 [NAK2/Err:Pr]; s_a2 > s_a2 [Err/Err:Pr]; } fsm Pr(qs 1, qd b) { s_d0 > s_d1 [D0/D0:Dr,A:Ps]; s_d0 > s_d1 [D0/D0:Dr,Err:Ps]; s_d1 > s_d2 [D1/D1:Dr,A:Ps]; s_d1 > s_d2 [D1/D1:Dr,Err:Ps]; s_d2 > s_d0 [D2/D2:Dr,A:Ps]; s_d2 > s_d0 [D2/D2:Dr,Err:Ps]; s_d0 > s_d0 [Err/NAK0:Ps]; s_d0 > s_d0 [Err/Err:Ps]; s_d1 > s_d1 [Err/NAK1:Ps]; s_d1 > s_d1 [Err/Err:Ps]; s_d2 > s_d2 [Err/NAK2:Ps]; s_d2 > s_d2 [Err/Err:Ps]; } visible{Dg,Dr}
The composite system is

It is perhaps a little simpler to examine the visible{Dg,Dr} system. This is

This protocol is correct for errors with notification in both directions.
Although Model 5 was designed using NAKs, it is clear from the analysis that it works because the NAK acts as an acknowledgement of all the previous data frames. The reception of an Err immediately indicates that there is a missing frame. Model 5 also indicates that it is necessary to distinguish between NAKs in order to retransmit the correct data. In model 5 we used the value of the data frame, D0, D1, or D2 to create a corresponding NAK0, NAK1, and NAK2. This is a violation of the principle that data from higher layers cannot be used for control. In this model we imagine that the data is carried in a numbered frame. We will use two serial numbers N0 and N1. Thus there are 6 possible frames (N0 D0, N0 D1, N0 D2, N1 D0, N1 D1, N1 D2). We also will have two acknowledgements A0, and A1 corresponding to the serial numbers N0 and N1. An ack Ax means that the next expected serial number is Nx.
We will build the model slowly starting out with a system with no channel errors. We model the frame consisting of a serial number and data as two transmissions to Pr on the same transition. The queue of Pr is, of course, now of length 2 (qs 2, qd b). Pr reads the serial number N0 or N1 followed by a read of the data Dx. After reading the entire frame, it sends the data to Dr and the appropriate ack (A0 or A1) to Ps.
/* model 6 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 60 no errors */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_a0 [D0/N0:Pr,D0:Pr]; s_n0 > s_a0 [D1/N0:Pr,D1:Pr]; s_n0 > s_a0 [D2/N0:Pr,D2:Pr]; s_a0 > s_n1 [A1/P:Dg]; s_n1 > s_a1 [D0/N1:Pr,D0:Pr]; s_n1 > s_a1 [D1/N1:Pr,D1:Pr]; s_n1 > s_a1 [D2/N1:Pr,D2:Pr]; s_a1 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_d0 > s_n1 [D0/D0:Dr,A1:Ps]; s_d0 > s_n1 [D1/D1:Dr,A1:Ps]; s_d0 > s_n1 [D2/D2:Dr,A1:Ps]; s_n1 > s_d1 [N1/:]; s_d1 > s_n0 [D0/D0:Dr,A0:Ps]; s_d1 > s_n0 [D1/D1:Dr,A0:Ps]; s_d1 > s_n0 [D2/D2:Dr,A0:Ps]; } visible{Dg,Dr}
Dg and Dr are the same as in the previous models. The FSM diagram for Ps is

and for Pr is

These diagrams are really quite simple (essentially 4 states each) with the different data resulting in different transitions. This is much simpler than the corresponding Ps and Pr for the previous NAK based models.
The composite system is

An analysis of this diagram reveals there are no nonprogress cycles and there are no deadlocks. In general these diagrams are difficult to read. It is better to view the PostScript files at various resolutions using Ghostscript.
The visible{Dg,Dr} is

This is identical to the visible{Dg,Dr} diagrams of previous models. These two diagrams imply there are no errors.
This model introduces channel errors in exactly the same way as with Model 5.
/* model 6 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 60 no errors 61 Err Ps>Pr */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr]; s_n0 > s_a00 [D0/Err:Pr]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr]; s_n0 > s_a01 [D1/Err:Pr]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr]; s_n0 > s_a02 [D2/Err:Pr]; s_a00 > s_a00 [A0/N0:Pr,D0:Pr]; s_a00 > s_a00 [A0/Err:Pr]; s_a01 > s_a01 [A0/N0:Pr,D1:Pr]; s_a01 > s_a01 [A0/Err:Pr]; s_a02 > s_a02 [A0/N0:Pr,D2:Pr]; s_a02 > s_a02 [A0/Err:Pr]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr]; s_n1 > s_a10 [D0/Err:Pr]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr]; s_n1 > s_a11 [D1/Err:Pr]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr]; s_n1 > s_a12 [D2/Err:Pr]; s_a10 > s_a10 [A1/N1:Pr,D0:Pr]; s_a10 > s_a10 [A1/Err:Pr]; s_a11 > s_a11 [A1/N1:Pr,D1:Pr]; s_a11 > s_a11 [A1/Err:Pr]; s_a12 > s_a12 [A1/N1:Pr,D2:Pr]; s_a12 > s_a12 [A1/Err:Pr]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_n0 [Err/A0:Ps]; s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D1/A1:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_n1 [Err/A1:Ps]; s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; } visible{Dg,Dr}
The major difference in the Pr in model 6 versus Model 5 is that a frame without error requires two read operations by Pr whereas an Err frame requires only one.
The FSM diagrams for Ps and Pr are


The composite system is

Again an examination, and m61.err, indicates that there are no deadlock states. The only nonprogress cycles have continual errors in the channel. This is an ``acceptable'' nonprogress cycle.
Again the visible{Dg,Dr} is the same as L34 indicating the specification is satisfied.

In this model we add errors in the Pr > Ps channel. In Ps we treat the reception of an error as being the same as receiving an incorrect Ax in the state.
/* model 6 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 60 no errors 61 Err Ps>Pr 62 Err Ps<>Pr */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr]; s_n0 > s_a00 [D0/Err:Pr]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr]; s_n0 > s_a01 [D1/Err:Pr]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr]; s_n0 > s_a02 [D2/Err:Pr]; s_a00 > s_a00 [A0/N0:Pr,D0:Pr]; s_a00 > s_a00 [A0/Err:Pr]; s_a00 > s_a00 [Err/N0:Pr,D0:Pr]; /* same effect as A0 */ s_a00 > s_a00 [Err/Err:Pr]; s_a01 > s_a01 [A0/N0:Pr,D1:Pr]; s_a01 > s_a01 [Err/N0:Pr,D1:Pr]; s_a01 > s_a01 [A0/Err:Pr]; s_a01 > s_a01 [Err/Err:Pr]; s_a02 > s_a02 [A0/N0:Pr,D2:Pr]; s_a02 > s_a02 [Err/N0:Pr,D2:Pr]; s_a02 > s_a02 [A0/Err:Pr]; s_a02 > s_a02 [Err/Err:Pr]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr]; s_n1 > s_a10 [D0/Err:Pr]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr]; s_n1 > s_a11 [D1/Err:Pr]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr]; s_n1 > s_a12 [D2/Err:Pr]; s_a10 > s_a10 [A1/N1:Pr,D0:Pr]; s_a10 > s_a10 [Err/N1:Pr,D0:Pr]; s_a10 > s_a10 [A1/Err:Pr]; s_a10 > s_a10 [Err/Err:Pr]; s_a11 > s_a11 [A1/N1:Pr,D1:Pr]; s_a11 > s_a11 [Err/N1:Pr,D1:Pr]; s_a11 > s_a11 [A1/Err:Pr]; s_a11 > s_a11 [Err/Err:Pr]; s_a12 > s_a12 [A1/N1:Pr,D2:Pr]; s_a12 > s_a12 [Err/N1:Pr,D2:Pr]; s_a12 > s_a12 [A1/Err:Pr]; s_a12 > s_a12 [Err/Err:Pr]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_n0 [Err/A0:Ps]; s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D0/Err:Ps,D0:Dr]; s_d0 > s_n1 [D1/Err:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_d0 > s_n1 [D2/Err:Ps,D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_n1 [Err/A1:Ps]; s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D0/Err:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D1/Err:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; s_d1 > s_n0 [D2/Err:Ps,D2:Dr]; } visible{Dg,Dr}
The FSM diagrams for Ps and Pr are


The composite system is

m62.err indicates that there are deadlock states.
States and deadlocked processes  m62.fsm Dg: qs:1 qd:b  Dr: qs:1 qd:b  Ps: qs:1 qd:b  Pr: qs:2 qd:b  "; Unspecified receptions and deadlocked processes: Unspecified reception: Pr Dg  s0  q: Dr  s2  q: D2 Ps  s_a12  q: Pr  s_n0  q: N1 D2 Complete deadlock: Unspecified reception: Pr Dg  s0  q: Dr  s0  q: Ps  s_a12  q: Pr  s_n0  q: N1 D2 Unspecified reception: Pr Dg  s2  q: Dr  s1  q: D1 Ps  s_a01  q: Pr  s_n1  q: N0 D1 Complete deadlock: Unspecified reception: Pr Dg  s2  q: Dr  s2  q: Ps  s_a01  q: Pr  s_n1  q: N0 D1 Unspecified reception: Pr Dg  s1  q: Dr  s0  q: D0 Ps  s_a10  q: Pr  s_n0  q: N1 D0 Complete deadlock: Unspecified reception: Pr Dg  s1  q: Dr  s1  q: Ps  s_a10  q: Pr  s_n0  q: N1 D0 Unspecified reception: Pr Dg  s0  q: Dr  s2  q: D2 Ps  s_a02  q: Pr  s_n1  q: N0 D2 Complete deadlock: Unspecified reception: Pr Dg  s0  q: Dr  s0  q: Ps  s_a02  q: Pr  s_n1  q: N0 D2 Unspecified reception: Pr Dg  s2  q: Dr  s1  q: D1 Ps  s_a11  q: Pr  s_n0  q: N1 D1 Complete deadlock: Unspecified reception: Pr Dg  s2  q: Dr  s2  q: Ps  s_a11  q: Pr  s_n0  q: N1 D1 Unspecified reception: Pr Dg  s1  q: Dr  s0  q: D0 Ps  s_a00  q: Pr  s_n1  q: N0 D0 Complete deadlock: Unspecified reception: Pr Dg  s1  q: Dr  s1  q: Ps  s_a00  q: Pr  s_n1  q: N0 D0 Nomber of States: 121 Unused transitions:
All processes except Pr have empty queues and the state of Pr is s_n1 (N0 D0). This state is reached by an Err in the Pr/Ps channel followed by the reception of reception of (N0 D0) by Pr after Ps treats the Err as the wrong Ack. This is clearly a duplicate at Pr and should be rejected. In Model 5, we had a similar problem and decided to solve it by having Ps send an Err when it received an Err. This is not an entirely satisfactory solution because it actually adds Err as a symbol in the alphabet.
Again the visible{Dg,Dr} is the same as L34 indicating the specification is satisfied when there is no deadlock  not an entirely satisfactory method of satisfying the specification.

/* model 6 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 60 no errors 61 Err Ps>Pr 62 Err Ps<>Pr 63 Treat N0 in s_n1 as a duplicate */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 1, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr]; s_n0 > s_a00 [D0/Err:Pr]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr]; s_n0 > s_a01 [D1/Err:Pr]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr]; s_n0 > s_a02 [D2/Err:Pr]; s_a00 > s_a00 [A0/N0:Pr,D0:Pr]; s_a00 > s_a00 [A0/Err:Pr]; s_a00 > s_a00 [Err/N0:Pr,D0:Pr]; s_a00 > s_a00 [Err/Err:Pr]; s_a01 > s_a01 [A0/N0:Pr,D1:Pr]; s_a01 > s_a01 [Err/N0:Pr,D1:Pr]; s_a01 > s_a01 [A0/Err:Pr]; s_a01 > s_a01 [Err/Err:Pr]; s_a02 > s_a02 [A0/N0:Pr,D2:Pr]; s_a02 > s_a02 [Err/N0:Pr,D2:Pr]; s_a02 > s_a02 [A0/Err:Pr]; s_a02 > s_a02 [Err/Err:Pr]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr]; s_n1 > s_a10 [D0/Err:Pr]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr]; s_n1 > s_a11 [D1/Err:Pr]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr]; s_n1 > s_a12 [D2/Err:Pr]; s_a10 > s_a10 [A1/N1:Pr,D0:Pr]; s_a10 > s_a10 [Err/N1:Pr,D0:Pr]; s_a10 > s_a10 [A1/Err:Pr]; s_a10 > s_a10 [Err/Err:Pr]; s_a11 > s_a11 [A1/N1:Pr,D1:Pr]; s_a11 > s_a11 [Err/N1:Pr,D1:Pr]; s_a11 > s_a11 [A1/Err:Pr]; s_a11 > s_a11 [Err/Err:Pr]; s_a12 > s_a12 [A1/N1:Pr,D2:Pr]; s_a12 > s_a12 [Err/N1:Pr,D2:Pr]; s_a12 > s_a12 [A1/Err:Pr]; s_a12 > s_a12 [Err/Err:Pr]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_n0 [Err/A0:Ps]; s_n0 > s_n0 [Err/Err:Ps]; s_n0 > s_d0x [N1/:]; /* m63  reject as duplicate*/ s_d0x > s_n0 [D0/A0:Ps]; /* m63 */ s_d0x > s_n0 [D0/Err:Ps]; /* m63 */ s_d0x > s_n0 [D1/A0:Ps]; /* m63 */ s_d0x > s_n0 [D1/Err:Ps]; /* m63 */ s_d0x > s_n0 [D2/A0:Ps]; /* m63 */ s_d0x > s_n0 [D2/Err:Ps]; /* m63 */ s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D0/Err:Ps,D0:Dr]; s_d0 > s_n1 [D1/Err:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_d0 > s_n1 [D2/Err:Ps,D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_n1 [Err/A1:Ps]; s_n1 > s_n1 [Err/Err:Ps]; s_n1 > s_d1x [N0/:]; /* m63 */ s_d1x > s_n1 [D0/A1:Ps]; /* m63 */ s_d1x > s_n1 [D0/Err:Ps]; /* m63 */ s_d1x > s_n1 [D1/A1:Ps]; /* m63 */ s_d1x > s_n1 [D1/Err:Ps]; /* m63 */ s_d1x > s_n1 [D2/A1:Ps]; /* m63 */ s_d1x > s_n1 [D2/Err:Ps]; /* m63 */ s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D0/Err:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D1/Err:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; s_d1 > s_n0 [D2/Err:Ps,D2:Dr]; } visible{Dg,Dr}
The FSM diagrams for Ps and Pr are


The composite system is

The composite system has no deadlocks and the only livelocks are continual losses in the channel.
Again the visible{Dg,Dr} is the same as L34 indicating the specification is satisfied.

In this model the channel errors are without any notification. This means that we must replace a lost message by another event, the expiration of a timer. Each type of message must have its own timeout. This means we have T0 for N0 Dx frames and T1 for N1 Dx frames. Every message sent is protected by a Tx. We put the Tx into the input queue of Ps. Since we cannot afford to block the incoming Ack, the input queue is increased to (qs 2, qd b). Only Ps is protected by timeouts.
We start with the model M63 with duplicate rejection. We remove all the errors in the Pr > Ps direction and all reception of Err messages. In general Err send messages are replaced by a null send :. Because every sent message puts a Tx in Ps's input queue, it is possible for the Tx messages to be received in the wrong state. In these states they are read with no action. It is also possible that acks, Ax are received in the wrong state. If so, they are ignored. The new model is
/* model 7 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 71 Errors without notification Ps>Pr  use timeouts and messages T0, T1 */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 2, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_n0 [T1/:]; s_n0 > s_n0 [A0/:]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr,T0:Ps]; s_n0 > s_a00 [D0/T0:Ps]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr,T0:Ps]; s_n0 > s_a01 [D1/T0:Ps]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr,T0:Ps]; s_n0 > s_a02 [D2/T0:Ps]; s_a00 > s_a00 [T0/N0:Pr,D0:Pr,T0:Ps]; s_a00 > s_a00 [T0/T0:Ps]; s_a00 > s_a00 [A0/:]; s_a01 > s_a01 [T0/N0:Pr,D1:Pr,T0:Ps]; s_a01 > s_a01 [T0/T0:Ps]; s_a01 > s_a01 [A0/:]; s_a02 > s_a02 [T0/N0:Pr,D2:Pr,T0:Ps]; s_a02 > s_a02 [T0/T0:Ps]; s_a02 > s_a02 [A0/:]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_n1 [T0/:]; s_n1 > s_n1 [A1/:]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr,T1:Ps]; s_n1 > s_a10 [D0/T1:Ps]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr,T1:Ps]; s_n1 > s_a11 [D1/T1:Ps]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr,T1:Ps]; s_n1 > s_a12 [D2/T1:Ps]; s_a10 > s_a10 [T1/N1:Pr,D0:Pr,T1:Ps]; s_a10 > s_a10 [T1/T1:Ps]; s_a10 > s_a10 [A1/:]; s_a11 > s_a11 [T1/N1:Pr,D1:Pr,T1:Ps]; s_a11 > s_a11 [T1/T1:Ps]; s_a11 > s_a11 [A1/:]; s_a12 > s_a12 [T1/N1:Pr,D2:Pr,T1:Ps]; s_a12 > s_a12 [T1/T1:Ps]; s_a12 > s_a12 [A1/:]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_d0x [N1/:]; s_d0x > s_n0 [D0/A0:Ps]; s_d0x > s_n0 [D1/A0:Ps]; s_d0x > s_n0 [D2/A0:Ps]; s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D1/A1:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_d1x [N0/:]; s_d1x > s_n1 [D0/A1:Ps]; s_d1x > s_n1 [D1/A1:Ps]; s_d1x > s_n1 [D2/A1:Ps]; s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; } visible{Dg,Dr}
Although this model was derived from M63, the fact that Ax could arrive at several other states was not immediately obvious. This was determined from examining the composite system of several preliminary trials.
The FSM diagrams for Ps and Pr are


The composite system is

The composite system has no deadlocks and the only livelocks are continual losses in the channel.
Again the visible{Dg,Dr} is the same as L34 indicating the specification is satisfied.

The only change in 72 from 71 was to add the loss in the return channel. Ps was unchanged.
/* model 7 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 71 Errors without notification Ps>Pr  use timeouts and messages T0, T1 72 Plus errors Pr > Ps */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 2, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_n0 [T1/:]; s_n0 > s_n0 [A0/:]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr,T0:Ps]; s_n0 > s_a00 [D0/T0:Ps]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr,T0:Ps]; s_n0 > s_a01 [D1/T0:Ps]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr,T0:Ps]; s_n0 > s_a02 [D2/T0:Ps]; s_a00 > s_a00 [T0/N0:Pr,D0:Pr,T0:Ps]; s_a00 > s_a00 [T0/T0:Ps]; s_a00 > s_a00 [A0/:]; s_a01 > s_a01 [T0/N0:Pr,D1:Pr,T0:Ps]; s_a01 > s_a01 [T0/T0:Ps]; s_a01 > s_a01 [A0/:]; s_a02 > s_a02 [T0/N0:Pr,D2:Pr,T0:Ps]; s_a02 > s_a02 [T0/T0:Ps]; s_a02 > s_a02 [A0/:]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_n1 [T0/:]; s_n1 > s_n1 [A1/:]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr,T1:Ps]; s_n1 > s_a10 [D0/T1:Ps]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr,T1:Ps]; s_n1 > s_a11 [D1/T1:Ps]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr,T1:Ps]; s_n1 > s_a12 [D2/T1:Ps]; s_a10 > s_a10 [T1/N1:Pr,D0:Pr,T1:Ps]; s_a10 > s_a10 [T1/T1:Ps]; s_a10 > s_a10 [A1/:]; s_a11 > s_a11 [T1/N1:Pr,D1:Pr,T1:Ps]; s_a11 > s_a11 [T1/T1:Ps]; s_a11 > s_a11 [A1/:]; s_a12 > s_a12 [T1/N1:Pr,D2:Pr,T1:Ps]; s_a12 > s_a12 [T1/T1:Ps]; s_a12 > s_a12 [A1/:]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_d0x [N1/:]; s_d0x > s_n0 [D0/A0:Ps]; s_d0x > s_n0 [D1/A0:Ps]; s_d0x > s_n0 [D2/A0:Ps]; s_d0x > s_n0 [D0/:]; s_d0x > s_n0 [D1/:]; s_d0x > s_n0 [D2/:]; s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D1/A1:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_d0 > s_n1 [D0/D0:Dr]; s_d0 > s_n1 [D1/D1:Dr]; s_d0 > s_n1 [D2/D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_d1x [N0/:]; s_d1x > s_n1 [D0/A1:Ps]; s_d1x > s_n1 [D1/A1:Ps]; s_d1x > s_n1 [D2/A1:Ps]; s_d1x > s_n1 [D0/:]; s_d1x > s_n1 [D1/:]; s_d1x > s_n1 [D2/:]; s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; s_d1 > s_n0 [D0/D0:Dr]; s_d1 > s_n0 [D1/D1:Dr]; s_d1 > s_n0 [D2/D2:Dr]; } visible{Dg,Dr}
The FSM diagrams for Ps and Pr are


The composite system is

The composite system has no deadlocks and the only livelocks are continual losses in the channel.
Again the visible{Dg,Dr} is the same as L34 indicating the specification is satisfied.

This chapter will be a introduction to Holzmann's modeling language ``Promela'' and its analytic engine ``Spin''. This chapter is a really a list of pointers to tutorial and analytical information on Promela, Spin. We will be discussing these sources in class. In addition, the software m2p which translates an FSM model in our language to Promela. We will discuss this translation because it indicates the importance of accounting for slightly different semantics in modeling languages.
The url for Spin home page is http://netlib.belllabs.com/cm/cs/what/spin/index.html
This has all the links to the online documentation for Promela/Spin. It It also has links for installing Spin/Xspin on your PC http://cm.belllabs.com/cm/cs/what/spin/Man/README.html#S1. It is essential that you install it on your own PC or have access to it from a workstation at INRS or your local university.
The Spin Online References page,
http://cm.belllabs.com/cm/cs/what/spin/Man/index.html, has several tutorial articles on Promela and Spin:
In addition, there is detailed information on the
The basic aspects of the conversion is as follows:
The program m2p converts our FSM notation to Promela. An example, using the last model, m72.fsm for the Alternating Bit Protocol is as follows:
An example session is C:\TEMP>dir Volume in drive C is MJF98 Serial number is 1237:10D1 Directory of C:\TEMP\* 100499 7:46 <DIR> . 100499 7:46 <DIR> .. 12600 10:39 2,811 M72.fsm 2,811 bytes in 1 file and 2 dirs 4,096 bytes allocated 1,400,291,328 bytes free C:\TEMP>m2p M72.fsm m72 C:\TEMP>dir Volume in drive C is MJF98 Serial number is 1237:10D1 Directory of C:\TEMP\* 100499 7:46 <DIR> . 100499 7:46 <DIR> .. 12600 10:39 2,811 M72.fsm 21000 10:52 4,593 m72.log 21000 10:52 7,282 m72.prm 21000 10:52 214 m72_0.dot 21000 10:52 211 m72_1.dot 21000 10:52 1,767 m72_2.dot 21000 10:52 1,185 m72_3.dot 21000 10:52 2,114 m72_i.fsm 20,177 bytes in 8 files and 2 dirs 40,960 bytes allocated 1,400,254,464 bytes free  Comments: ** The M72_?.dot files are the FSMs for the four input FSMs in m72.fsm ** the m72.log is a debug log file ** the m72.prm is the converted file  The original m72.fsm file is  /* model 7 ... a frame from Ps > Pr is (N? D?) where N? is N0 or N1 (sequence number) and D? is D0 D1 D2 (data values) ... a frame from Pr > Ps is A0 or A1 where Ax, x is the next sequence number, in order 71 Errors without notification Ps>Pr  use timeouts and messages T0, T1 72 Plus errors Pr > Ps */ fsm Dg(qs 1, qd b) { s0 > s1 [P/D0:Ps]; s1 > s2 [P/D1:Ps]; s2 > s0 [P/D2:Ps]; } fsm Dr(qs 1, qd b) { s0 > s1 [D0/:]; s1 > s2 [D1/:]; s2 > s0 [D2/:]; } fsm Ps(qs 2, qd b) { s_0 > s_n0 [/P:Dg]; s_n0 > s_n0 [T1/:]; s_n0 > s_n0 [A0/:]; s_n0 > s_a00 [D0/N0:Pr,D0:Pr,T0:Ps]; s_n0 > s_a00 [D0/T0:Ps]; s_n0 > s_a01 [D1/N0:Pr,D1:Pr,T0:Ps]; s_n0 > s_a01 [D1/T0:Ps]; s_n0 > s_a02 [D2/N0:Pr,D2:Pr,T0:Ps]; s_n0 > s_a02 [D2/T0:Ps]; s_a00 > s_a00 [T0/N0:Pr,D0:Pr,T0:Ps]; s_a00 > s_a00 [T0/T0:Ps]; s_a00 > s_a00 [A0/:]; s_a01 > s_a01 [T0/N0:Pr,D1:Pr,T0:Ps]; s_a01 > s_a01 [T0/T0:Ps]; s_a01 > s_a01 [A0/:]; s_a02 > s_a02 [T0/N0:Pr,D2:Pr,T0:Ps]; s_a02 > s_a02 [T0/T0:Ps]; s_a02 > s_a02 [A0/:]; s_a00 > s_n1 [A1/P:Dg]; s_a01 > s_n1 [A1/P:Dg]; s_a02 > s_n1 [A1/P:Dg]; s_n1 > s_n1 [T0/:]; s_n1 > s_n1 [A1/:]; s_n1 > s_a10 [D0/N1:Pr,D0:Pr,T1:Ps]; s_n1 > s_a10 [D0/T1:Ps]; s_n1 > s_a11 [D1/N1:Pr,D1:Pr,T1:Ps]; s_n1 > s_a11 [D1/T1:Ps]; s_n1 > s_a12 [D2/N1:Pr,D2:Pr,T1:Ps]; s_n1 > s_a12 [D2/T1:Ps]; s_a10 > s_a10 [T1/N1:Pr,D0:Pr,T1:Ps]; s_a10 > s_a10 [T1/T1:Ps]; s_a10 > s_a10 [A1/:]; s_a11 > s_a11 [T1/N1:Pr,D1:Pr,T1:Ps]; s_a11 > s_a11 [T1/T1:Ps]; s_a11 > s_a11 [A1/:]; s_a12 > s_a12 [T1/N1:Pr,D2:Pr,T1:Ps]; s_a12 > s_a12 [T1/T1:Ps]; s_a12 > s_a12 [A1/:]; s_a10 > s_n0 [A0/P:Dg]; s_a11 > s_n0 [A0/P:Dg]; s_a12 > s_n0 [A0/P:Dg]; } fsm Pr(qs 2, qd b) { s_n0 > s_d0 [N0/:]; s_n0 > s_d0x [N1/:]; s_d0x > s_n0 [D0/A0:Ps]; s_d0x > s_n0 [D1/A0:Ps]; s_d0x > s_n0 [D2/A0:Ps]; s_d0x > s_n0 [D0/:]; s_d0x > s_n0 [D1/:]; s_d0x > s_n0 [D2/:]; s_d0 > s_n1 [D0/A1:Ps,D0:Dr]; s_d0 > s_n1 [D1/A1:Ps,D1:Dr]; s_d0 > s_n1 [D2/A1:Ps,D2:Dr]; s_d0 > s_n1 [D0/D0:Dr]; s_d0 > s_n1 [D1/D1:Dr]; s_d0 > s_n1 [D2/D2:Dr]; s_n1 > s_d1 [N1/:]; s_n1 > s_d1x [N0/:]; s_d1x > s_n1 [D0/A1:Ps]; s_d1x > s_n1 [D1/A1:Ps]; s_d1x > s_n1 [D2/A1:Ps]; s_d1x > s_n1 [D0/:]; s_d1x > s_n1 [D1/:]; s_d1x > s_n1 [D2/:]; s_d1 > s_n0 [D0/A0:Ps,D0:Dr]; s_d1 > s_n0 [D1/A0:Ps,D1:Dr]; s_d1 > s_n0 [D2/A0:Ps,D2:Dr]; s_d1 > s_n0 [D0/D0:Dr]; s_d1 > s_n0 [D1/D1:Dr]; s_d1 > s_n0 [D2/D2:Dr]; } visible{Dg,Dr}  The converted file is m72.prm  /* Conversion FSM file, {\em M72.FSM}, to Promela {\em m72.prm}*/ mtype= { P, D0, D1, D2, T1, A0, N0, T0, A1, N1 }; chan Dg_chan=[1] of {mtype}; chan Dr_chan=[1] of {mtype}; chan Ps_chan=[2] of {mtype}; chan Pr_chan=[2] of {mtype}; proctype Dg () { s0: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!D0; goto s1} s1: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!D1; goto s2} s2: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!D2; goto s0} } proctype Dr () { s0: atomic{(Dr_chan?[D0]) > Dr_chan?D0; > goto s1} s1: atomic{(Dr_chan?[D1]) > Dr_chan?D1; > goto s2} s2: atomic{(Dr_chan?[D2]) > Dr_chan?D2; > goto s0} } proctype Ps () { s_0: atomic{( (len(Dg_chan) <= 0)) > Dg_chan!P; goto s_n0} s_n0: if :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; > goto s_n0} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; > goto s_n0} :: atomic{(Ps_chan?[D0] && (len(Pr_chan) <= 0)) > Ps_chan?D0; Pr_chan!N0; Pr_chan!D0; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[D0]) > Ps_chan?D0; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[D1] && (len(Pr_chan) <= 0)) > Ps_chan?D1; Pr_chan!N0; Pr_chan!D1; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[D1]) > Ps_chan?D1; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[D2] && (len(Pr_chan) <= 0)) > Ps_chan?D2; Pr_chan!N0; Pr_chan!D2; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[D2]) > Ps_chan?D2; Ps_chan!T0; goto s_a02} fi; s_a00: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!D0; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; > goto s_a00} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_a01: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!D1; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; > goto s_a01} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_a02: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!D2; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; > goto s_a02} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_n1: if :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; > goto s_n1} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; > goto s_n1} :: atomic{(Ps_chan?[D0] && (len(Pr_chan) <= 0)) > Ps_chan?D0; Pr_chan!N1; Pr_chan!D0; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[D0]) > Ps_chan?D0; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[D1] && (len(Pr_chan) <= 0)) > Ps_chan?D1; Pr_chan!N1; Pr_chan!D1; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[D1]) > Ps_chan?D1; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[D2] && (len(Pr_chan) <= 0)) > Ps_chan?D2; Pr_chan!N1; Pr_chan!D2; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[D2]) > Ps_chan?D2; Ps_chan!T1; goto s_a12} fi; s_a10: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!D0; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; > goto s_a10} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; s_a11: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!D1; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; > goto s_a11} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; s_a12: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!D2; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; > goto s_a12} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; } proctype Pr () { s_n0: if :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; > goto s_d0} :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; > goto s_d0x} fi; s_d0x: if :: atomic{(Pr_chan?[D0] && (len(Ps_chan) <= 1)) > Pr_chan?D0; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[D1] && (len(Ps_chan) <= 1)) > Pr_chan?D1; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[D2] && (len(Ps_chan) <= 1)) > Pr_chan?D2; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[D0]) > Pr_chan?D0; > goto s_n0} :: atomic{(Pr_chan?[D1]) > Pr_chan?D1; > goto s_n0} :: atomic{(Pr_chan?[D2]) > Pr_chan?D2; > goto s_n0} fi; s_d0: if :: atomic{(Pr_chan?[D0] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D0; Ps_chan!A1; Dr_chan!D0; goto s_n1} :: atomic{(Pr_chan?[D1] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D1; Ps_chan!A1; Dr_chan!D1; goto s_n1} :: atomic{(Pr_chan?[D2] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D2; Ps_chan!A1; Dr_chan!D2; goto s_n1} :: atomic{(Pr_chan?[D0] && (len(Dr_chan) <= 0)) > Pr_chan?D0; > goto s_n1} :: atomic{(Pr_chan?[D1] && (len(Dr_chan) <= 0)) > Pr_chan?D1; > goto s_n1} :: atomic{(Pr_chan?[D2] && (len(Dr_chan) <= 0)) > Pr_chan?D2; > goto s_n1} fi; s_n1: if :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; > goto s_d1} :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; > goto s_d1x} fi; s_d1x: if :: atomic{(Pr_chan?[D0] && (len(Ps_chan) <= 1)) > Pr_chan?D0; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[D1] && (len(Ps_chan) <= 1)) > Pr_chan?D1; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[D2] && (len(Ps_chan) <= 1)) > Pr_chan?D2; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[D0]) > Pr_chan?D0; > goto s_n1} :: atomic{(Pr_chan?[D1]) > Pr_chan?D1; > goto s_n1} :: atomic{(Pr_chan?[D2]) > Pr_chan?D2; > goto s_n1} fi; s_d1: if :: atomic{(Pr_chan?[D0] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D0; Ps_chan!A0; Dr_chan!D0; goto s_n0} :: atomic{(Pr_chan?[D1] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D1; Ps_chan!A0; Dr_chan!D1; goto s_n0} :: atomic{(Pr_chan?[D2] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?D2; Ps_chan!A0; Dr_chan!D2; goto s_n0} :: atomic{(Pr_chan?[D0] && (len(Dr_chan) <= 0)) > Pr_chan?D0; > goto s_n0} :: atomic{(Pr_chan?[D1] && (len(Dr_chan) <= 0)) > Pr_chan?D1; > goto s_n0} :: atomic{(Pr_chan?[D2] && (len(Dr_chan) <= 0)) > Pr_chan?D2; > goto s_n0} fi; } init{ atomic{run Dg(); run Dr(); run Ps(); run Pr(); }} 
This chapter will discuss methods and models for describing and testing correctness properties  safety, liveness, and satisfaction of the specification. To describe liveness properties and satisfaction of specifications, it will introduce regular and wregular languages, linear temporal logic, and the finite state machines (automata) to represent them. The discussion starts with safety properties.
Safety properties are state properties. They can be tested by determining if all reachable (reachability is critical) states are acceptable. General protocol safety properties are
These properties were tested in the INRSFSM model by an examination of each reachable state, either by directly examining the FSM composite state diagram. These properties were also calculated by cfr and reported in the .err file. The reporting of unspecified receptions was important for determining when a single process might be deadlocked in a livelock cycle. Such a deadlock would not be reported as a system deadlock.
Promela, in contrast to INRSFSM, allows variables. The global state in Promela composite system execution is the execution states of each process and the values of each variable. The composite INRSFSM has only an execution state. The question of whether the complete set of reachable states is reasonable is now much more complicated. The assert(.) expression is the key method for determining whether the state variables are reasonable in any particular composite process execution state.
s_n1: if :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; > goto s_d1} :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; > goto s_d1x} fi;
This expression will block if the message in the input channel is not N0 or N1. Unless this leads to a system deadlock, it will not be reported by Spin. The technique is to convert the potential deadlock to an assertion violation This is done as follows:
#define True 1 #define False 0 #define Vrai 1 #define Faux 0 s_n1: if :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; > goto s_d1} :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; > goto s_d1x} :: (nempty(Pr_chan) && !((Pr_chan?[N0])  (Pr_chan?[N1]))) > assert(False) fi;
In general one would add :: else assert(False) to the if ... fi expression but here it is complicated because the else will be executed when the channel is empty giving a false error. If possible an :: else assert(False), or equivalent, should be added to all if .. fi or do .. od expressions where the choices should be complete and :: else skip to if .. fi expressions where it is acceptable if none of the choices are true.
The service specification for the protocols of Chapter 3 was that ``it transfer an infinite sequence of arbitrary data from L3 of the sender to L3 of the receiver, in order, without loss or error''. In those models we used the special sequence (D0 D1 D2)^{*}. In the INRSFSM models we used the blocking behaviour of the FSM and the reporting of unspecified receptions to show correctness. In the Promela models it is appropriate to add a new global variable state and assertions on its value. This approach has the advantage that we can use the same state variable later to test liveness properties. One way of modifying the code for m72.prm is as follows:
byte state=0; proctype Dr () { s0: atomic{(Dr_chan?[D0]) > assert(state==0); state=1; Dr_chan?D0; goto s1} s1: atomic{(Dr_chan?[D1]) > assert(state==1); state=2; Dr_chan?D1; goto s2} s2: atomic{(Dr_chan?[D2]) > assert(state==2); state=0; Dr_chan?D2; goto s0} }
After each assert(state==x), the next value of state is set.
The service specification for our protocol required that we be able to transmit an arbitrary sequence of data, without error. How do we represent an arbitrary sequence by an FSM and how do we test that it has been received without error.

These FSMs generate/accept the sequence (0 1 2)^{*} by starting at the initial state s0 (indicated by the arrow pointing to the state) and terminating at the ``accept'' state with the double circle, also s0. (01 2)^{*} is a ``regular'' expression and the set of sequences (e,012,012012,012012012, ...) is a ``regular'' expression. The sequence e is the zero length or ``empty'' sequence.
The FSM that accepts the regular language (e,0,01,012,0120,01201,012012,..) has all three states as accepting states. An ``accepting'' state for a regular language is one

The regular language accepted by this FSM, also known as an ``automaton'', may also written as

Each of the expressions (0 1 2)^{*}, 0 (1 2 0)^{*}, 0 1 (2 1 0)^{*} represent a set of sequences and the + is the sum or set union of these sequences. The general form of each expression is the sequence to get from the initial state, s0, to a accept state and the expression in (...) is the sequence to return to this state. For example,
The number of different sequences in the langage is infinite.
If we interpret the ``accept'' state as a state that is infinitely
recurrent in any infinite sequence, we have the langage accepted by Dr2
as

This FSM is known as a ``Büchi automaton''. Interestingly, there are only 3 infinite sequences in this Wregular language.
An FSM that generates/accepts all possible sequences of an arbitrary alphabet (d0, d1, d2, .. dn) consists of one state with n selfloop transitions. This is a very simple model, but it is impossible to use it for testing correctness because it impossible to check if the sequence actually sent was the one accepted. Sequences with and without errors are indistinguishable.
Wolper noted that it is possible to test protocol for the correct transmission of arbitrary sequences by using a sequence with just three values. This sequence is D0^{*} D1 D0^{*} D2 D0^{w}. Wolper originally described the language in terms of coloured balls, White, Red, and Blue W^{*} R W^{*} B W^{w}. The FSM that accepts this sequence is

The composite system with a generator/receiver simultaneously tests an infinite number of finite sequences.
The INRSFSM model for Wolper's message generation has 783 states. The Promela model m72 with Wolper's message generation and safety tests is
/* Conversion of FSM file, {\em m7w.fsm}, to Promela {\em m7w.prm}*/ #define True 1 #define Vrai 1 #define False 0 #define Faux 0 mtype= { P, W, R, B, T1, A0, N0, T0, A1, N1 }; chan Dg_chan=[1] of {mtype}; chan Dr_chan=[1] of {mtype}; chan Ps_chan=[2] of {mtype}; chan Pr_chan=[2] of {mtype}; byte state=0; proctype Dg () { s0: if :: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!W; goto s0} :: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!R; goto s1} fi; s1: if :: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!W; goto s1} :: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!B; goto s2} fi; s2: atomic{(Dg_chan?[P] && (len(Ps_chan) <= 1)) > Dg_chan?P; Ps_chan!W; goto s2} } proctype Dr () { s0: if :: atomic{(Dr_chan?[W]) > assert(state == 0); Dr_chan?W; goto s0} :: atomic{(Dr_chan?[R]) > assert(state == 0); state = 1; Dr_chan?R; goto s1} :: (nempty(Dr_chan) && !((Dr_chan?[W])  (Dr_chan?[R]))) > assert(False) fi; s1: if :: atomic{(Dr_chan?[W]) > assert(state == 1); Dr_chan?W; goto s1} :: atomic{(Dr_chan?[B]) > assert(state == 1); state = 2; Dr_chan?B; goto s2} :: (nempty(Dr_chan) && !((Dr_chan?[W])  (Dr_chan?[B]))) > assert(False) fi; s2: if :: atomic{(Dr_chan?[W]) > assert(state == 2); Dr_chan?W; goto s2} :: (nempty(Dr_chan) && !(Dr_chan?[W])) > assert(False) fi } proctype Ps () { s_0: atomic{( (len(Dg_chan) <= 0)) > Dg_chan!P; goto s_n0} s_n0: if :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; goto s_n0} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; goto s_n0} :: atomic{(Ps_chan?[W] && (len(Pr_chan) <= 0)) > Ps_chan?W; Pr_chan!N0; Pr_chan!W; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[W]) > Ps_chan?W; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[R] && (len(Pr_chan) <= 0)) > Ps_chan?R; Pr_chan!N0; Pr_chan!R; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[R]) > Ps_chan?R; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[B] && (len(Pr_chan) <= 0)) > Ps_chan?B; Pr_chan!N0; Pr_chan!B; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[B]) > Ps_chan?B; Ps_chan!T0; goto s_a02} fi; s_a00: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!W; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a00} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; goto s_a00} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_a01: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!R; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a01} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; goto s_a01} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_a02: if :: atomic{(Ps_chan?[T0] && (len(Pr_chan) <= 0)) > Ps_chan?T0; Pr_chan!N0; Pr_chan!B; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; Ps_chan!T0; goto s_a02} :: atomic{(Ps_chan?[A0]) > Ps_chan?A0; goto s_a02} :: atomic{(Ps_chan?[A1] && (len(Dg_chan) <= 0)) > Ps_chan?A1; Dg_chan!P; goto s_n1} fi; s_n1: if :: atomic{(Ps_chan?[T0]) > Ps_chan?T0; goto s_n1} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; goto s_n1} :: atomic{(Ps_chan?[W] && (len(Pr_chan) <= 0)) > Ps_chan?W; Pr_chan!N1; Pr_chan!W; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[W]) > Ps_chan?W; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[R] && (len(Pr_chan) <= 0)) > Ps_chan?R; Pr_chan!N1; Pr_chan!R; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[R]) > Ps_chan?R; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[B] && (len(Pr_chan) <= 0)) > Ps_chan?B; Pr_chan!N1; Pr_chan!B; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[B]) > Ps_chan?B; Ps_chan!T1; goto s_a12} fi; s_a10: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!W; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a10} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; goto s_a10} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; s_a11: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!R; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a11} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; goto s_a11} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; s_a12: if :: atomic{(Ps_chan?[T1] && (len(Pr_chan) <= 0)) > Ps_chan?T1; Pr_chan!N1; Pr_chan!B; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[T1]) > Ps_chan?T1; Ps_chan!T1; goto s_a12} :: atomic{(Ps_chan?[A1]) > Ps_chan?A1; goto s_a12} :: atomic{(Ps_chan?[A0] && (len(Dg_chan) <= 0)) > Ps_chan?A0; Dg_chan!P; goto s_n0} fi; } proctype Pr () { s_n0: if :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; goto s_d0} :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; goto s_d0x} fi; s_d0: if :: atomic{(Pr_chan?[W] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?W; Ps_chan!A1; Dr_chan!W; goto s_n1} :: atomic{(Pr_chan?[R] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?R; Ps_chan!A1; Dr_chan!R; goto s_n1} :: atomic{(Pr_chan?[B] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?B; Ps_chan!A1; Dr_chan!B; goto s_n1} :: atomic{(Pr_chan?[W] && (len(Dr_chan) <= 0)) > Pr_chan?W; Dr_chan!W; goto s_n1} :: atomic{(Pr_chan?[R] && (len(Dr_chan) <= 0)) > Pr_chan?R; Dr_chan!R; goto s_n1} :: atomic{(Pr_chan?[B] && (len(Dr_chan) <= 0)) > Pr_chan?B; Dr_chan!B; goto s_n1} fi; s_d0x: if :: atomic{(Pr_chan?[W] && (len(Ps_chan) <= 1)) > Pr_chan?W; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[R] && (len(Ps_chan) <= 1)) > Pr_chan?R; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[B] && (len(Ps_chan) <= 1)) > Pr_chan?B; Ps_chan!A0; goto s_n0} :: atomic{(Pr_chan?[W]) > Pr_chan?W; goto s_n0} :: atomic{(Pr_chan?[R]) > Pr_chan?R; goto s_n0} :: atomic{(Pr_chan?[B]) > Pr_chan?B; goto s_n0} fi; s_n1: if :: atomic{(Pr_chan?[N1]) > Pr_chan?N1; goto s_d1} :: atomic{(Pr_chan?[N0]) > Pr_chan?N0; goto s_d1x} fi; s_d1: if :: atomic{(Pr_chan?[W] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?W; Ps_chan!A0; Dr_chan!W; goto s_n0} :: atomic{(Pr_chan?[R] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?R; Ps_chan!A0; Dr_chan!R; goto s_n0} :: atomic{(Pr_chan?[B] && (len(Dr_chan) <= 0) && (len(Ps_chan) <= 1)) > Pr_chan?B; Ps_chan!A0; Dr_chan!B; goto s_n0} :: atomic{(Pr_chan?[W] && (len(Dr_chan) <= 0)) > Pr_chan?W; Dr_chan!W; goto s_n0} :: atomic{(Pr_chan?[R] && (len(Dr_chan) <= 0)) > Pr_chan?R; Dr_chan!R; goto s_n0} :: atomic{(Pr_chan?[B] && (len(Dr_chan) <= 0)) > Pr_chan?B; Dr_chan!B; goto s_n0} fi; s_d1x: if :: atomic{(Pr_chan?[W] && (len(Ps_chan) <= 1)) > Pr_chan?W; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[R] && (len(Ps_chan) <= 1)) > Pr_chan?R; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[B] && (len(Ps_chan) <= 1)) > Pr_chan?B; Ps_chan!A1; goto s_n1} :: atomic{(Pr_chan?[W]) > Pr_chan?W; goto s_n1} :: atomic{(Pr_chan?[R]) > Pr_chan?R; goto s_n1} :: atomic{(Pr_chan?[B]) > Pr_chan?B; goto s_n1} fi; } init{ atomic{run Dg(); run Dr(); run Ps(); run Pr(); }} /*  the results  (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim  (none specified) assertion violations + cycle checks  (disabled by DSAFETY) invalid endstates + Statevector 48 byte, depth reached 341, errors: 0 784 states, stored 8416 states, matched 9200 transitions (= stored+matched) 22063 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype Dg (0 of 30 states) unreached in proctype Dr line 65, state 13, "assert(0)" line 74, state 28, "assert(0)" line 81, state 37, "assert(0)" line 83, state 40, "end" (4 of 40 states) unreached in proctype Ps (0 of 235 states) unreached in proctype Pr (0 of 149 states) unreached in proctype :init: (0 of 6 states) */
Liveness properties are the properties of infinite sequences and hence cycles in an FSM. A liveness property is satisfied if all paths in the FSM lead to states that satisfy the property. This section introduces Linear Temporal Logic (LTL) for describing the properties of cycles, and the use of LTL for proving properties in Promela/Spin.
Propsitional boolean logic forms the basis of LTL.
&& a\b 0  1   commutative  0  0  0   1  0  1    a\b 0  1   commutative  0  0  1   1  1  1   ! a  0  1   1  0   > a\b 0  1   not commutative  0  1  1   1  0  1  
(a > b) == (!a  b)  proof? !(a && b) == (!a  !b)  De Morgan I !(a  b) == (!a && !b)  De Morgan II !!a == a (a  a) == (a && a) == a (a !a) == 1 (a &&!a) == 0
bit a,b; byte c; if :: ((a == b) && (c == 0)) > ch!A :: ((a != b)  (c > 0)) > ch!B :: else assert(1) /* necessary? */ fi
Linear Temporal Logic (LTL) is a language for the description of the properties of infinite sequences. All such sequences are generated by an FSM. A sequence is infinite if and only if it traverses one or more cycles in the FSM.
[1] ![]p == <>!p  proof? ( not always {\em p} implies there exists ???) [2] !<>p == []!p  proof? [3] !(p U q) == (!q)<u>(!p && !q)  proof? [4] !(p <u> q) == (!q)U(!p && !q)  proof? [5] [](p && q) == []p && []q  proof? [6] <>(p  q) == <>p  <>q  proof? [7/9] p U (q  r) == pUq  pUr  proof? [8/10] (p && q) U r == pUr && qUr  proof? [11] []<>(p  r) == []<>p  []<>r  proof? [12] <>[](p && r) == <>[]p && <>[]r  proof?
Wolper showed that it is possible to represent any LTL formula by a Büchi automata
[] < > p  (p) is infinitely recurrent

< > []p  stability of (p)

[](p > < > q)

![](p > < > q)

rUq

[](p > rUq)

Spin calculates a Büchi automata (really a never automata) that corresponds to an LTL formula. Unlike automata for regular languages, there is no canonical or minimal Büchi automaton for a particular LTL formula (wregular language).
C:\INRS\T224_00>spin f "<>[]p" never { /* <>[]p */ T0_init: if :: ((p)) > goto accept_S2 :: (1) > goto T0_init fi; accept_S2: if :: ((p)) > goto T0_S2 fi; T0_S2: if :: ((p)) > goto accept_S2 fi; accept_all: skip }
This calculation corresponds to

There is one more state in this automaton than the one calculated by hand above.
Another example is
C:\INRS\T224_00>spin f "[](p >r U q)" never { /* [](p >r U q) */ T0_init: if :: ((! ((p))  (q))) > goto accept_S24 :: ((r)) > goto T0_S39 fi; accept_S24: if :: ((! ((p))  (q))) > goto T0_init :: ((r)) > goto T0_S39 fi; accept_S39: if :: ((r)) > goto T0_S39 :: ((q)) > goto T0_init fi; T0_S39: if :: ((r)) > goto T0_S39 :: ((q)) > goto accept_S24 :: ((q) && (r)) > goto accept_S39 fi; accept_all: skip }
This corresponds to

There is real difference between this automaton and the one calculated above, by hand. Perhaps there is an error in the one we calculated by hand  or perhaps this is just an example of the lack of a canonical form.
A liveness test for m7w is < > [](state==3). In general, we need to test if all the paths in the composite system satisfy this formula. Unfortunately this computation is too difficult. It much easier to determine whether a system accepts only the ``empty'' language. If an LTL formula must be true for every path in the system, then is means that the negation of this formula must never be true in the system. Spin computes if the language accepted by the system is empty, and hence the Holzmann calls these never automata.
In order to determine whether the language accepted by the system is empty, it is necessary to create a ``synchronous product'' between the original system and the never automaton.
Promela/Spin has a special proposition, (np_), which is false in every progress state and is true in every other state. The never automatom, shown below, tests for the existence of nonprogress cycles.
never { /* <>[] np_ */ do :: skip :: np_ > break od; accept: do :: np_ od }
In this example we must show that the Promela process generates the language W^{*}WW(WW)^{*}BB^{w}. The Büchi automaton that accepts this language is

/* an example of a liveness test  {\em ww_b1} */ /* W* W W (WW)* B B* */ mtype = {W,B,s0,s1,s2,s3, null} /* liveness test variable */ mtype state; /* !<>cp spin f "\!<>cp" where (cp) is (state == s3)*/ never { accept_init: T0_init: if :: (! ((state == s3))) > goto accept_S1 fi; accept_S1: T0_S1: if :: (! ((state == s3))) > goto accept_S1 fi; accept_all: skip } active proctype wb () { mtype message; message=null; state=s0; new_message: if :: (state==s0) > message = W; if :: state=s0 :: state=s1 fi :: (state==s1) > message = W; state=s2 :: (state==s2) > if :: state=s1 ; message = W :: state=s3 ; message = B fi :: (state==s3) > message = B :: else > assert(0) fi; goto new_message }
This model uses a different method for representing an FSM than we the translation by m2p.
The results are
warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) pan: acceptance cycle (at depth 10) pan: wrote ww_b1.trail pan: reducing search depth to 21 pan: wrote ww_b1.trail pan: reducing search depth to 9 (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 20 byte, depth reached 21, errors: 2 12 states, stored (22 visited) 12 states, matched 34 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype wb line 50, state 20, "message = B" line 51, state 22, "assert(0)" (2 of 26 states)
The error trace is
1: proc 0 (NEVER) line 18 "never" 1: proc  (:never:) line 18 "ww_b1" (state 1) [(!((state==s3)))] Never claim moves to line 18 [(!((state==s3)))] 2: proc 0 (wb) line 36 "ww_b1" (state 1) [message = null] wb(1):message = null 3: proc 0 (NEVER) line 23 "never" 3: proc  (:never:) line 23 "ww_b1" (state 5) [(!((state==s3)))] Never claim moves to line 23 [(!((state==s3)))] 4: proc 0 (wb) line 37 "ww_b1" (state 2) [state = s0] state = s0 ««<START OF CYCLE»»> 5: proc  (:never:) line 23 "ww_b1" (state 5) [(!((state==s3)))] 6: proc 0 (wb) line 40 "ww_b1" (state 3) [((state==s0))] 7: proc  (:never:) line 23 "ww_b1" (state 5) [(!((state==s3)))] 8: proc 0 (wb) line 40 "ww_b1" (state 4) [message = W] wb(1):message = W 9: proc  (:never:) line 23 "ww_b1" (state 5) [(!((state==s3)))] 10: proc 0 (wb) line 41 "ww_b1" (state 5) [state = s0] state = s0 spin: trail ends after 10 steps #processes: 2 state = s0 10: proc 0 (wb) line 40 "ww_b1" (state 23) 10: proc 0 (NEVER) line 22 "never" 10: proc  (:never:) line 22 "ww_b1" (state 7) 2 processes created  The first error is the first cycle in {\em ww_b1} new_message: if :: (state==s0) > message = W; if :: state=s0 :: state=s1 fi
We add a progress label to cut the cycle.
/* an example of a liveness test  {\em ww_b2}*/ mtype = {W,B,s0,s1,s2,s3, null} /* !<>cp 8:ours> spin f "\!<>cp" */ /* liveness test variable */ mtype state; never { accept_init: T0_init: if :: (!(state == s3) && np_) > goto accept_S1 fi; accept_S1: T0_S1: if :: (!(state == s3) && np_ ) > goto accept_S1 fi; accept_all: skip } active proctype wb () { mtype message; message=null; state=s0; new_message: if :: (state==s0) > progress_s0: message = W; if :: state=s0 :: state=s1 fi :: (state==s1) > message = W; state=s2 :: (state==s2) > if :: state=s1 ; message = W :: state=s3 ; message = B fi :: (state==s3) > message = B :: else > assert(0) fi; goto new_message }  the results  warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 20 byte, depth reached 6, errors: 0 4 states, stored (8 visited) 2 states, matched 10 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype wb line 37, state 7, "state = s0" line 37, state 7, "state = s1" line 40, state 10, "message = W" line 41, state 11, "state = s2" line 43, state 14, "message = W" line 44, state 16, "message = B" line 42, state 17, "state = s1" line 42, state 17, "state = s3" line 46, state 20, "message = B" line 47, state 22, "assert(0)" (8 of 26 states)  There is no ``error'' but there is much unreached code. This indicates a very big problem. The {\em progress} label cuts the program just after (state==s0) and prevents progress to the rest of the program. new_message: if :: (state==s0) > progress_s0: message = W; if :: state=s0 :: state=s1 fi
In this model, the position of the progress_s0 is changed so it only cuts the first cycle.
active proctype wb () { mtype message; message=null; state=s0; new_message: if :: (state==s0) > message = W; if :: skip; progress_s0: state=s0 :: state=s1 fi :: (state==s1) > message = W; state=s2 :: (state==s2) > if :: state=s1 ; message = W :: state=s3 ; message = B fi :: (state==s3) > message = B :: else > assert(0) fi; goto new_message  the results  warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) pan: acceptance cycle (at depth 10) pan: wrote ww_b3.trail pan: reducing search depth to 21 (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 20 byte, depth reached 21, errors: 1 13 states, stored (25 visited) 11 states, matched 36 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype wb line 49, state 21, "message = B" line 50, state 23, "assert(0)" (2 of 27 states)  error  The new error is the second cycle.
Here we add a new progress_s2 to cut the second cycle.
active proctype wb () { mtype message; message=null; state=s0; new_message: if :: (state==s0) > message = W; if :: skip; progress_s0: state=s0 :: state=s1 fi :: (state==s1) > message = W; state=s2 :: (state==s2) > if :: state=s1 ; progress_s2: message = W :: state=s3 ; message = B fi :: (state==s3) > message = B :: else > assert(0) fi; goto new_message } the results  warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 20 byte, depth reached 20, errors: 0 13 states, stored (26 visited) 9 states, matched 35 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype wb line 45, state 21, "message = B" line 46, state 23, "assert(0)" (2 of 27 states)  error  There are no errors but the final state is not accesible. The problem here, and it is not at all obvious, is in the statement of language of the {\em never} automaton. If a test with a {\em never} automaton includes the existence of nonprogress cycles, it is almost impossible to get a correct specification by the negation of an LTL expression.
/* exemple of a liveness test*/ /* spin specification ... un test which includes a finitely recurring cycle  the correct LTL expression <>([](!cp && np_))  this expression means ==> It is an error if there exists a cycle where (cp) is false and there does not exist a progress label. */ mtype = {W,B,s0,s1,s2,s3, null} /* <>([](!cp && np_)) 146:ours> spin f '<>([](\!cp && np_))' */ /* correctness variable (liveness) */ mtype state; never { T0_init: if :: (1) > goto T0_init :: (! (state == s3) && (np_)) > goto accept_S2 fi; accept_S2: if :: (! (state == s3) && (np_)) > goto T0_S2 fi; T0_S2: if :: (! (state == s3) && (np_)) > goto accept_S2 fi; accept_all: skip } active proctype wb () { mtype message; message=null; state=s0; new_message: if :: (state==s0) > message = W; if :: skip; progress_s0: state=s0 :: state=s1 fi :: (state==s1) > message = W; state=s2 :: (state==s2) > if :: state=s1 ; progress_s2: message = W :: state=s3 ; message = B; skip fi :: (state==s3) > message = B :: else > assert(0) fi; goto new_message }  the results  warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 20 byte, depth reached 27, errors: 0 39 states, stored (62 visited) 20 states, matched 82 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype wb line 62, state 24, "assert(0)" (1 of 28 states)
There are permanent cycles which exist because there is another process with a transition that could execute, and break the cycle, at any point in the cycle. This is known as a ``weakly unfair'' cycle. Spin allows the enforcing of ``weak fairness'' to prevent such a cycle being indicated as an error.
/* an example of the effect of the application of {\em weak fairness} */ byte state[2]; /* C:\ATHENA.BAK>spin f "![]<>a" */ never { /* ![]<>a */ T0_init: if :: (! (state[0] == 1)) > goto accept_S2 :: (1) > goto T0_init fi; accept_S2: if :: (! (state[0] == 1)) > goto T0_S2 fi; T0_S2: if :: (! (state[0] == 1)) > goto accept_S2 fi; accept_all: skip } proctype A (bit id) {A_init: state[id] = 0; skip; state[id] = 1; goto A_init } init{ atomic{run A(0); run A(1)}}  the results  C:\INRS\T224_00>pan a warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) pan: acceptance cycle (at depth 19) pan: wrote wf.prm.trail (Spin Version 3.3.9  31 January 2000) Warning: Search not completed + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 28 byte, depth reached 31, errors: 1 15 states, stored (18 visited) 2 states, matched 20 transitions (= visited+matched) 1 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte)  error trace  1: proc 0 (NEVER) line 10 "never" 1: proc  (:never:) line 10 "wf.prm" (state 1) [(!((state[0]==1)))] Never claim moves to line 10 [(!((state[0]==1)))] 2: proc 0 (:init:) line 34 "wf.prm" (state 1) [(run A(0))] 3: proc 0 (:init:) line 34 "wf.prm" (state 2) [(run A(1))] 4: proc 0 (NEVER) line 15 "never" 4: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 5: proc 2 (A) line 28 "wf.prm" (state 1) [state[id] = 0] state[0] = 0 state[1] = 0 6: proc 0 (NEVER) line 19 "never" 6: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 7: proc 2 (A) line 29 "wf.prm" (state 2) [(1)] 8: proc 0 (NEVER) line 15 "never" 8: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 9: proc 2 (A) line 30 "wf.prm" (state 3) [state[id] = 1] state[0] = 0 state[1] = 1 10: proc 0 (NEVER) line 19 "never" 10: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 11: proc 2 (A) line 28 "wf.prm" (state 1) [state[id] = 0] state[0] = 0 state[1] = 0 12: proc 0 (NEVER) line 15 "never" 12: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 13: proc 2 (A) line 29 "wf.prm" (state 2) [(1)] 14: proc 0 (NEVER) line 19 "never" 14: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 15: proc 2 (A) line 30 "wf.prm" (state 3) [state[id] = 1] state[0] = 0 state[1] = 1 16: proc 0 (NEVER) line 15 "never" 16: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 17: proc 1 (A) line 28 "wf.prm" (state 1) [state[id] = 0] state[0] = 0 state[1] = 1 18: proc 0 (NEVER) line 19 "never" 18: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 19: proc 1 (A) line 29 "wf.prm" (state 2) [(1)] ««<START OF CYCLE»»> 20: proc 0 (NEVER) line 15 "never" 20: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 21: proc 2 (A) line 28 "wf.prm" (state 1) [state[id] = 0] state[0] = 0 state[1] = 0 22: proc 0 (NEVER) line 19 "never" 22: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 23: proc 2 (A) line 29 "wf.prm" (state 2) [(1)] 24: proc 0 (NEVER) line 15 "never" 24: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 25: proc 2 (A) line 30 "wf.prm" (state 3) [state[id] = 1] state[0] = 0 state[1] = 1 26: proc 0 (NEVER) line 19 "never" 26: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 27: proc 2 (A) line 28 "wf.prm" (state 1) [state[id] = 0] state[0] = 0 state[1] = 0 28: proc 0 (NEVER) line 15 "never" 28: proc  (:never:) line 15 "wf.prm" (state 7) [(!((state[0]==1)))] Never claim moves to line 15 [(!((state[0]==1)))] 29: proc 2 (A) line 29 "wf.prm" (state 2) [(1)] 30: proc 0 (NEVER) line 19 "never" 30: proc  (:never:) line 19 "wf.prm" (state 11) [(!((state[0]==1)))] Never claim moves to line 19 [(!((state[0]==1)))] 31: proc 2 (A) line 30 "wf.prm" (state 3) [state[id] = 1] state[0] = 0 state[1] = 1 spin: trail ends after 31 steps #processes: 4 state[0] = 0 state[1] = 1 31: proc 2 (A) line 28 "wf.prm" (state 1) 31: proc 1 (A) line 30 "wf.prm" (state 3) 31: proc 0 (:init:) line 34 "wf.prm" (state 4) <valid endstate> 31: proc 0 (NEVER) line 14 "never" 31: proc  (:never:) line 14 "wf.prm" (state 9) 4 processes created  Comment  This cycle is a continual execution of {\em proc 2}, but {\em proc 1} is able to execute its Promela expression at any time. ===================================================== If {\em pan} is executed with {\em weak fairness}, the result is C:\INRS\T224_00>pan a f warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) (Spin Version 3.3.9  31 January 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness enabled) invalid endstates  (disabled by neverclaim) Statevector 28 byte, depth reached 51, errors: 0 46 states, stored (139 visited) 96 states, matched 235 transitions (= visited+matched) 2 atomic steps hash conflicts: 125 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype A (0 of 5 states) unreached in proctype :init: (0 of 4 states)  Comment  No errors and no unreached code ...
This chapter discusses an example of modeling a real protocol, CDMARLP, layer 2 for CDMA cellular mobile radio. We will use the standard IS707, Data Service Options for Wideband Spread Spectrum Systems. The standard is available from http://www.tiaonline.org for $258us. This model will use Chapter 2, Radio Link Protocol of IS707.
A general network model for mobile radio is given below.

This model is generic for all mobile radio systems. The Mobile Radio Network is a set of cells. The major difference between the systems GSM (Global System for Mobile), CDMA (Code Division Multiple Access), and TDMA (Time Division Multiple Access), is the modulation system between the MS (Mobile Station) and the BTS (Base Transmission System). Several BTS are used for each BSC (Base Station Controller) to reduce the cost. Between each BSC and the fixed wire network is an MSC (Mobile Switching Center).
The principal traffic on all current mobile radio networks, and the driving force of the design is voice telephony. The data traffic is allowed to use any bandwidth left over after the voice traffic has been served. A lot of the complication in the data protocols is due to the necessity of adapting to the needs of the voice traffic. It is conceivable the this will change in the future.
A critical difference between mobile data protocols and fixed wireline protocols is that the the location of an MS is unknown, and the physical (layer 1) connection does not always exist. The sequence of actions described below are applicable for any mobile radio system. We begin when the MS enters a new cell:
Each phase of the protocol has its own model There will be model for the connection phase, data transfer phase, and the disconnection phase. This chapter will only consider the connection and data transfer phases.
CDMARLP has transparent and nontransparent connections. The transparent connection just sends a stream of octets without any error correction. The nontransparent connection corrects errors, and may, additionally, use encryption. The model here is for nontransparent connections.
The specification of a nontransparent CDMA/RLP connection, without encryption, is in (Section 3.1.1.1, IS707.2). It is
When the RLP layer is initialized or reset, it shall transmit a continuous stream of SYNC RLP control frames (see 4.3.1). When the RLP layer receives a SYNC RLP control frame it shall respond with a SYNC/ACK RLP control frame, and shall continue sending SYNC/ACK RLP control frames until the next valid frame which is not a SYNC RLP control frame is received. When the RLP layer receives a SYNC/ACK RLP control frame it shall respond with an ACK RLP control frame, and shall continue sending ACK RLP control frames until the next valid frame which is not a SYNC/ACK control frame is received. When the RLP layer receives an ACK RLP control frame, it shall send no more SYNC, SYNC/ACK or ACK RLP control frames, and should begin sending RLP data frames.
The PDUs for CDMA/RLP are SYNC, SYNC_ACK, ACK, and I (information).
The initial INRSFSM model is
fsm c1(qs 1,qd p) /* notons on perd le message si le tampon est plein */ { init_ss>init_ss [/SYNC:c2]; init_ss>SR [SYNC/:]; /* receive message and change state */ init_ss>SAR [SYNC_ACK/:]; /* design decision */ SR>SR [SYNC/:]; SR>SR [/SYNC_ACK:c2]; SR>SAR [SYNC_ACK/:]; SR>td [ACK/:]; SAR>SAR [SYNC_ACK/:]; SAR>SAR [/ACK:c2]; SAR>td [ACK/:]; td>td [/I:c2]; td>td [I/:]; } fsm c2(qs 1,qd p) { init_ss>init_ss [/SYNC:c1]; init_ss>SR [SYNC/:]; init_ss>SAR [SYNC_ACK/:]; SR>SR [SYNC/:]; SR>SR [/SYNC_ACK:c1]; SR>SAR [SYNC_ACK/:]; SR>td [ACK/:]; SAR>SAR [SYNC_ACK/:]; SAR>SAR [/ACK:c1]; SAR>td [ACK/:]; td>td [/I:c1]; td>td [I/:]; } The state init_ss is used because {\em init} is a keyword in Promela. States and deadlocked processes  cdma0.fsm c1: qs:1 qd:p  c2: qs:1 qd:p  "; Unspecified receptions and deadlocked processes: Unspecified reception: c1 c1  td  q: ACK c2  SAR  q: Unspecified reception: c1 c1  td  q: ACK c2  SAR  q: I Deadlock: the input buffers are full c1  td  q: ACK c2  SAR  q: I Unspecified reception: c2 c1  td  q: c2  SAR  q: I Unspecified reception: c1 c1  td  q: ACK c2  SAR  q: SYNC_ACK Unspecified reception: c2 c1  SAR  q: SYNC_ACK c2  td  q: ACK Unspecified reception: c2 c1  SAR  q: c2  td  q: ACK Unspecified reception: c1 c1  SAR  q: I c2  td  q: ACK Deadlock: the input buffers are full c1  SAR  q: I c2  td  q: ACK Unspecified reception: c1 c1  SAR  q: I c2  td  q: Unspecified reception: c2 c1  SAR  q: ACK c2  td  q: ACK Unspecified reception: c2 c1  td  q: c2  td  q: ACK Unspecified reception: c2 c1  td  q: I c2  td  q: ACK Unspecified reception: c1 c1  td  q: ACK c2  SAR  q: ACK Unspecified reception: c1 c1  td  q: ACK c2  td  q: Unspecified reception: c1 c1  td  q: ACK c2  td  q: I Nomber of States: 72 Unused transitions:  There are really only two errors here c1  td  q: ACK ... an ACK is possible here c1  SAR  q: I ... an I is possible here ... this is an error in the standard  incompleteness is not uncommon in in a standard These corrections are made in cdma1.fsm  fsm c1(qs 1,qd p) { init_ss>init_ss [/SYNC:c2]; init_ss>SR [SYNC/:]; init_ss>SAR [SYNC_ACK/:]; SR>SR [SYNC/:]; SR>SR [/SYNC_ACK:c2]; SR>SAR [SYNC_ACK/:]; SR>td [ACK/:]; SAR>SAR [SYNC_ACK/:]; SAR>SAR [/ACK:c2]; SAR>td [ACK/:]; SAR>td [I/:]; td>td [ACK/:]; td>td [/I:c2]; td>td [I/:]; } fsm c2(qs 1,qd p) { init_ss>init_ss [/SYNC:c1]; init_ss>SR [SYNC/:]; init_ss>SAR [SYNC_ACK/:]; SR>SR [SYNC/:]; SR>SR [/SYNC_ACK:c1]; SR>SAR [SYNC_ACK/:]; SR>td [ACK/:]; SAR>SAR [SYNC_ACK/:]; SAR>SAR [/ACK:c1]; SAR>td [ACK/:]; SAR>td [I/:]; td>td [ACK/:]; td>td [/I:c1]; td>td [I/:]; }  cdma1.err is States and deadlocked processes  cdma1.fsm c1: qs:1 qd:b  c2: qs:1 qd:b  "; Unspecified receptions and deadlocked processes: Nomber of States: 72 Unused transitions: 
The composed system is

It appears there are no safety or liveness errors, and all the nonprogress cycles are acceptable. However, we will use a Promela model to check that it is really true.
m2p is used to translate cdma1.fsm to cdma1.prm. The key problem for the liveness tests is finding the appropriate LTL expression. It is clear that we want to test that all paths in the composite system lead to td,td.
!<>[]((state[0]==1) && (state[1] == 1)) The first model is /* Conversion of FSM file, {\em cdma1.fsm}, to Promela {\em cdma1.prm}*/ mtype= { SYNC, SYNC_ACK, ACK, I }; chan c1_chan=[1] of {mtype}; chan c2_chan=[1] of {mtype}; byte state[2]; never { /* !<>[]a */ T0_init: if :: (! ((state[0]==1)&&(state[1]==1))) > goto accept_S9 :: (1) > goto T0_init fi; accept_S9: if :: (1) > goto T0_init fi; } proctype c1 () {byte id=0; init_ss: if :: atomic{( (len(c1_chan) <= 1) && (len(c2_chan) <= 0)) > c2_chan!SYNC; goto init_ss} :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: atomic{( (len(c1_chan) <= 1) && (len(c2_chan) <= 0)) > c2_chan!SYNC_ACK; goto SR} :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} fi; fi; SAR: if :: atomic{( (len(c1_chan) <= 1) && (len(c2_chan) <= 0)) > c2_chan!ACK; goto SAR} :: if :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; td: state[id]=1; if :: atomic{( (len(c1_chan) <= 1) && (len(c2_chan) <= 0)) > c2_chan!I; goto td} :: if :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; } proctype c2 () {byte id=1; init_ss: if :: atomic{( (len(c1_chan) <= 0)) > c1_chan!SYNC; goto init_ss} :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: atomic{( (len(c1_chan) <= 0)) > c1_chan!SYNC_ACK; goto SR} :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} fi; fi; SAR: if :: atomic{( (len(c1_chan) <= 0)) > c1_chan!ACK; goto SAR} :: if :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; td: state[id]=1; if :: atomic{( (len(c1_chan) <= 0)) > c1_chan!I; goto td} :: if :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; } init{ atomic{run c1(); run c2(); }}  the results  C:\INRS\CDMA_RLP>pan a I warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) pan: acceptance cycle (at depth 53) pan: wrote cdma1.prm.trail pan: reducing search depth to 34 pan: wrote cdma1.prm.trail pan: reducing search depth to 16 pan: wrote cdma1.prm.trail pan: reducing search depth to 7 (Spin Version 3.3.10  15 March 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 36 byte, depth reached 116, errors: 3 103 states, stored (180 visited) 290 states, matched 470 transitions (= visited+matched) 237 atomic steps hash conflicts: 1 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype c1 line 43, state 10, "c1_chan?SYNC_ACK" line 57, state 30, "c1_chan?ACK" line 71, state 50, "c1_chan?I" line 81, state 63, "c1_chan?ACK" (4 of 74 states) unreached in proctype c2 line 128, state 50, "c2_chan?I" (1 of 74 states) unreached in proctype :init: (0 of 4 states)  C:\INRS\CDMA_RLP>spin t r s l g cdma1.prm > cd1.tr1 et cd1.tr1 est Never claim moves to line 20 [(!(((state[0]==1)&&(state[1]==1))))] Never claim moves to line 25 [(1)] 6: proc 2 (c2) line 94 "cdma1.prm" Send SYNC > queue 1 (c1_chan) Never claim moves to line 20 [(!(((state[0]==1)&&(state[1]==1))))] 8: proc 1 (c1) line 40 "cdma1.prm" [Recv] SYNC < queue 1 (c1_chan) 9: proc 1 (c1) line 41 "cdma1.prm" Recv SYNC < queue 1 (c1_chan) ««<START OF CYCLE»»> Never claim moves to line 25 [(1)] 12: proc 2 (c2) line 94 "cdma1.prm" Send SYNC > queue 1 (c1_chan) Never claim moves to line 20 [(!(((state[0]==1)&&(state[1]==1))))] 14: proc 1 (c1) line 52 "cdma1.prm" [Recv] SYNC < queue 1 (c1_chan) 15: proc 1 (c1) line 53 "cdma1.prm" Recv SYNC < queue 1 (c1_chan) spin: trail ends after 15 steps #processes: 4 queue 1 (c1_chan): state[0] = 0 state[1] = 0 15: proc 2 (c2) line 92 "cdma1.prm" (state 15) c2(3):id = 1 15: proc 1 (c1) line 47 "cdma1.prm" (state 35) c1(2):id = 0 15: proc 0 (:init:) line 147 "cdma1.prm" (state 4) <valid endstate> 15: proc 0 (NEVER) line 24 "never" 15: proc  (:never:) line 24 "cdma1.prm" (state 9) 4 processes created The problem ... a nonprogress cycle with SYNC ... =============================================================== The second model is /* Conversion of FSM file, {\em cdma1.fsm}, to Promela {\em cdma1.prm}*/ mtype= { SYNC, SYNC_ACK, ACK, I }; chan c1_chan=[1] of {mtype}; chan c2_chan=[1] of {mtype}; byte state[2]; never { /* !<>[]a */ T0_init: if :: (! ((state[0]==1)&&(state[1]==1))&& np_) > goto accept_S9 :: (1) > goto T0_init fi; accept_S9: if :: (1) > goto T0_init fi; } proctype c1 () {byte id=0; init_ss: if :: c2_chan!SYNC; progress_ss: goto init_ss :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: c2_chan!SYNC_ACK; progress_sr: goto SR :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} fi; fi; SAR: if :: c2_chan!ACK; progress_sar: goto SAR :: if :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; td: state[id]=1; if :: c2_chan!I; goto td :: if :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; } proctype c2 () {byte id=1; init_ss: if :: c1_chan!SYNC; progress_ss: goto init_ss :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: c1_chan!SYNC_ACK; progress_sr: goto SR :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} fi; fi; SAR: if :: c1_chan!ACK; progress_sar: goto SAR :: if :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; td: state[id]=1; if :: c1_chan!I; goto td :: if :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; } init{ atomic{run c1(); run c2(); }} .................... the results .......................... C:\INRS\CDMA_RLP>pan a I warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) pan: acceptance cycle (at depth 65) pan: wrote cdma1a.prm.trail pan: reducing search depth to 41 pan: wrote cdma1a.prm.trail pan: reducing search depth to 20 pan: wrote cdma1a.prm.trail pan: reducing search depth to 9 (Spin Version 3.3.10  15 March 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 36 byte, depth reached 132, errors: 3 90 states, stored (144 visited) 260 states, matched 404 transitions (= visited+matched) 125 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype c1 line 44, state 9, "c1_chan?SYNC_ACK" line 53, state 20, "c1_chan?SYNC" line 57, state 28, "c1_chan?ACK" line 66, state 39, "c1_chan?SYNC_ACK" line 70, state 47, "c1_chan?I" line 79, state 58, "c1_chan?ACK" (6 of 69 states) unreached in proctype c2 line 97, state 9, "c2_chan?SYNC_ACK" line 110, state 28, "c2_chan?ACK" line 123, state 47, "c2_chan?I" (3 of 69 states) unreached in proctype :init: (0 of 4 states) ...................................................................... C:\INRS\CDMA_RLP>spin t r s p cdma1a.prm > cd1a.tr1 Le fichier cd1a.tr1 est 1: proc 0 (NEVER) line 20 "never" 1: proc  (:never:) line 20 "cdma1a.prm" (state 1) [((!(((state[0]==1)&&(state[1]==1)))&&np_))] Never claim moves to line 20 [((!(((state[0]==1)&&(state[1]==1)))&&np_))] 2: proc 0 (:init:) line 141 "cdma1a.prm" (state 1) [(run c1())] 3: proc 0 (:init:) line 141 "cdma1a.prm" (state 2) [(run c2())] 4: proc 0 (NEVER) line 25 "never" 4: proc  (:never:) line 25 "cdma1a.prm" (state 7) [(1)] Never claim moves to line 25 [(1)] 5: proc 2 (c2) line 91 "cdma1a.prm" Send SYNC > queue 1 (c1_chan) 5: proc 2 (c2) line 91 "cdma1a.prm" (state 1) [c1_chan!SYNC] 6: proc 0 (NEVER) line 21 "never" 6: proc  (:never:) line 21 "cdma1a.prm" (state 3) [(1)] Never claim moves to line 21 [(1)] 7: proc 2 (c2) line 92 "cdma1a.prm" (state 3) [(1)] 8: proc 0 (NEVER) line 20 "never" 8: proc  (:never:) line 20 "cdma1a.prm" (state 1) [((!(((state[0]==1)&&(state[1]==1)))&&np_))] Never claim moves to line 20 [((!(((state[0]==1)&&(state[1]==1)))&&np_))] 9: proc 1 (c1) line 38 "cdma1a.prm" Send SYNC > queue 2 (c2_chan) 9: proc 1 (c1) line 38 "cdma1a.prm" (state 1) [c2_chan!SYNC] 10: proc 0 (NEVER) line 25 "never" 10: proc  (:never:) line 25 "cdma1a.prm" (state 7) [(1)] Never claim moves to line 25 [(1)] 11: proc 2 (c2) line 94 "cdma1a.prm" [Recv] SYNC < queue 2 (c2_chan) 11: proc 2 (c2) line 94 "cdma1a.prm" (state 4) [(c2_chan?[SYNC])] 12: proc 2 (c2) line 95 "cdma1a.prm" Recv SYNC < queue 2 (c2_chan) 12: proc 2 (c2) line 95 "cdma1a.prm" (state 5) [c2_chan?SYNC] ««<START OF CYCLE»»> 13: proc 0 (NEVER) line 21 "never" 13: proc  (:never:) line 21 "cdma1a.prm" (state 3) [(1)] Never claim moves to line 21 [(1)] 14: proc 1 (c1) line 39 "cdma1a.prm" (state 3) [(1)] 15: proc 0 (NEVER) line 20 "never" 15: proc  (:never:) line 20 "cdma1a.prm" (state 1) [((!(((state[0]==1)&&(state[1]==1)))&&np_))] Never claim moves to line 20 [((!(((state[0]==1)&&(state[1]==1)))&&np_))] 16: proc 1 (c1) line 38 "cdma1a.prm" Send SYNC > queue 2 (c2_chan) 16: proc 1 (c1) line 38 "cdma1a.prm" (state 1) [c2_chan!SYNC] 17: proc 0 (NEVER) line 25 "never" 17: proc  (:never:) line 25 "cdma1a.prm" (state 7) [(1)] Never claim moves to line 25 [(1)] 18: proc 2 (c2) line 105 "cdma1a.prm" [Recv] SYNC < queue 2 (c2_chan) 18: proc 2 (c2) line 105 "cdma1a.prm" (state 19) [(c2_chan?[SYNC])] 19: proc 2 (c2) line 106 "cdma1a.prm" Recv SYNC < queue 2 (c2_chan) 19: proc 2 (c2) line 106 "cdma1a.prm" (state 20) [c2_chan?SYNC] spin: trail ends after 19 steps #processes: 4 queue 1 (c1_chan): [SYNC] queue 2 (c2_chan): state[0] = 0 state[1] = 0 19: proc 2 (c2) line 101 "cdma1a.prm" (state 33) 19: proc 1 (c1) line 39 "cdma1a.prm" (state 3) 19: proc 0 (:init:) line 141 "cdma1a.prm" (state 4) <valid endstate> 19: proc 0 (NEVER) line 19 "never" 19: proc  (:never:) line 19 "cdma1a.prm" (state 5) 4 processes created  the cycle still exists  The problem is the LTL expression.  We need to use LTL to describe exactly what constitutes an error. A definition is  ``It is an error if the system remains in a cycle where the final state is not {\em td,td} and if it remains in a cycle that does not have a progress label''. The LTL for this test is {\em (<>[]!((state[0]==1)&&(state[1]==1)) \&\& <>[]np\_)}. The third model is /* Conversion of FSM file, {\em cdma1.fsm}, to Promela {\em cdma1.prm}*/ mtype= { SYNC, SYNC_ACK, ACK, I }; chan c1_chan=[1] of {mtype}; chan c2_chan=[1] of {mtype}; byte state[2]; never { /* (<>[]!a && <>[]b) */ T0_init: if :: (! ((state[0]==1)&&(state[1]==1)) && np_) > goto accept_S4 :: (! ((state[0]==1)&&(state[1]==1))) > goto T0_S12 :: (np_) > goto T0_S27 :: (1) > goto T0_init fi; accept_S4: if :: (! ((state[0]==1)&&(state[1]==1)) && np_) > goto accept_S4 fi; T0_S12: if :: (! ((state[0]==1)&&(state[1]==1)) && np_) > goto accept_S4 :: (! ((state[0]==1)&&(state[1]==1))) > goto T0_S12 fi; T0_S27: if :: (! ((state[0]==1)&&(state[1]==1)) && np_) > goto accept_S4 :: (np_) > goto T0_S27 fi; } proctype c1 () {byte id=0; init_ss: if :: c2_chan!SYNC; progress_ss: goto init_ss :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: c2_chan!SYNC_ACK; progress_sr: goto SR :: if :: atomic{(c1_chan?[SYNC]) > c1_chan?SYNC; goto SR} :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} fi; fi; SAR: if :: c2_chan!ACK; progress_sar: goto SAR :: if :: atomic{(c1_chan?[SYNC_ACK]) > c1_chan?SYNC_ACK; goto SAR} :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; td: state[id]=1; if :: c2_chan!I; goto td :: if :: atomic{(c1_chan?[ACK]) > c1_chan?ACK; goto td} :: atomic{(c1_chan?[I]) > c1_chan?I; goto td} fi; fi; } proctype c2 () {byte id=1; init_ss: if :: c1_chan!SYNC; progress_ss: goto init_ss :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} fi; fi; SR: if :: c1_chan!SYNC_ACK; progress_sr: goto SR :: if :: atomic{(c2_chan?[SYNC]) > c2_chan?SYNC; goto SR} :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} fi; fi; SAR: if :: c1_chan!ACK; progress_sar: goto SAR :: if :: atomic{(c2_chan?[SYNC_ACK]) > c2_chan?SYNC_ACK; goto SAR} :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; td: state[id]=1; if :: c1_chan!I; goto td :: if :: atomic{(c2_chan?[ACK]) > c2_chan?ACK; goto td} :: atomic{(c2_chan?[I]) > c2_chan?I; goto td} fi; fi; } init{ atomic{run c1(); run c2(); }} ............ the results ................. C:\INRS\CDMA_RLP>spin a cdma1b.prm C:\INRS\CDMA_RLP>gcc DREACH o pan pan.c C:\INRS\CDMA_RLP>pan a I warning: for p.o. reduction to be valid the never claim must be stutterclosed (never claims generated from LTL formulae are stutterclosed) (Spin Version 3.3.10  15 March 2000) + Partial Order Reduction Full statespace search for: neverclaim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates  (disabled by neverclaim) Statevector 36 byte, depth reached 114, errors: 0 823 states, stored (978 visited) 7421 states, matched 8399 transitions (= visited+matched) 3200 atomic steps hash conflicts: 1085 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte) unreached in proctype c1 (0 of 69 states) unreached in proctype c2 (0 of 69 states) unreached in proctype :init: (0 of 4 states)
The nontransparent CDMARLP connection service is the same as all the other layer 2 protocols that we have studied  the transfer of an arbitrary, unbounded, sequence of bytes without error. Nontransparent CDMARLP is a pure NAK protocol. The receiver does not send ACKs, nor can an NAK be interpreted as an ACK. It sends a NAK when it detects a missing message. In a NAK based protocol, it is impossible to distinguish between a a channel that does not make any errors and one that is completely broken. The technique to maked this distinction in CDMARLP is as follows:
This description is in section 3.1.2.1 de IS702.2.
The project in this course is the development of a Promela model of the data transfer phase, without encryption, of CDMARLP, according to section 3.1.2.1. It is required that you use the capabilities of Promela/Spin to deteremine if any errors exist in the standard. It is very important that you are able to show that your model follows the satndard and is free of programming errors.
To help interpret the standard, note the following discussion
/* procedural information on NAK protocol for CDMARLP IS707.2 Section 3.1.2.1 */ v_s next new frame to send v_r next new frame to receive v_r'value of v_r after receiving new frame v_n next in sequence frame to receive v_n' value of v_n after receiving new frame rcv_buffer[M] ... buffer for received data ???? rcv_n_s; received sequence # in data frame Note on arithmetic mod M wrt window W ... W==M/2 .. here a < b <==> (ab+M) %M >= W a > b <==> (ba+M) %M > W ... note < and > not transitive ... Acceptance rules for DATA frames ... ** rcv_n_s < v_n > discard as a duplicate ** rcv_n_s == v_n > v_n' != v_n ... pass data from v_n to v_n'1 to L3 ** ((rcv_n_s > v_n) && (rcv_n_s < v_r) && (rcv_n_s !duplicate)) > store in rcv_buffer ** ((rcv_n_s == v_r) && (v_r == v_n)) ... pass new data to L3 && set v_n=(v_n+1)%M && v_r=(v_r+1)%M increment active NAK counters ** ((rcv_n_s >= v_r) && (v_r > v_n)) ... store new data in rcv_buffer[rcv_n_s] && set v_n=(rcv_n_s+1)%M increment active NAK counters send NAKs for all segments from v_n to v_r1 (simplification of actual protocol) Acceptance rules for IDLE frames ... ** ((rcv_n_s >= v_r) && (v_r > v_n)) ... set v_r=rcv_n_s send NAKs for all segments from v_n to v_r1 whose NAK counter is not active (== 0). increment active NAK counters ** else ignore Action on receiving a NAK ... ** resend all frames from FIRST to LAST inclusive ... ((rcv_n_s >= v_r) && (v_r > v_n)) ... set v_r=rcv_n_s send NAKs for all segments from v_n to v_r1 (simplification of actual protocol) else ... ignore rcv_n_s Erasure Count ... all PH_ERR_IND shall be considered as erasures ... ** When the consecutive erasure count exceeds M/2, the channel will be reset. ... here considered 'disconnected'.