A ``Formal'' Promela Model
for CDMA-RLP based on IS707-2

Michael J. Ferguson
INRS-TÚlÚcommunications

Contents

1  Introduction
    1.1  Literate Programming Methodology
    1.2  Some Pragmatics
        1.2.1  Text Editor
        1.2.2  LaTeX as an intermediate documentation language
        1.2.3  PDF documentation
        1.2.4  The choice of a ``literate programming'' program
    1.3  The Model Architecture
2  General program structure and output file
    2.1  Definitions
        2.1.1  Modular Arithmetic
        2.1.2  Definitions of TRUE and FALSE
        2.1.3  System Parameters
    2.2  Channels
    2.3  Global variables
3  MT and BS Promela Model
    3.1  local variables
    3.2  variable initialization
    3.3  mtypes
        3.3.1  initialise send parameters
        3.3.2  check if NAK pending
        3.3.3  if NAK pending - send NAK
        3.3.4  check if retransmission pending
        3.3.5  if retransmission pending - send retransmission
        3.3.6  send new DATA or IDLE
        3.3.7  mtypes
        3.3.8  send IDLE
    3.4  rcv and process next message
        3.4.1  mtypes
        3.4.2  receive message and check channel ABORT
        3.4.3  model message loss and track erasures
        3.4.4  process new received message
        3.4.5  process DATA message
        3.4.6  duplicate message
        3.4.7  next in-order frame with no missing frames
        3.4.8  next in-order frame with missing frames
        3.4.9  test if data valid
        3.4.10  missing old frame
        3.4.11  new data
        3.4.12  process NAK message
        3.4.13  process IDLE message
        3.4.14  increment NAK Counters
    3.5  abort connection
4  init
5  References
6  Index
Index

1  Introduction

1.1  Literate Programming Methodology

This document is a complete Promela/Spin model for CDMA-RLP as described in IS707-2 standard (see ./is707-2.htm). The objectives of this work are to produce a realistic Promela model of the CDMA-RLP standard and to demonstrate a methodology where

The methodology used is a semi-literate and visual version of the ``literate programming'' method of Knuth[4]. In Knuth's approach there is a single master web file that is processed using the program weave to produce a documentation file and is also processed by the program tangle to produce the program file for the compiler. In the approach here, there will be one or more auxilliary documentation files. It is necessary to link the master web file with these external documentation files, which in this case is the IS707-2 standard. The coordinating of the program model and the standard will use HTML hyperlinks and colour.

All current literate programming methodologies alternate the code with the documentation and tend to discourage comments within the code, even though all programming languages allow this. The alternation of documentation/code fragments the visible flow of the program. The use of inline comments can alleviate this somewhat, but if the inline comments too voluminous, the effect on visualising the code flow is similar. In addition to alternating documentation, the approach here embeds hyperlinks in comments in the code.

The method here allows for mixing the two forms of documentation by embedding hyperlinks that point to the relevant document and code sections of the standard.

There are no current systems that allow for all the capabilities listed above. The approach here was to enhance several current systems to create a new system that is capable, with a minimum of pain, to accomplish the above objectives.

1.2  Some Pragmatics

In this section I will discuss the design choices that led to the modified system used for this model. These involved the choice of the literate programming web engine and the underlying typographical engine.

1.2.1  Text Editor

