{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];
}

2.3.4  Modeling of the communication channel and message loss

The most general model of a communication channel between processes p_a and p_b use a process p_c for the channel.

A simple example of a process for a channel p_c, where p_a sends message a to p_b, and p_b responds with a b. The programme acb.fsm

/* 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 non-deterministic 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 acb-p.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 non-deterministic 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 */
}

Chapter 3
A sequence of Data Link Protocols leading to the Alternating Bit Protocol

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.

3.1  Data Link Protocols

3.1.1  Service Requirements

The key service requirement of the Data Link Protocol (DLP) is

• accept an unbounded sequence of bytes (octets) from the local L3, the Network layer, and deliver them, in order, and without error to the ``Peer'' L3 layer at the other end of the L1 connection.

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

• control the flow of the octets when the destination is congested
• send frames, possibly empty, periodically to the destination
• control maximum delay for delivery to the Peer L2 and L3 entities.
• minimize the bandwidth utilisation of the connection

Initially we will be concerned only with the correctness of the delivery of the data.

3.1.2  Environment Model

• L3 source model - periodic?, octet by octet?, message?, L2 or L3 controlled?, data transparent?, ... 
• L1 channel model - errors with/without notification, frame reordering, delay, capacity, undetected errors, ... 
• L3 sink model- periodic?, octet by octet?, message?, L2 or L3 controlled?, data transparent?, ... 

This gives us wide range of models, even for simple protocols. In this section we will introduce the complications slowly.

3.2  Model 1 - Simple two-way handshake without errors

Alphabet

• D - Data message, Ps -> Pr
• A - Ack message, Pr -> Ps

Procedural Rules

• Ps sends a D and waits for an A from Pr before sending the next D. This is known as a ``two-way handshake''

Environment

• L1 - Channel sends messages without loss, error, or duplication

Formal Model

• Message/events are D and A
• Ps States: After examination of the procedural rules, it is seen that Ps has two states, ``able to send D'', s_d and ``waiting for A'', s_a.
• Pr States: After examination of the procedural rules, it is seen that Pr also has two states, ``waiting for D'', s_d and ``able to send A'', s_a.

/* 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

3.2.1  Is the protocol ``correct''?

Are there any general protocol errors?

• Safety Properties:

  • Deadlocks: No
  • Unspecified Reception: No
  • Unused Transitions: No
• Liveness Properties:

  • Livelocks: No - the only cycle is correct progress (why?)

Does it satisfy the specifications?

• Does it transfer an infinite sequence of arbitrary data from L3 of the sender to L3 of the receiver, in order, without loss or error? This is not evident from the model - why?

  • How do we represent an infinite sequence of arbitrary data with an FSM?
  • How do we check if the received sequence is identical to the sent sequence? We will discuss these issues in a future chapter on regular languages.
  • Model 1 only has one type of data symbol, D; thus the data sequence is not arbitrary.

3.3  Data Sequences and L3 service

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

3.3.1  Dg:Dr - simple direct connection (L3-1)

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.

3.3.2  Dg:Dr - simple direct connection with Dr input queue (qs 2) (L3-2)

This model is identical to L3-1 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 L3-1, 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?)

3.3.3  Dg:Dr - Connection via an ideal channel with (qs 1, qd b) (L3-3)

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 L3-3 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 L3-2, the additional Ch process increases the interleaving again leading to a more complicated behaviour.

3.3.4  Dg:Dr - Connection via an ideal channel with (qs 1, qd b) and Polling flow control (L3-4)

This model controls the flow between the channel and Dg via a poll. The channel is identical to that in L3-3 except for the extra state where it sends a Poll to Dg. The code for L3-4 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

3.4  Model 2 - addition of L3 data and tests of correctness

Alphabet

• D0, D1, D2 and A

Procedural Rules

• Pr starts by sending D0 and waits for an A, then D1 and waits for an A, then D2 and waits for an A, and then repeats the cycle.

Environment

• L1 - Channel sends messages without loss, error, or duplication

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

Is this protocol correct?

Even this very simple protocol is rather messy.

• Safety Properties:

  • Deadlocks: No - Since Dr is designed to block if it receives a message that is incorrect, we know that all messages that are received, are received in the correct order. However, this does not mean that any messages are actually received.
  • Unspecified Receptions: No
  • Unused Transitions: No
• Liveness Properties: To study liveness properties we must examine the cycles in the composite system. We need to show that all cycles send exactly the sequence D0 D1 D2 to Dr. All cycles pass through the state Dg:s1(),Dr:s0(),Ps:s_d(),Pr:s_d(D0) and that in all cycles Dr passes through s0, s1, and s2. This means that the system accepts the infinite sequence (D0 D1 D2)^w. Thus there are no liveness errors.

visible{Dg,Dr}

The visible system projection for Dg and Dr is

An examination of this diagram shows that it is identical to that of L3-4. this means that the environment of (Ps,Pr) is equivalent to an ideal channel with a Poll.

3.5  Model 3 - Errors with notification Ps -> Pr

This model now adds channel errors with notification to the model. This done as follows:

/* model 3-1 --- 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 3-1 --- poll 
	--- Ps -> Pr errors with notification*/
