Standard declarations
E
e
INT
BOOL
STRING
block
DATA
colset DATA = string;
NO
colset NO = int;
NOxDATA
NO
DATA
colset NOxDATA = product NO * DATA;
NO
n
k
var n,k : NO;
DATA
d
data
var d, data : DATA;
BOOL
success
var success : BOOL;
val AllPackets =
1`(1,"COL" )++
1`(2,"OUR")++
1`(3,"ED ")++
1`(4,"PET")++
1`(5,"RI ")++
1`(6,"NET");
val AllPackets =
1`(1,"COL" )++
1`(2,"OUR")++
1`(3,"ED ")++
1`(4,"PET")++
1`(5,"RI ")++
1`(6,"NET");
Packets
To Send
NOxDATA
AllPackets
B
NOxDATA
Data
Received
DATA
1`""
NextSend
NO
1`1
A
NOxDATA
D
NO
C
NO
NextRec
NO
1`1
Send
Packet
Transmit
Packet
Receive
Packet
Transmit
Ack
Receive
Ack
(n,d)
if success
then 1`(n,d)
else empty
(n,d)
if n=k
then data^d
else data
n
(n,d)
(n,d)
if n=k
then k+1
else k
n
if success
then 1`n
else empty
n
n
data
k
if n=k
then k+1
else k
k