Although my favourite editor is Emacs, I considered a specialised HTML editor, Amaya (http://www.w3.org/Amaya/) for inserting the anchors and links, and the text highlighting that I felt would be needed for the documentation. Amaya, like Acrobat for PDF, has been optimised for setting internal links and anchors. Amaya automatically chooses the names for the anchors and guarantees that these names will be unique. However the names chosen are not necessarily appropriate for external access. It is possible to force Amaya to choose an appropriate name, but I felt the mechanism was not really very convenient. In addition, I did not find a convenient way to highlight text. I feel that highlighting of text is important because it allows the reader to determine immediately what part of the page is actually relevant for the code. I chose to do this here with colour.

Knuth used PlainTeX for formatting his documentation files. He also used a flat, sectionless structure, and formatted the program fragments so they looked nice. This flat, sectionless structure meant that it was difficult to show the gross structure of a program. In addition, nice formatting, for example changing ``&&'' to ``'', made it difficult to recognize textual program expressions in the typeset version. Knuth's version was also programming language dependent. A major advantage of that approach was that it was possible to create an extensive index of all the variables in the program. In 1992 I modified the cweb program of Levy to use all the typesetting capabilities of INRSTeX[1] (eg sections, lists, ...), and in addition modified the typeset ``c'' program fragments to appear more similar to a normal textual ``c'' program. Although it would have been quite easy to convert the grammar from ``c'' to ``Promela'', it would have been almost impossible to convert the INRSTeX file to HTML. The current universal version of TeX is LaTeX.

1.2.2  LaTeX as an intermediate documentation language

LaTeX has a number of advantages as an intermediate documentation language in this context:

1.2.3  PDF documentation

The IS707-2 standard is published as a PDF document. Although it is possible using Adobe Acrobat to link the information within a PDF document to either internal targets (anchors) or external targets, it is impossible to place a named internal target anchor in a PDF document and have that accessible from an external document. This capability seems to only be available in HTML documents. This meant that it was necessary to convert the PDF document to an HTML document. Adobe has a free online web based service that converts the PDF to HTML. However, all the formatting, figures, and tables are lost in the conversion. This form was unacceptable for the model documentation version of the standard because it did not look like the original version. This deficiency would reduce reader confidence that the derived system actually was based on the original standard. For this reason, this HTML version to a version was converted to a LaTeX document that with a format almost identical with the original PDF document. The conversion was possible, and relatively easy, but much more of hack than a production methododology. The method used was as follows:

1.2.4  The choice of a ``literate programming'' program

``Spiderweb''(http://www.tex.ac.uk/tex-archive/web/spiderweb/README) and ``FunnelWeb''(http://www.ross.net/funnelweb/index.shtml) are two well known ``language independent'' literate programming engines. I chose FunnelWeb because it appeared to slightly more minimalist than SpiderWeb. The TeX formatting side of FunnelWeb is PlainTeX oriented and had a number of incompatibilities when converted to LaTeX. FunnelWeb also allows for HTML output, but this output is quite constrained. The only way that it would be possible to get the necessary capabilities is through modifications to FunnelWeb. The version of Funnelweb used here is sufficiently different from the original in details and philosophy that it is not really FunnelWeb. A number of the changes were necessitated by design decision in LaTeX to implement verbatim as a list environment, and the, albeit consistent, translation of this environment into the HTML <pre> environment by TTH. FunnelWeb is run in its TeX formatting mode.

This is a list of, and the reasons for, the major changes that were made to FunnelWeb.

1.3  The Model Architecture

CDMA mobile radio systems, after they have established a physical connection, send frames every 20ms. Since Promela has no concept of real time, this fact is modeled by having the BS (Base Station) and the MT (Mobile Terminal) send a message through a Promela channel and then wait for the arrival of the message from the other side. This arriving message is either processed or modeled as a loss in the channel. Since RLP knows that there should be a complete frame every 20ms, a loss is the channel is referred to as an erasure. After a complete (W-1), where W is the size of the window (W=128 in IS707-2) of consecutive erasures, (127 in IS707-2).

The model in this paper makes the following assumptions:

A discussion of the model structure is give when the Promela processes (proctypes) are given in section 3.

2  General program structure and output file

A Promela model usually has all of the components shown in the output file. The output file is the actual Promela program that is processed by Spin.

1: rlp-vp.prm
{ 
 
definitions 
 mtype={
mtypes}; 
 
channels 
 
global variables 
 
proctypes 
 
init 
 
} This macro is attached to an output file.

2.1  Definitions

2.1.1  Modular Arithmetic

Note that all arithmetic in RLP is modulo MODULUS, where MODULUS=256, for data transfer in IS707-2. The standard defines less than < and greater than > in terms of an effective window of MODULUS/2 = 128. The formula for implementing < and > for an arbitrary window, WINDOW and modulus MODULUS is
a < b <==> (a-b+MODULUS) %MODULUS >=WINDOW
a > b <==> (b-a+MODULUS) %MODULUS > WINDOW ... note that < > are not transitive ...

Only the formula (a<b), lt(a,b), is used in this model and is a Promela definition

2: definitions +
{ 
 #define lt(a,b) ((a-b+MODULUS)%MODULUS>=WINDOW
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

Note that MODULUS=16 and WINDOW=8 in this model is a defined value below.

3: definitions +
{ 
 #define MODULUS 32 
 #define WINDOW 16 /* 1/2 of MODULUS */ 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

2.1.2  Definitions of TRUE and FALSE

TRUE=1 and FALSE =0, consistent with their values in C. 4: definitions +
{ 
 #define TRUE 1 
 #define FALSE 0 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

2.1.3  System Parameters

The values of these parameters are arbitrary and their meaning and use will be indicated in the appropriate section.

5: definitions +
{ 
 #define NO_NAK_PENDING 240 
 #define NO_RESND_PENDING 230 
 #define RESND_PENDING 231 
 #define RLP_DELAY 2 
 #define NAK_SET 4 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

2.2  Channels

There are two channels, one in each direction:

6: channels +
{ 
   chan MT_BS=[SIZE_CH] of {mtype, byte, mtype, byte, byte}; /* RLP -> RLP */ 
   chan BS_MT=[SIZE_CH] of {mtype, byte, mtype, byte, byte}; /* RLP -> RLP */ 
 
} This macro is defined in definitions 6 and 32.
This macro is invoked in definition 1.

Promela channels have a fixed message format so room must be made in the format for message with the most parameters, namely the NAK. The data in each message are snd_msg, snd_seq, snd_data, snd_first, snd_last. Not all message types use all values. The empty value for snd_data is NULL and the empty value for snd_data, snd_first, snd_last is NOVALUE.

7: mtypes +
{ 
 NULL
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

8: definitions +
{ 
 #define NOVALUE 242 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

The channels are of length SIZE_CH=2. Since Promela uses asynchronous interleaving, it is necessary to allow either the Mobile Terminal or Base Station to receive, process, and send a new message before the opposite side processes the previous message.

9: definitions +
{ 
 #define SIZE_CH  2 /* length of channels */ 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

2.3  Global variables

rcv_state[.] is a global variable that models the aborting the connection by the physical layer, either due to detecting especially bad error conditions or in response to an abort request by the RLP layer. rcv_state[.] is initialized to NOVALUE. In this model an aborting of a connection is always due to a request from RLP.

10: global variables
{ 
   byte rcv_state[2];  
 
} This macro is invoked in definition 1.

rcv_state[.]==ABORT is the value when the MT or BS determines that the connection has been broken.

11: definitions +
{ 
 #define ABORT 223 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

3  MT and BS Promela Model

The models of the MT and BS differ only in their ID values

12: definitions +
{ 
 #define MT 0 /* id of Mobile Terminal */ 
 #define BS 1 /* id of Base Station */ 
 
} This macro is defined in definitions 2, 3, 4, 5, 8, 9, 11 and 12.
This macro is invoked in definition 1.

This is the basic structure of the MT and BS processes. Each process has 3 input parameters, the input channel ch_in, the output channel ch_out, and the process id.

13: proctypes
{ 
 proctype rlp(chan ch_inch_out; byte id
 {  
local variables 
   d_step{ 
    
variable initialization 
        } 
  send_next: /* send next message */ 
    
send next message 
    
rcv and process next message 
    goto send_next
    
abort connection 
 } 
 
} This macro is invoked in definition 1.

Although, Spin initializes all Promela variables to 0, it is good programming practise to initialise all variables. The main program loop consists of send next message and rcv and process next message.

3.1  local variables

This is a complete list of the local variables. They will be explained in detail when they are first used. They probably should be declared at first use so as to be certain none are missing.

14: local variables
{ 
     mtype rcv_msgsnd_msg
     byte v_nv_rv_s
 /* v_s sequence # of next new send message */ 
 /* v_r sequence # of next new receive message */ 
 /* v_n sequence # of next in order receive message */ 
     byte rcv_n_srcv_first,  rcv_last
     byte snd_seqsnd_firstsnd_last
     byte snd_data_state=0; 
     byte rcv_data_state=0;  
     mtype snd_datarcv_data
     byte erasure_count
     byte nak_increment
     byte nak[MODULUS]; 
 /* nak[.]  NAK timer and status */ 
     byte nak_set[MODULUS];  
    byte nak_set_inc,nak_set_abort;/* debug variables */ 
 /* nak_set[.]  counts number of successive settings of nak[.] */ 
     mtype  rcv_buffer[MODULUS];  
 /* rcv_buffer[.] rcv data */ 
     mtype snd_buffer[MODULUS]; /* send buffer */ 
     byte resnd_buffer[MODULUS];  
 /* resnd_buffer[.] resend status */ 
  
     byte p1; /* scratch variable */ 
     mtype rcv_msg_status; /* print trace variable */ 
     mtype new_data; /* data value in next new message */ 
 
} This macro is invoked in definition 13.

3.2  variable initialization

This is the initialization all the state variables. Again they will be explained in detail when they are first used.

15: variable initialization +
{ 
     /* variable initialization */ 
     p1=0;  
     do :: (p1<MODULUS); 
            nak[p1]=NO_NAK_PENDING
            nak_set[p1]=0; 
            rcv_buffer[p1]=NULL
            resnd_buffer[p1]=NO_RESND_PENDING
            snd_buffer[p1]=NULL
            p1++ 
        :: (p1==MODULUS); 
            break 
     od; 
     v_s=0; 
     v_r=0; 
     v_n=0; 
     erasure_count=0; 
     nak_increment=0; 
 
} This macro is defined in definitions 15.
This macro is invoked in definition 13.

3.3  mtypes

Non-transparent data transfer in RLP uses three message types NAK, DATA, and IDLE. These three represented as Promela mtypes.

16: mtypes +
{ 
 NAK, /* parameters: V_S, first, last */ 
 DATA, /* parameters: V_S, data */  
 IDLE, /* V_S  */ 
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

RLP has strict priority rules on the order of sending the messages:

  1. NAK messages
  2. messages that need to be retransmitted because of the reception of a NAK
  3. New DATA messages
  4. IDLE messages if there are no DATA messages to send.

17: send next message
{ 
  atomic{ 
   
initialise send parameters 
   
check if NAK pending 
   if :: 
if NAK pending - send NAK 
      :: else -> 
         
check if retransmission pending 
         if :: 
if retransmission pending - send retransmission 
            :: else -> 
                
send new DATA or IDLE 
         fi 
   fi; 
        } 
   if :: (rcv_state[(id+1)%2]!= ABORT) -> /* send message only if 
                                            destination has not aborted */ 
              ch_outsnd_msgsnd_seqsnd_datasnd_firstsnd_last 
      :: else -> goto end_abort 
   fi; 
 
} This macro is invoked in definition 13.

The initial if ... fi; sets the values of the parameters of the sent message. The message is actually sent by ch_out! on the output channel. It is only sent if the destination has not yet aborted.

3.3.1  initialise send parameters

This section initialises the next output message parameters and does so everytime a next is to be sent. snd_msg and snd_data are mtype so the are initialised to the mtype NULL while the other three are byte so they are initialised to the byte value NOVALUE.

18: initialise send parameters
{ 
   snd_msg=NULL
   snd_seq=NOVALUE
   snd_data=NULL
   snd_first=NOVALUE
   snd_last=NOVALUE
 
} This macro is invoked in definition 17.

3.3.2  check if NAK pending

This section determines if a NAK needs to be sent. The array nak[.] holds the status of the NAK counter (timer) for each sequence number. The possible values are

The standard distingushes between a NAK retransmission timer and a NAK abort timer. However, the rules for expiration of each of them is identical. The retransmission timer is allowed to expire twice whereupon it is followed by the abort timer. If the abort timer expires, the connection is aborted. In this model, there is no distinction made of the type of counter. Rather, nak_set[.] records the number of successive times the NAK counter has been set and takes appropriate action. At the first setting of the retransmission counter, one NAK is sent, the second, two NAKs are sent, and at the third, three NAKs are sent. At the fourth setting of the retransmission counter, the connection is aborted.

All of the missing receive message sequence numbers are between the values v_n, the sequence number of next message to be received in order, and v_r, the sequence number of the next new message to be received. The code first sets p1=v_n and looks for the first sequence number that has (nak[p1] > NO_NAK_PENDING but also has (p1, ie lt(p1,v_r). It sets snd_first to this value. The number of unsent NAKs for this sequence number is reduced by one. When the value of nak[p1] drops to NO_NAK_PENDING, nak[p1] is set to 0 for the next count-up to RLP_DELAY. It then continues to increase p1 over a continuous interval where (nak[p1] > NO_NAK_PENDING) is still true. At the first p1 where the assertion fails, it subtracts 1 from p1 and sets snd_last to this value. During the entire interval, it sets the NAK counter to 0. The assert(lt(v_n,p1) || (v_n == p1)); is a sanity check on the code and should never fail. If it does, it says that the NAK interval is larger than the entire receive window.

19: check if NAK pending
{ 
   p1=v_n
   do :: lt(p1,v_r) ->  
         if :: ((nak[p1] > NO_NAK_PENDING)) -> /* first NAK_PENDING */ 
                snd_first=p1
                do :: ((nak[p1] > NO_NAK_PENDING)) ->  
                      /* set NAK timer */ 
                       nak[p1]-; /* reduce # of NAKs needed by 1 */ 
                       if :: (nak[p1] == NO_NAK_PENDING) ->  
                              /* all the outstanding NAKs have been sent */ 
                              nak[p1]=0 
                          :: else -> skip 
                       fi; 
                       p1 = (p1+1)%MODULUS 
                    :: else ->  
                       p1 = (p1+MODULUS-1)%MODULUS
                       assert(lt(v_n,p1|| (v_n == p1)); 
                       snd_last=p1
                       break 
                od; 
                break 
            :: else -> skip 
         fi; 
         p1 = (p1+1)%MODULUS 
      :: else -> break 
   od; 
 
} This macro is invoked in definition 17.

3.3.3  if NAK pending - send NAK

If there is a valid nak_pending interval, then snd_msg is set to be NAK and the snd_seq is set to v_s. Note that if this test is true, then the execution of the if ... fi terminates after these to actions.

20: if NAK pending - send NAK
{ 
  (snd_first != NOVALUE) -> /* send NAK */ 
    snd_msg=NAK
    snd_seq=v_s
 
} This macro is invoked in definition 17.

3.3.4  check if retransmission pending

If there is no NAK to be sent, then we check to see if there is any retransmissions needed. The resend_buffer[.] holds the status of the need of retransmissions. If resend_buffer[p1]==RESND_PENDING, the message with sequence number p1 needs to be resent. After it is sent, the resend_buffer[p1] is set to NO_RESND_PENDING. It is necessary to check all possible sequence numbers in the current send window. The send window is all sequence numbers that are less than v_s, the next new message sequence number. Thus we set p1=(v_s+MODULUS-WINDOW+1)%MODULUS;. We indicate that a retransmission at sequence number p1 is necessary by setting snd_seq=p1.

21: check if retransmission pending
{ 
  p1=(v_s+MODULUS-WINDOW)%MODULUS
  snd_seq=NOVALUE
  do :: lt(p1,v_s) -> 
        if :: (resnd_buffer[p1] == RESND_PENDING) ->  
               snd_seq=p1
               resnd_buffer[snd_seq]=NO_RESND_PENDING
               break 
           :: else -> skip 
        fi; 
        p1 = (p1+1)%MODULUS 
     :: else -> break 
  od; 
 
} This macro is invoked in definition 17.

3.3.5  if retransmission pending - send retransmission

If snd_seq has been set, then additionals retransmission parameters are set. Note that the snd_buffer[p1] holds the data value that was actually sent originally in the message with sequence number p1.

22: if retransmission pending - send retransmission
{ 
     (snd_seq != NOVALUE) -> /* retransmit data */ 
        snd_data=snd_buffer[snd_seq]; 
        snd_msg=DATA  
 
} This macro is invoked in definition 17.

3.3.6  send new DATA or IDLE

If there has not been any snd_msg set, then a non-deterministic choice between a new DATA or IDLE message is sent.

23: send new DATA or IDLE
{ 
 /* send new DATA or IDLE non-deterministic choice */ 
   if :: skip ->  
          
send new_data 
      :: skip ->  
          
send IDLE 
   fi 
 
} This macro is invoked in definition 17.

3.3.7  mtypes

If the non-deterministic choice is to send a new DATA message, then the data for the new message is chosen. The message data is generated using a 3 state machine with three mtypes, W,R,B.

24: mtypes +
{ 
 W
 R
 B
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

Wolper [5] has shown that this simple state machine will test to see if there is any message loss, duplication, or re-ordering in an infinite sequence of messages. See Holzmann ([3], pages 157-159) for a complete discussion. Data is always W.

25: send new_data
{ 
   if :: (snd_data_state == 0) -> 
           if :: new_data = W  
              :: new_data = R
                 snd_data_state = 1 
           fi 
      :: (snd_data_state == 1) -> 
           if :: new_data = W  
              :: new_data = B
               snd_data_state = 2 
           fi 
      :: (snd_data_state == 2) -> 
           new_data = W  
   fi; 
   snd_buffer[v_s]=new_data
   snd_buffer[(v_s+WINDOW)%MODULUS]=NULL
   assert(resnd_buffer[(v_s+WINDOW)%MODULUS]==NO_RESND_PENDING); 
   snd_msg=DATA
   snd_seq=v_s
   snd_data=new_data
      /* remove old data from snd_buffer */ 
   v_s = (v_s+1)%MODULUS 
 
} This macro is invoked in definition 23.

After setting snd_buffer[v_s]=new_data, the data in the snd_buffer for the sequence number that is newly outside the window is set to NULL. The assert(resnd_buffer[(v_s+WINDOW)%MODULUS]==NO_RESND_PENDING); is a sanity check and never should be in error. Finally v_s is incremented.

3.3.8  send IDLE

The sending of a new IDLE message is very simple. It has no data, and its sequence number is v_s. The sequence number is not incremented.

26: send IDLE
{ 
 snd_msg=IDLE
 snd_seq=v_s
 
} This macro is invoked in definition 23.

3.4  rcv and process next message

This is the most complicated part of the model. It starts out by initialising the receive variables. Then the channel is checked to see if the other side has aborted. If it has not, then the first message in the channel is read. Channel loss is then modeled and the number of successive erasures is computed. The process new received message is where the real work is done. Finally, if the received message is new DATA, or IDLE, the NAK counters are incremented.

27: rcv and process next message
{ 
    
initialise rcv variables 
    
receive message and check channel ABORT 
    
model message loss and track erasures 
    
process new received message 
    
increment NAK Counters 
 
} This macro is invoked in definition 13.

3.4.1  mtypes

The first five rcv_... variables here correspond to the snd_... in section 3.3.1. The variable rcv_msg_status is initialised to RCVD.

28: mtypes +
{ 
 RCVD
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

The model sets rcv_msg_status=LOST if the nondeterministic choice of LOSS is made in model message loss and track erasures.

29: initialise rcv variables
{ 
   rcv_msg=NULL
 d_step{ 
   rcv_n_s=NOVALUE
   rcv_data=NULL
   rcv_first=NOVALUE
   rcv_last=NOVALUE
   rcv_msg_status=RCVD;  
       } 
 
} This macro is invoked in definition 27.

3.4.2  receive message and check channel ABORT

It is possible that the other side will abort and there will be nothing in the channel. If the other side has aborted, there is no reason to continue. This test blocks if there is no message in the channel and the other side has not aborted. This blocking, models the wait for the corresponding message, each 20ms, from the other side.

30: receive message and check channel ABORT
{ 
   if ::  ch_inrcv_msgrcv_n_srcv_datarcv_firstrcv_last 
      :: (rcv_state[(id+1)%2] == ABORT) -> goto end_abort 
   fi; 
 
} This macro is invoked in definition 27.

3.4.3  model message loss and track erasures

If there is a message in the channel and the other side has not aborted, then a non-deterministic choice is made for losing (erasing) the message. If the message is lost, then the erasure_count is incremented. When (erasure_count==WINDOW), the connection is aborted. In addition, the channel LOSS is used to record the loss of messages. This is added so an error trace by Spin will clearly show when a message was LOST. When Spin searches the state graph, it always starts on the first choice. This model prefers no-loss to loss.

31: model message loss and track erasures
{ 
 atomic{ 
   if :: skip; erasure_count=0 
      :: erasure_count++;  
         if :: (erasure_count==WINDOW) -> 
                goto end_abort 
            :: (erasure_count<WINDOW) -> 
                skip 
            :: else -> assert(0) 
         fi;  
         printf("Erasure: %d id: %d\n", erasure_count,id); 
          /* send!/rcv? in LOSS channel must be atomic */ 
         LOSSLOSTrcv_msgrcv_n_s;  
         LOSSLOSTrcv_msgrcv_n_s
         rcv_msg_status=LOST
         goto send_next 
   fi; 
       } 
 
} This macro is invoked in definition 27.

The channel LOSS and the mtype LOST is now added.

32: channels +
{ 
   chan LOSS=[1] of {mtype, mtype, byte};  
 
} This macro is defined in definitions 6 and 32.
This macro is invoked in definition 1.

The special message LOST is

33: mtypes +
{ 
 LOST
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

3.4.4  process new received message

The arrival of a new message may require incrementing the NAK counter. If this is the case, nak_increment is set TRUE. It is initialised FALSE.

34: process new received message
{ 
 atomic{ 
   nak_increment=FALSE
   if :: (rcv_msg==DATA) ->  
           
process DATA message 
      :: (rcv_msg==IDLE) ->  
           
process IDLE message 
      :: (rcv_msg==NAK) ->  
           
process NAK message 
   fi; 
       } 
 
} This macro is invoked in definition 27.

3.4.5  process DATA message

The processing of DATA messages is central to the protocol. The nak[rcv_n_s] is set to NO_NAK_PENDING. This will be correct even if this is a duplicate. The duplicate message tests (rcv_n_s >= v_n) if the message is in the current receive window. If it is in the window further processing occurs. The various cases are discussed below.

35: process DATA message
{ 
   nak[rcv_n_s]=NO_NAK_PENDING; /* reset NAK counters even */ 
   nak_set[rcv_n_s]=0;        /*   if discarded */ 
  
   if :: 
duplicate message 
      :: else ->  
          if :: 
next in-order frame with no missing frames 
                 
             :: 
next in-order frame with missing frames 
  
             :: 
missing old frame 
  
             :: 
new data 
             :: else -> assert(0) 
          fi 
   fi                   
 
} This macro is invoked in definition 34.

3.4.6  duplicate message

If the received message sequence number rcv_n_s, is less than v_n, it means that this is a duplicate and that this data has already been sent to layer 3. The data is discarded, and a message, DISCARD, is sent to the LOSS channel so the discard action will show up on a Spin trace.

36: duplicate message
{ 
 lt(rcv_n_s,v_n) ->  
           /* rcv_n_s < v_n  */ 
            LOSSDISCARDrcv_msgrcv_n_s;  
            LOSSDISCARD,rcv_msgrcv_n_s
            rcv_msg_status=DISCARD
            skip /* discard */ 
 
} This macro is invoked in definition 35.

The new message DISCARD is added to the .

37: mtypes +
{ 
 DISCARD
 
} This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.

3.4.7  next in-order frame with no missing frames

In this case there is no missing data frames, (v_r == v_n), and the received sequence number, (rcv_n_s == v_n). The data in the frame is passed to layer 3, v_n and v_r are incremented.

38: next in-order frame with no missing frames
{ 
 ((v_r == v_n) && (rcv_n_s == v_n)) -> 
 /* pass rcv_data to layer 3 */ 
    rcv_buffer[v_n]=rcv_data
    
test if data valid 
    rcv_buffer[v_n]=NULL
    v_r = (v_r+1)%MODULUS
    v_n = (v_n+1)%MODULUS
    nak_increment = TRUE
 
} This macro is invoked in definition 35.

3.4.8  next in-order frame with missing frames

In this case, there are missing data frames, (v_n < v_r), but the received data frame is the next one in order, (v_n == rcv_n_s). The action is similar to the previous case but here all data in contiguous frames are passed up to layer 3, and v_n becomes the next missing frame.

39: next in-order frame with missing frames
{ 
 ((v_r != v_n) && (rcv_n_s == v_n))->  
    /* next in order data */ 
    rcv_buffer[rcv_n_s]=rcv_data
    /* pass data to layer 3 and update v_n */ 
    do 
       :: (rcv_buffer[v_n] != NULL) -> 
         
test if data valid 
           rcv_buffer[v_n]=NULL
           /* simulate sending to layer 3 by  
    NULL insertion */ 
           assert(lt(v_nv_r)); /* sanity test of code */ 
           v_n = (v_n+1)%MODULUS 
       :: else ->  break 
    od; 
 
} This macro is invoked in definition 35.

3.4.9  test if data valid

When data is passed to layer 3, it is checked to see if it is contained in W*RW*BWw language that was defined by Wolper and used for the data generation (see section 3.3.7.) A simple 3 state machine is defined with an assertion violation, assert(0), if the data is invalid. In all cases, the data being passed to layer 3 has the sequence number v_n. Data is always W.

40: test if data validM
{ 
   if :: (rcv_data_state == 0) -> 
          if :: (rcv_buffer[v_n] == W) ->  
                  skip 
             :: (rcv_buffer[v_n] == R) -> 
                  rcv_data_state = 1 
             :: else -> assert(0) 
          fi 
      :: (rcv_data_state == 1) -> 
          if :: (rcv_buffer[v_n] == W) -> 
                  skip 
             :: (rcv_buffer[v_n] == B) -> 
                  rcv_data_state = 2 
             :: else -> assert(0) 
          fi 
      :: (rcv_data_state == 2) -> 
          if :: (rcv_buffer[v_n] == W
             :: else -> assert(0) 
          fi  
   fi;  
 
} This macro is invoked in definition 38 and 39.

3.4.10  missing old frame

If the new frame is between the next in-order frame, v_n and v_r, and it is not a duplicate, it is placed in the receive buffer, rcv_buffer[rcv_n_s]. If it is a duplicate, the data in the frame is checked to see if it has the same value.

41: missing old frame
{ 
 ((v_r != v_n) && lt(v_nrcv_n_s)  
        && lt(rcv_n_sv_r)) -> 
  /* check duplicate values equal */ 
    if :: (rcv_buffer[rcv_n_s] != NULL) ->  
             assert(rcv_buffer[rcv_n_s]==rcv_data
       :: else -> 
            rcv_buffer[rcv_n_s]=rcv_data 
    fi 
 
} This macro is invoked in definition 35.

3.4.11  new data

If the frame is new and there are missing frames, then the NAK counters must be incremented, and a new NAK for the missing frames needs be sent. The test here is quite complicated. This test allows for (v_r == v_n) and strictly tests, in this case whether (v_r < rcv_n_s). If (v_n < v_r), then the test is whether (v_r <= rcv_n_s). Since this is a new data frame the NAK counters must be incremented. This is indicated by setting nak_increment=TRUE and setting the NAK counters for all the new missing frames to NAK_PENDING. The NAK counters are processed in section 3.4.14.

42: new data
{ 
 (((v_r == v_n) && lt(v_rrcv_n_s)) 
      || ((v_r != v_n) && (lt(v_rrcv_n_s)  
         || (v_r == rcv_n_s)))) ->  
   rcv_buffer[rcv_n_s]=rcv_data
   nak_increment=TRUE
   do :: lt(v_rrcv_n_s) -> 
          nak_set[v_r]=1; 
          nak[v_r]=NO_NAK_PENDING + nak_set[v_r]; 
          v_r = (v_r+1)%MODULUS 
      :: else -> 
          assert(v_r == rcv_n_s); /* model sanity check */ 
          v_r = (rcv_n_s+1)%MODULUS
          break 
   od 
 
} This macro is invoked in definition 35.

3.4.12  process NAK message

Note that the effective send window of this protocol are all sequence numbers that are less than the current upper edge of the window, v_s. The standard notes that if the either rcv_first or rcv_last is not in the send window, the connection must be ABORTed. When the NAK interval is in the window, the resnd_buffer[.] from rcv_first to rcv_last is set to RESND_PENDING.

43: process NAK message
{ 
 /* parameters rcv_n_s, rcv_first, rcv_last */ 
   if :: (!(lt(rcv_first,v_s) && lt(rcv_last,v_s))) -> 
          goto end_abort 
      :: else ->  
   fi; 
 /* set new retransmissions */ 
   do  
      :: (lt(rcv_firstrcv_last)  
           || (rcv_first ==  rcv_last)) -> 
          resnd_buffer[rcv_first] = RESND_PENDING
          rcv_first = (rcv_first+1)%MODULUS 
      :: else -> break 
   od 
 
} This macro is invoked in definition 34.

3.4.13  process IDLE message

The processing of the IDLE message is surprisingly difficult. The standard says However, this is misleading for in another part of the standard, it says that the NAK counters must be incremented. The processing of an IDLE is essentially identical to a new DATA frame.

44: process IDLE message
{ 
   if :: lt(rcv_n_s,v_n) ->  
          /* rcv_n_s < v_n  - error condition  
              probably should be v_r rather than v_n  
            - should probably abort*/ 
          LOSSDISCARDrcv_msgrcv_n_s;  
          LOSSDISCARD,rcv_msgrcv_n_s
          skip /* silently discard */ 
      :: else ->  
          if :: (lt(v_rrcv_n_s|| (v_r == rcv_n_s)) -> 
               /* increment active NAK counters */ 
                 nak_increment = TRUE
               /* set NAK_PENDING for all new missing data  
                     and update v_r */ 
                 do :: lt(v_rrcv_n_s) -> 
                        assert(rcv_buffer[v_r] == NULL); 
                        nak_set[v_r]=1; 
                        nak[v_r]=NO_NAK_PENDING + nak_set[v_r]; 
                        v_r = (v_r+1)%MODULUS 
                    :: else ->  
                        assert(v_r == rcv_n_s);  
                        break 
                 od 
              :: else -> skip 
          fi 
   fi 
 
} This macro is invoked in definition 34.

3.4.14  increment NAK Counters

If the DATA is new or it is valid IDLE message, the NAK counters should be updated.

45: increment NAK Counters
{ 
   if :: (nak_increment == TRUE) -> 
          p1=0; 
          do  
             :: (p1 < MODULUS) ->  
                  if :: (nak[p1] < RLP_DELAY) -> nak[p1]++ 
                     :: (nak[p1] == RLP_DELAY) ->  
                          nak_set[p1]++; nak_set_inc = 1;  
                          if :: (nak_set[p1] == NAK_SET) -> 
                                 nak_set_abort=1; /* if we abort this way*/ 
                                 printf("NAK_ABORT\n"); 
                                 goto end_abort 
                             :: else ->printf("NAK_TIMEOUT: %d p1:%d\n",nak_set[p1],p1);  
                                nak[p1] = NO_NAK_PENDING + nak_set[p1
                          fi 
                     :: else -> skip 
                  fi; 
                  p1++ 
             :: (p1 == MODULUS) -> break 
             :: else -> assert(0) 
          od; 
      :: else -> skip   
   fi; 
 
} This macro is invoked in definition 27.

3.5  abort connection

46: abort connection
{ 
    end_abortrcv_state[id]=ABORT;  
 
} This macro is invoked in definition 13.

4  init

The initialiser process, init, is

47: init
{ 
 init {atomic { run rlp(MT_BS,BS_MT,BS);  
     run rlp(BS_MT,MT_BS,MT)}}                
 
} This macro is invoked in definition 1.

5  References

References

[1]
Ferguson, M. J. INRSTEX: a document preparation system for multiple languages. In TEX for Scientific Documentation, Second European Conference (Strasbourg, France, jun 1986), pp. 74-88.

[2]
Goossens, M., Mittelbach, F., and Samarin, A. The Latex Companion. Addison-Wesley, Reading, Massachusetts, 1993.

[3]
Holzmann, G. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, NJ, 1991.

[4]
Knuth, D. Literate programming. CSLI Lecture Notes Number 27, Stanford University Center for the Study of Language and Information, Stanford, CA, 1992.

[5]
Wolper, P. Specifying interesting properties of programs in propositional temporal logic. In Proc. 22nd IEEE Symposium on Foundations of Computer Science (St. Petersburg Beach, Fla., jan 1986), IEEE, IEEE.

6  Index

Index (showing section)

a, 2-1
ABORT, 2-3, 3-3, 3-4, 3-5

B, 3-3, 3-4
b, 2-1
BS, 1-3, 3-0, 4-0
BS_MT, 2-2, 4-0

ch_in, 3-0, 3-4
ch_out, 3-0, 3-3

d, 3-4
DATA, 3-3, 3-4
DISCARD, 3-4

end_abort, 3-3, 3-4, 3-5
erasure_count, 3-1, 3-2, 3-4

FALSE, 2-1, 3-4

id, 3-0, 3-3, 3-4, 3-5
IDLE, 3-3, 3-4
init, 4-0
LOSS, 3-4
LOST, 3-4
lt(a,b), 2-1

macros
     definition
         abort connection, 3-5
         channels, 2-2, 3-4
         check if NAK pending, 3-3
         check if retransmission pending, 3-3
         definitions, 2-1, 2-2, 2-3, 3-0
         duplicate message, 3-4
         global variables, 2-3
         if NAK pending - send NAK, 3-3
         if retransmission pending - send retransmission, 3-3
         increment NAK Counters, 3-4
         init, 4-0
         initialise rcv variables, 3-4
         initialise send parameters, 3-3
         local variables, 3-1
         missing old frame, 3-4
         model message loss and track erasures, 3-4
         mtypes, 2-2, 3-3, 3-4
         new data, 3-4
         next in-order frame with missing frames, 3-4
         next in-order frame with no missing frames, 3-4
         process DATA message, 3-4
         process IDLE message, 3-4
         process NAK message, 3-4
         process new received message, 3-4
         proctypes, 3-0
         rcv and process next message, 3-4
         receive message and check channel ABORT, 3-4
         rlp-vp.prm, 2-0
         send IDLE, 3-3
         send new DATA or IDLE, 3-3
         send new_data, 3-3
         send next message, 3-3
         test if data valid, 3-4
         variable initialization, 3-2
     used
         abort connection, 3-0
         channels, 2-0
         check if NAK pending, 3-3
         check if retransmission pending, 3-3
         definitions, 2-0
         duplicate message, 3-4
         global variables, 2-0
         if NAK pending - send NAK, 3-3
         if retransmission pending - send retransmission, 3-3
         increment NAK Counters, 3-4
         init, 2-0
         initialise rcv variables, 3-4
         initialise send parameters, 3-3
         local variables, 3-0
         missing old frame, 3-4
         model message loss and track erasures, 3-4
         mtypes, 2-0
         new data, 3-4
         next in-order frame with missing frames, 3-4
         next in-order frame with no missing frames, 3-4
         process DATA message, 3-4
         process IDLE message, 3-4
         process NAK message, 3-4
         process new received message, 3-4
         proctypes, 2-0
         rcv and process next message, 3-0
         receive message and check channel ABORT, 3-4
         send IDLE, 3-3
         send new DATA or IDLE, 3-3
         send new_data, 3-3
         send next message, 3-0
         test if data valid, 3-4
         variable initialization, 3-0
MODULUS, 2-1, 3-1, 3-2, 3-3, 3-4
MT, 1-3, 3-0, 4-0
MT_BS, 2-2, 4-0
NAK, 3-3, 3-4
nak, 3-1, 3-2, 3-3, 3-4
nak_increment, 3-1, 3-2, 3-4
NAK_SET, 2-1, 3-4
nak_set, 3-1, 3-2, 3-4
nak_set_abort, 3-1, 3-4
nak_set_inc, 3-1, 3-4
new_data, 3-1, 3-3
NO_NAK_PENDING, 2-1, 3-2, 3-3, 3-4
NO_RESND_PENDING, 2-1, 3-2, 3-3
NOVALUE, 2-2, 3-3, 3-4
NULL, 2-2, 3-2, 3-3, 3-4

p1, 3-1, 3-2, 3-3, 3-4
proctype, 3-0

R, 3-3, 3-4
rcv_buffer, 3-1, 3-2, 3-4
rcv_data, 3-1, 3-4
rcv_data_state, 3-1, 3-4
rcv_first, 3-1, 3-4
rcv_last, 3-1, 3-4
rcv_msg, 3-1, 3-4
rcv_msg_status, 3-1, 3-4
rcv_n_s, 3-1, 3-4
rcv_state, 2-3, 3-3, 3-4, 3-5
RCVD, 3-4
resnd_buffer, 3-1, 3-2, 3-3, 3-4
RESND_PENDING, 2-1, 3-3, 3-4
RLP_DELAY, 2-1, 3-4
send_next, 3-0, 3-4
SIZE_CH, 2-2
snd_buffer, 3-1, 3-2, 3-3
snd_data, 3-1, 3-3
snd_data_state, 3-1, 3-3
snd_first, 3-1, 3-3
snd_last, 3-1, 3-3
snd_msg, 3-1, 3-3
snd_seq, 3-1, 3-3

TRUE, 2-1, 3-4

v_n, 3-1, 3-2, 3-3, 3-4
v_r, 3-1, 3-2, 3-3, 3-4
v_s, 3-1, 3-2, 3-3, 3-4

W, 3-3, 3-4
WINDOW, 2-1, 3-3, 3-4




File translated from TEX by TTH, version 3.01.
On 3 Oct 2001, 09:34.