/* model 3-2 --- 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?)

Is this protocol correct?

• Safety Properties: Again there are no deadlocks so the the data is received correctly.
• Liveness Properties: All the cycles except the three two-transition cycles that correspond to the continuous loss of the repeated message after reception of a NAK are identical to Model 2. The continuous loss of messages indicates that the channel is broken so one would not expect to have correct communication. This cycle is infinite iff whenever the there is a choice between sending the message or an error notification, the error notification is chosen. This choice is ``unfair''.

visible{Dg,Dr}

The visible system projection for Dg and Dr is

A careful examination of this diagram shows that it is identical to that of L3-4. 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.

3.6  Model 4 - Errors with notification P_s <-> P_r

This model adds errors, with notification, in P_r -> P_s. The new model is

/* model 4-1 --- 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

Is this protocol correct?

• Safety Properties: An examination of the composite system or m4-1.err shows that there are many deadlock states. Although m4-1.err clearly indicates which states are deadlocks, a careful examination of the composite system is necessary to determine the reason. As usual in these circumstances, the error is obvious when it is is discovered. In this case, treating an Err as a NAK causes Ps to resend a D? that has already been received.

3.7  Model 5 - An ACK/NAK based protocol

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.

3.7.1  Model 5-1

The new system is

/* model 5-1 --- 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

Is this protocol correct?

The entry occurs when the transition s_d0 -> s_d1 [D0/D0:Dr,Err:Ps] is executed. Since model M5-1 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.

• s_a0 -> s_a0 [NAK2/Err:Pr];
• s_a1 -> s_a1 [NAK0/Err:Pr];
• s_a2 -> s_a2 [NAK1/Err:Pr];

visible{Dg,Dr}

The visible system projection for Dg and Dr is

An examination of this diagram shows that it is identical to that of L3-4. 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.

3.7.2  Model 5-2

Model 5-2 treats the NAK(i+1) as an ACK for the previous data. The new system is

/* model 5-1 --- 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 5-2 --- 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

Is this protocol correct?

• Safety Properties:

  • The visible{Dg,Dr} system is identical to the L3-4 system where the environment is a polling channel. Thus there are no deadlock states or other safety property errors.
• Liveness Properties:

  • The visible{Dg,Dr} system shows that there are no liveness errors involving the environment and Dg,Dr on L3. However, there still may be liveness errors just involving Ps and Pr. There are numerous Ps/Pr ``non-progress'' cycles in the composite system but they all involve at least one Err in the channel. A cycle involving continuous errors in the channel is not a ``permanent''condition in any functioning communication system. Hence these cycles are noot considered liveness errors.

This protocol is correct for errors with notification in both directions.

3.8  Model 6 - an ACK based Protocol

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.

3.8.1  Model 6-0 - no channel errors

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
	6-0 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 non-progress 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.

3.8.2  Model 6-1 - Errors Ps -> Pr

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
	6-0 no errors
        6-1 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 m6-1.err, indicates that there are no deadlock states. The only non-progress cycles have continual errors in the channel. This is an ``acceptable'' non-progress cycle.

Again the visible{Dg,Dr} is the same as L3-4 indicating the specification is satisfied.

3.8.3  Model 6-2 - Errors Ps <-> Pr

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
	6-0 no errors
        6-1 Err Ps->Pr
        6-2 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

m6-2.err indicates that there are deadlock states.

States and deadlocked processes --- m6-2.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 L3-4 indicating the specification is satisfied when there is no deadlock - not an entirely satisfactory method of satisfying the specification.

3.8.4  Model 6-3 - Errors Ps <-> Pr (Duplicate rejection)

/* 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
	6-0 no errors
        6-1 Err Ps->Pr
        6-2 Err Ps<->Pr
        6-3 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/-:-]; /* m6-3 -- reject as duplicate*/
  s_d0x -> s_n0 [D0/A0:Ps]; /* m6-3 */
  s_d0x -> s_n0 [D0/Err:Ps]; /* m6-3 */
  s_d0x -> s_n0 [D1/A0:Ps]; /* m6-3 */
  s_d0x -> s_n0 [D1/Err:Ps]; /* m6-3 */
  s_d0x -> s_n0 [D2/A0:Ps]; /* m6-3 */
  s_d0x -> s_n0 [D2/Err:Ps]; /* m6-3 */
  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/-:-]; /* m6-3 */
  s_d1x -> s_n1 [D0/A1:Ps]; /* m6-3 */
  s_d1x -> s_n1 [D0/Err:Ps]; /* m6-3 */
  s_d1x -> s_n1 [D1/A1:Ps]; /* m6-3 */
  s_d1x -> s_n1 [D1/Err:Ps]; /* m6-3 */
  s_d1x -> s_n1 [D2/A1:Ps]; /* m6-3 */
  s_d1x -> s_n1 [D2/Err:Ps]; /* m6-3 */
  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 L3-4 indicating the specification is satisfied.

