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.
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.
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.
LaTeX has a number of advantages as an intermediate documentation language in this context:
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:
``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.
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.
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.
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.
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.
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.
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.
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.
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_in, ch_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.
14: local variables º
{
mtype rcv_msg, snd_msg;
byte v_n, v_r, v_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_s, rcv_first, rcv_last;
byte snd_seq, snd_first, snd_last;
byte snd_data_state=0;
byte rcv_data_state=0;
mtype snd_data, rcv_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.
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.
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.
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_out! snd_msg, snd_seq, snd_data, snd_first, snd_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.
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.
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
19: check if NAK pending º
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 º
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 º
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 º
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 º
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 + º
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 º
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.
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 º
27: rcv and process next message º
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 + º
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 º
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 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 º
The channel LOSS and the mtype LOST is now added.
32: channels + º
The special message LOST is
33: mtypes + º
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 º
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 º
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 º
The new message DISCARD is added to the
37: mtypes + º
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 º
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 º
40: test if data validM º
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 º
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 º
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 º
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 the DATA is new or it is valid IDLE message, the
NAK counters should be updated.
45: increment NAK Counters º
The initialiser process, init, is
47: init º
{
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
{
(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
{
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
{
(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
{
/* 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
{
W,
R,
B,
}
This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.
{
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.
3.3.8 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.
{
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
{
RCVD,
}
This macro is defined in definitions 7, 16, 24, 28, 33 and 37.
This macro is invoked in definition 1.
{
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
{
if :: ch_in? rcv_msg, rcv_n_s, rcv_data, rcv_first, rcv_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
{
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 */
LOSS! LOST, rcv_msg, rcv_n_s;
LOSS? LOST, rcv_msg, rcv_n_s;
rcv_msg_status=LOST;
goto send_next
fi;
}
}
This macro is invoked in definition 27.
{
chan LOSS=[1] of {mtype, mtype, byte};
}
This macro is defined in definitions 6 and 32.
This macro is invoked in definition 1.
{
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
{
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
{
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
{
lt(rcv_n_s,v_n) ->
/* rcv_n_s < v_n */
LOSS! DISCARD, rcv_msg, rcv_n_s;
LOSS? DISCARD,rcv_msg, rcv_n_s;
rcv_msg_status=DISCARD;
skip /* discard */
}
This macro is invoked in definition 35.
{
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
{
((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
{
((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_n, v_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.
{
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
{
((v_r != v_n) && lt(v_n, rcv_n_s)
&& lt(rcv_n_s, v_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
{
(((v_r == v_n) && lt(v_r, rcv_n_s))
|| ((v_r != v_n) && (lt(v_r, rcv_n_s)
|| (v_r == rcv_n_s)))) ->
rcv_buffer[rcv_n_s]=rcv_data;
nak_increment=TRUE;
do :: lt(v_r, rcv_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
{
/* 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_first, rcv_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
{
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*/
LOSS! DISCARD, rcv_msg, rcv_n_s;
LOSS? DISCARD,rcv_msg, rcv_n_s;
skip /* silently discard */
:: else ->
if :: (lt(v_r, rcv_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_r, rcv_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 :: (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_abort: rcv_state[id]=ABORT;
}
This macro is invoked in definition 13.
4 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
6 Index
Index (showing section)
File translated from
TEX
by
TTH,
version 3.01.
On 3 Oct 2001, 09:34.