3.9  Model 7 - an ACK based Protocol - Errors without notification

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.

3.9.1  Model 7-1 - Errors without notification Ps -> Pr (Duplicate rejection)

We start with the model M6-3 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
        7-1 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 M6-3, 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 L3-4 indicating the specification is satisfied.

3.9.2  Model 7-2 - Errors without notification Ps <-> Pr (Duplicate rejection)

The only change in 7-2 from 7-1 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
        7-1 Errors without notification Ps->Pr --- use timeouts and 
		messages T0, T1
        7-2 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 L3-4 indicating the specification is satisfied.

Chapter 4
Introduction to Promela/Spin

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.

4.1  The Spin Homepage

The url for Spin home page is http://netlib.bell-labs.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.bell-labs.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.

4.2  Introduction to Promela and Spin

The Spin Online References page,

http://cm.bell-labs.com/cm/cs/what/spin/Man/index.html, has several tutorial articles on Promela and Spin:

• Basic Spin Manual, a general introduction to language and tool, http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html
• A concise language reference for Promela, http://cm.bell-labs.com/cm/cs/what/spin/Man/Quick.html. This is an excellent introduction to the Promela and Spin, and goes into considerable detail.
• Guidelines for verification with Xspin, http://cm.bell-labs.com/cm/cs/what/spin/Man/GettingStarted.html
• Guidelines for verification directly with Spin, without graphical interface, http://cm.bell-labs.com/cm/cs/what/spin/Man/Roadmap.html
• A sample set of exercises with Spin, http://cm.bell-labs.com/cm/cs/what/spin/Man/Exercises.html

In addition, there is detailed information on the

• keywords, grammar, and sematics of Promela, http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.html;
• the runtime options for Spin, http://cm.bell-labs.com/cm/cs/what/spin/Man/Spin.html, for those of you who don't use Xspin;
• compile time options for creating the pan executables, http://cm.bell-labs.com/cm/cs/what/spin/Man/Pan.html#B, for those of you who don't use Xspin;
• runtime verification options for the pan executables, http://cm.bell-labs.com/cm/cs/what/spin/Man/Pan.html#A, for those of you who don't use Xspin;
• and finally, a description of the meaning of the output of pan, http://cm.bell-labs.com/cm/cs/what/spin/Man/Pan.html#C

4.3  An example conversion from FSM notation to Promela

The basic aspects of the conversion is as follows:

• States in the FSM model are labels. All the transitions of a specific state are listed as alternatives in an if ... fi construct
• The next state is reached by a goto <next state>
• The input queue of an fsm process is a Promela channel. Channels are all declared as global variables.
• Transitions in the FSM model are atomic. They consist of a 0 or 1 reads from the input channel and 0 or more writes to the input channels of other processes. The atomic construct of Promela is used to assure this atomicity. However, if an atomic blocks in its interior, control is allowed to switch to another process. Thus an atomic that blocks is not atomic. The only place that the atomic can block in the interior is if the destination channel is full. Each atomic adds a guard statement that checks to see if the channels have enough room before allowing the atomic to execute. This captures the semantics of the fsm model.
• Messages are modeled as mtypes.

The program m2p converts our FSM notation to Promela. An example, using the last model, m7-2.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\*

10-04-99   7:46         <DIR>    .
10-04-99   7:46         <DIR>    ..
 1-26-00  10:39           2,811  M7-2.fsm
          2,811 bytes in 1 file and 2 dirs    4,096 bytes allocated
  1,400,291,328 bytes free

C:\TEMP>m2p M7-2.fsm m72

C:\TEMP>dir

 Volume in drive C is MJF98          Serial number is 1237:10D1
 Directory of  C:\TEMP\*

10-04-99   7:46         <DIR>    .
10-04-99   7:46         <DIR>    ..
 1-26-00  10:39           2,811  M7-2.fsm
 2-10-00  10:52           4,593  m72.log
 2-10-00  10:52           7,282  m72.prm
 2-10-00  10:52             214  m72_0.dot
 2-10-00  10:52             211  m72_1.dot
 2-10-00  10:52           1,767  m72_2.dot
 2-10-00  10:52           1,185  m72_3.dot
 2-10-00  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
              m7-2.fsm
          ** the m72.log is a debug log file
          ** the m72.prm is the converted file
--------------------------------------

The original m7-2.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
        7-1 Errors without notification Ps->Pr --- use timeouts and 
		messages T0, T1
        7-2 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 M7-2.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(); }}

--------------------------------------------------------

Chapter 5
Tests for Protocol Correctness

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 w-regular languages, linear temporal logic, and the finite state machines (automata) to represent them. The discussion starts with safety properties.

5.1  Description and Testing of 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

• No Deadlocks
• No Unspecified Reception
• No Unused Transitions

These properties were tested in the INRS-FSM 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.

5.1.1  Safety properties in Promela/Spin

Promela, in contrast to INRS-FSM, 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 INRS-FSM 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.

• System Deadlocks: reported by Spin
• Unspecified Receptions: use assert(.)
• Unused code (transitions): reported by Spin
• Sufficient range of variable values: eg: does a sequence number Ns, that is supposed to take on values, 0,1,2,3 actually take on all these values - compile pan.c with -DVAR_RANGES flag

Unspecified Receptions

 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.

5.1.2  Satisfaction of the Specification - Safety Properties

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 INRS-FSM 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 m7-2.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.

5.2  How do we represent an infinite sequence with an FSM? - Regular and w-Regular languages

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.

• 0,1,2,3,4,5,6,7,8,.... is a (symbolic) representation of an infinite, but not arbitrary, sequence, but there is no FSM that can represent it (why ?).
• 0,1,2,0,1,2,0,1,2,... [ \triangle || = ](0 1 2)^w is an infinite sequence. The superscript w means that the sequence 0 1 2 is repeated infinitely often. A related notation is (0 1 2)^* means that the sequence 0 1 2 is repeated a finite, but unbounded number of times. Any finite length cycle of symbols may be represented by an FSM.

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)<sup>*</sup> 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

(0 1 2)* + 0 (1 2 0)* + 0 1 (2 0 1)*

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,

• Accept state - s0: e is the sequence from the initial state s0 to the accept state s0, and 012 is the sequence to leave and return to s0.
• Accept state - s1: 0 is the sequence from the initial state s1 to the accept state s1, and 120 is the sequence to leave and return to s1.
• Accept state - s2: 01 is the sequence from the initial state s1 to the accept state s2, and 201 is the sequence to leave and return to s2.

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

(0 1 2)w + 0 (1 2 0)w + 0 1 (2 1 0)w

This FSM is known as a ``Büchi automaton''. Interestingly, there are only 3 infinite sequences in this W-regular language.

5.2.1  Data Independence and Arbitrary Sequences

An FSM that generates/accepts all possible sequences of an arbitrary alphabet (d0, d1, d2, .. dn) consists of one state with n self-loop 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.

• Message loss: if the system loses a message at message index i, there is a sequence with an R message at that index and the loss will be detected.
• Message interchange: if the system can interchange messages at i and k, there is a sequence with an R at i and a B at k and that interchange will be detected.
• Message value error: If the system can change the value of a message at i, there is a sequence with an R message at that index and the change will be detected.

The INRS-FSM model for Wolper's message generation has 783 states. The Promela model m7-2 with Wolper's message generation and safety tests is

 /* Conversion of FSM file, {\em m7-w.fsm}, to Promela {\em m7-w.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:
	never-claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid endstates	+

State-vector 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)

*/

5.3  Description and representation of Liveness properties

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.

5.3.1  Propositional Boolean Logic

Propsitional boolean logic forms the basis of LTL.

• a proposition: (state == 3) - this proposition is true or false. In general 1 is equivalent to true and 0 is equivalent to false.
• the boolean operators are && (and), || (or), -> (implication), and ! (negation) - this notation is that used in Promela.
• let state[i] be the value of the state of the execution of the process P_i. If the proposition ((state[0] == 3) && (state[2] == 2)) is true, then P₀ is in state 3 and P₂ is in state 2, at the same time.
• all the operators, except !, are binary. Let a and b be two propositions. It is possible to represent the functionality of each operator by a truth table.

                  && 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 |
                        |-------|

Some important relations

      (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

An example

  bit a,b;
  byte c;

  if :: ((a == b) && (c == 0)) -> ch!A
     :: ((a != b) || (c > 0)) -> ch!B
     :: else assert(1) /* necessary? */
  fi 

5.3.2  Propositional Linear Temporal Logic

Reference: Verification of Concurrent Systems, Gerard Holzmann, 1995 (Draft version), pp 47/56 -Chapter 3

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.

• a temporal formula

  • let t be a trace of states (s₁,s₂,s₃, ...)
  • let p be a temporal formula.
  • (t,i) satisfies p, (t,i) |= p, if p is true in state s_i - all boolean logic formulas are LTL formulas. An example if p is (s == 5) - (t,i) |= (s == 5) iff (s_i = = 5) is true.
• Some temporal operators that are acceptable in Promela models are

  • strong eventually < > - let p be an LTL formula. (t,i)|= < > p if there is a j ³ i where s_j|=p.
  • always [] - (t,i)|=[]p si " j ³ i, s_j|=p.
  • strong until U - (t,i)|=pUq if there existes a a j where s_j|=q, et "k (i £ k < j), s_k|=p.
• A temporal operator that is not acceptable in Spin LTL formulas is

  • next the chaotic interleaving in the global model of the composition of the processes makes it impossible to use next inside a single process.
• Some additional operators that are acceptable in Spin are

  • weak until p < u > q == pUq || []p - q may not necessarily occur in the sequence.
  • weak eventually < e > p == 1 < u > p where (1==true)

Some relationships betwen the operators

[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? 

5.3.3  Some standard liveness properties

• Infinitely recurrent

  • let p be a state formula. [] < > p implies that always there is a next point in the future where p will be true. This is exactly the condition that a state is a Büchi automata accepting state.
• Stability

  • let p be a state formula. < > []p implies that there is a point in the trace where p is true for the remainder of the trace.

5.3.4  LTL formula and Büchi automata

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)


rUq

[](p- > rUq)

5.3.5  Calculation of Büchi automata by Spin

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 (w-regular 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.

5.3.6  Using LTL for proving liveness properties

A liveness test for m7-w 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.

Synchronised Product

• This synchronised product is unique to Promela/Spin.
• For each transition in the original system, a transition in the never automaton is executed.
• If it is impossible to execute the next transition in the never automaton, the system blocks.
• After a complete examination of the accessible states, if there is not a cycle with an accepting state, the language accepted is empty, and the system ``satisfies'' the never automaton.

5.3.7  A complication - acceptable non-progress cycles

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 non-progress cycles.

never {	/* <>[] np_ */
	do
	:: skip
	:: np_ -> break
	od;
accept:	do
	:: np_
	od
}

5.3.8  A sequence of examples

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

Model ww_b1

/* 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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
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:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 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

Model ww_b2

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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.9 -- 31 January 2000)
	+ Partial Order Reduction

Full statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 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

model ww_b3

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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
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:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 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. 

Model ww_b4

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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.9 -- 31 January 2000)
	+ Partial Order Reduction

Full statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 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 non-progress cycles, it is almost impossible to get a
correct specification by the negation of an LTL expression.

Model ww_b5

/* 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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.9 -- 31 January 2000)
	+ Partial Order Reduction

Full statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 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)

5.3.9  Weak Fairness

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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
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:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid endstates       - (disabled by never-claim)

State-vector 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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.9 -- 31 January 2000)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness enabled)
        invalid endstates       - (disabled by never-claim)

State-vector 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 ... 

Chapter 6
Modeling of a Real Protocol

This chapter discusses an example of modeling a real protocol, CDMA-RLP, layer 2 for CDMA cellular mobile radio. We will use the standard IS-707, 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 IS-707.

6.1  A general network model for mobile radio

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.

6.1.1  General Procedures for Mobile Data Protocols

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:

• The MS listens to the signals in the cell to determine the cell parameters.
• The MS announces its entry using a random access channel (slotted Aloha)
• If the MS wishes to make a call, it uses a random access channel to ask for a physical channel.
• If there is a call for the MS, the BSC sends a paging signal to the MS. After the reception of the page, the MS uses a random access channel to ask for a physical channel.
• The MS negotiates the parameters of the channel with the BSC.
• The BSC initiates a connection at layer 2 (RLP) (connection phase)
• The upper layer connections are then made.
• The MS then enters the phase of data transfer (data-transfer phase)
• The upper layer connections are terminated
• The MS or the BSC can terminate the layer 2 connection or just cut the layer 1 physcial connection without explicitly terminating layer 2. (disconnection phase).

6.2  Modeling of CDMA-RLP

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.

CDMA-RLP has transparent and non-transparent connections. The transparent connection just sends a stream of octets without any error correction. The non-transparent connection corrects errors, and may, additionally, use encryption. The model here is for non-transparent connections.

6.2.1  CDMA-RLP - connection phase

The specification of a non-transparent 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).

• I: Initialise a connection: Send SYNCs until the reception of a SYNC_ACK.
• II: After the reception of a SYNC, send a sequence of SYNC_ACKS until the reception of a PDU which is not a SYNC, and initialise all the system parameters.
• III: After the reception of SYNC_ACK, send ACKS until the reception of a PDU that is not a SYNC_ACK.
• IV: After the reception of an ACK, I PDus may be sent.

• There is no indication of states: a detailed examination of the specification is necessary to determine which states are reasonable. Different actions occur after the ``reception'' of a PDU.
• In general, a state is defined when one awaits an event
• Ici

  • init_ss - the initial state
  • init_ss - send an sequence of SYNC and wait for a SYNC_ACK
  • SR - after the reception of a SYNC, send a sequuence of SYNC_ACKs, and wait for a PDU that is not a SYNC (II)
  • SAR - after the reception of a SYNC_ACK, send a sequence of ACKs and await a PDU that is not a SYNC_ACK (III)
  • td - after the reception of an ACK, send Is (information)

Modeling of connection phase by INRS-FSM

The initial INRS-FSM 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 --- cdma-0.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 cdma-1.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/-:-];
}

-------------------------------------------------------

cdma-1.err is

States and deadlocked processes --- cdma-1.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 non-progress cycles are acceptable. However, we will use a Promela model to check that it is really true.

Promela Model

m2p is used to translate cdma-1.fsm to cdma-1.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 cdma-1.fsm}, to Promela {\em cdma-1.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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: acceptance cycle (at depth 53)
pan: wrote cdma-1.prm.trail
pan: reducing search depth to 34
pan: wrote cdma-1.prm.trail
pan: reducing search depth to 16
pan: wrote cdma-1.prm.trail
pan: reducing search depth to 7
(Spin Version 3.3.10 -- 15 March 2000)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid endstates       - (disabled by never-claim)

State-vector 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 cdma-1.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 "cdma-1.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 "cdma-1.prm" [Recv] SYNC	<- queue 1 (c1_chan)
  9:	proc  1 (c1) line  41 "cdma-1.prm" Recv SYNC	<- queue 1 (c1_chan)
««<START OF CYCLE»»>
Never claim moves to line 25	[(1)]
 12:	proc  2 (c2) line  94 "cdma-1.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 "cdma-1.prm" [Recv] SYNC	<- queue 1 (c1_chan)
 15:	proc  1 (c1) line  53 "cdma-1.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 "cdma-1.prm" (state 15)
		c2(3):id = 1
 15:	proc  1 (c1) line  47 "cdma-1.prm" (state 35)
		c1(2):id = 0
 15:	proc  0 (:init:) line 147 "cdma-1.prm" (state 4) <valid endstate>
 15:	proc 0 (NEVER) line   24 "never"
 15:	proc  - (:never:) line  24 "cdma-1.prm" (state 9)
4 processes created

The problem ... a non-progress cycle with SYNC ... 


===============================================================


The second model is


 /* Conversion of FSM file, {\em cdma-1.fsm}, to Promela {\em cdma-1.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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: acceptance cycle (at depth 65)
pan: wrote cdma-1a.prm.trail
pan: reducing search depth to 41
pan: wrote cdma-1a.prm.trail
pan: reducing search depth to 20
pan: wrote cdma-1a.prm.trail
pan: reducing search depth to 9
(Spin Version 3.3.10 -- 15 March 2000)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid endstates       - (disabled by never-claim)

State-vector 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 cdma-1a.prm > cd1a.tr1

Le fichier cd1a.tr1 est 

  1:	proc 0 (NEVER) line   20 "never"
  1:	proc  - (:never:) line  20 "cdma-1a.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 "cdma-1a.prm" (state 1)	[(run c1())]
  3:	proc  0 (:init:) line 141 "cdma-1a.prm" (state 2)	[(run c2())]
  4:	proc 0 (NEVER) line   25 "never"
  4:	proc  - (:never:) line  25 "cdma-1a.prm" (state 7)	[(1)]
Never claim moves to line 25	[(1)]
  5:	proc  2 (c2) line  91 "cdma-1a.prm" Send SYNC	-> queue 1 (c1_chan)
  5:	proc  2 (c2) line  91 "cdma-1a.prm" (state 1)	[c1_chan!SYNC]
  6:	proc 0 (NEVER) line   21 "never"
  6:	proc  - (:never:) line  21 "cdma-1a.prm" (state 3)	[(1)]
Never claim moves to line 21	[(1)]
  7:	proc  2 (c2) line  92 "cdma-1a.prm" (state 3)	[(1)]
  8:	proc 0 (NEVER) line   20 "never"
  8:	proc  - (:never:) line  20 "cdma-1a.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 "cdma-1a.prm" Send SYNC	-> queue 2 (c2_chan)
  9:	proc  1 (c1) line  38 "cdma-1a.prm" (state 1)	[c2_chan!SYNC]
 10:	proc 0 (NEVER) line   25 "never"
 10:	proc  - (:never:) line  25 "cdma-1a.prm" (state 7)	[(1)]
Never claim moves to line 25	[(1)]
 11:	proc  2 (c2) line  94 "cdma-1a.prm" [Recv] SYNC	<- queue 2 (c2_chan)
 11:	proc  2 (c2) line  94 "cdma-1a.prm" (state 4)	[(c2_chan?[SYNC])]
 12:	proc  2 (c2) line  95 "cdma-1a.prm" Recv SYNC	<- queue 2 (c2_chan)
 12:	proc  2 (c2) line  95 "cdma-1a.prm" (state 5)	[c2_chan?SYNC]
««<START OF CYCLE»»>
 13:	proc 0 (NEVER) line   21 "never"
 13:	proc  - (:never:) line  21 "cdma-1a.prm" (state 3)	[(1)]
Never claim moves to line 21	[(1)]
 14:	proc  1 (c1) line  39 "cdma-1a.prm" (state 3)	[(1)]
 15:	proc 0 (NEVER) line   20 "never"
 15:	proc  - (:never:) line  20 "cdma-1a.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 "cdma-1a.prm" Send SYNC	-> queue 2 (c2_chan)
 16:	proc  1 (c1) line  38 "cdma-1a.prm" (state 1)	[c2_chan!SYNC]
 17:	proc 0 (NEVER) line   25 "never"
 17:	proc  - (:never:) line  25 "cdma-1a.prm" (state 7)	[(1)]
Never claim moves to line 25	[(1)]
 18:	proc  2 (c2) line 105 "cdma-1a.prm" [Recv] SYNC	<- queue 2 (c2_chan)
 18:	proc  2 (c2) line 105 "cdma-1a.prm" (state 19)	[(c2_chan?[SYNC])]
 19:	proc  2 (c2) line 106 "cdma-1a.prm" Recv SYNC	<- queue 2 (c2_chan)
 19:	proc  2 (c2) line 106 "cdma-1a.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 "cdma-1a.prm" (state 33)
 19:	proc  1 (c1) line  39 "cdma-1a.prm" (state 3)
 19:	proc  0 (:init:) line 141 "cdma-1a.prm" (state 4) <valid endstate>
 19:	proc 0 (NEVER) line   19 "never"
 19:	proc  - (:never:) line  19 "cdma-1a.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 cdma-1.fsm}, to Promela {\em cdma-1.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 cdma-1b.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 stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.10 -- 15 March 2000)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid endstates       - (disabled by never-claim)

State-vector 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)

Some questions

• What are the changes to the model to include channel losses.

6.2.2  CDMA-RLP - data transfer phase

The non-transparent CDMA-RLP 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. Non-transparent CDMA-RLP 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 CDMA-RLP is as follows:

• CDMA-RLP must send a message every 20ms. This is requirement forced by the speech coders.
• CDMA-RLP counts the number, Es, of successive missing or errored messages. Whwn Es > Em, where Em is an error threshold, the connection is aborted.

A description of the data transfer procedures

This description is in section 3.1.2.1 de IS-702.2.

A Course Project

The project in this course is the development of a Promela model of the data transfer phase, without encryption, of CDMA-RLP, 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 CDMA-RLP IS-707.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 <==>  (a-b+M) %M >= W
   a > b <==>  (b-a+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_r-1 
                        (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_r-1
		   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_r-1
                        (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'.