----------------------------------------------------------------------
-- Filename: i.m
-- Content: i-protocol
-- Version: Murphi 3.0
-- Author: translate to Murphi by Yifei Dong, 1998
----------------------------------------------------------------------
CONST
WindowSize : 2;
MaxSequence : 2*WindowSize - 1;
fixed : true;
candrop : true;
cancorrupt : true;
TYPE
SequenceNumber : 0..MaxSequence;
PacketType : ENUM {
DATA,
ACK,
NAK
};
Packet : RECORD
pty : PacketType;
seq : SequenceNumber;
ack : SequenceNumber;
END;
Channel : RECORD
full : boolean;
herr : boolean; -- negative of checksum
derr : boolean; -- convenient for CLEAR
body : Packet;
END;
ChanID : 0..1;
SenderState : ENUM {
S_START,
S_SENDMSG_1,
S_SENDMSG_2,
S_SENDMSG_3,
S_TIMEOUT_1,
S_GETPKT_1
};
ReceiverState : ENUM {
R_START,
R_GETPKT_1,
R_GETPKT_2,
R_GETPKT_3,
R_GETPKT_31,
R_GETPKT_4,
R_TIMEOUT_1
};
Action : ENUM {
tau,
lsend,
rrecv,
drop,
corrupt,
timeout,
progress
};
VAR
-- Channels
Channels : array [ChanID] of Channel;
-- Sender states
SState : SenderState;
SNext : SenderState;
SSendSeq : SequenceNumber;
SRack : SequenceNumber;
Sseq : SequenceNumber;
-- Receiver states
RState : ReceiverState;
RSendSeq : SequenceNumber;
RRecSeq : SequenceNumber;
RLack : SequenceNumber;
RRack : SequenceNumber;
RNakd : array[SequenceNumber] of boolean;
RRecBuf : array[SequenceNumber] of boolean;
Rseq : SequenceNumber;
Rtmp : SequenceNumber;
-- test variables
action : Action;
----------------------------------------------------------------------
---------------- Arithmetic Functions ------------------------------
----------------------------------------------------------------------
FUNCTION inc(s: SequenceNumber) : SequenceNumber;
BEGIN
IF s < MaxSequence THEN
RETURN s+1;
ELSE
RETURN 0;
END;
END;
FUNCTION sub(s1, s2: SequenceNumber) : SequenceNumber;
BEGIN
IF s1 >= s2 THEN
RETURN s1-s2;
ELSE
RETURN MaxSequence + 1 + s1 - s2;
END;
END;
FUNCTION in_open_interval(s, l, r: SequenceNumber) : boolean;
BEGIN
RETURN s != l & sub(l,s) <= WindowSize & sub(s,r) <= WindowSize;
END;
----------------------------------------------------------------------
---------- Formula monitor -----------------------------------------
----------------------------------------------------------------------
PROCEDURE observe(a: Action);
BEGIN
action := a;
END;
----------------------------------------------------------------------
---------------- Communication Functions ---------------------------
----------------------------------------------------------------------
FUNCTION isfull(Chan: Channel) : boolean;
BEGIN
return Chan.full;
END;
FUNCTION isempty(Chan: Channel) : boolean;
BEGIN
return ! Chan.full;
END;
PROCEDURE input(VAR Chan: Channel; VAR Hck, Dck: boolean; VAR Pak: Packet);
BEGIN
assert(isfull(Chan));
Pak := Chan.body;
Hck := ! Chan.herr;
Dck := ! Chan.derr;
CLEAR Chan;
END;
PROCEDURE output(VAR Chan: Channel; Pty: PacketType; Seq, Ack: SequenceNumber);
BEGIN
assert(isempty(Chan));
Chan.body.pty := Pty;
Chan.body.seq := Seq;
Chan.body.ack := Ack;
Chan.full := true;
Chan.herr := false;
Chan.derr := false;
END;
----------------------------------------------------------------------
---------------- Processes Data and Ack Channels -------------------
----------------------------------------------------------------------
RULESET n:ChanID DO
ALIAS Chan: Channels[n] DO
RULE "channel drop message"
isfull(Chan) & candrop
==>
BEGIN
Chan.full := false;
CLEAR Chan;
observe(drop);
END;
RULE "channel corrupt message header"
isfull(Chan) & cancorrupt & ! Chan.herr
==>
BEGIN
Chan.herr := true;
observe(corrupt);
END;
RULE "channel corrupt message data"
isfull(Chan) & cancorrupt & ! Chan.derr
==>
BEGIN
Chan.derr := true;
observe(corrupt);
END;
ENDALIAS;
ENDRULESET;
----------------------------------------------------------------------
ALIAS DataChan:Channels[0]; AckChan: Channels[1] DO
----------------------------------------------------------------------
----------------------------------------------------------------------
---------------- Process Sender ------------------------------------
----------------------------------------------------------------------
RULE "sender send message"
SState = S_START
==>
BEGIN
observe(lsend);
SState := S_SENDMSG_1;
END;
RULE "sender sendmsg 1"
SState = S_SENDMSG_1
==>
BEGIN
IF (sub(SSendSeq, SRack) > WindowSize) | (SSendSeq = SRack) THEN
SState := S_SENDMSG_3;
SNext := S_SENDMSG_1;
ELSE
SState := S_SENDMSG_2;
END;
observe(tau);
END;
RULE "sender sendmsg 2"
SState = S_SENDMSG_2 &
isempty(DataChan)
==>
BEGIN
output(DataChan, DATA, SSendSeq, 0);
SSendSeq := inc(SSendSeq);
SState := S_START;
SNext := S_START;
observe(tau);
END;
RULE "sender timeout"
(SState = S_START | SState = S_SENDMSG_3) &
isempty(DataChan)
==>
BEGIN
IF SState = S_START THEN
observe(progress); -- arbitary timeout as progress
ELSE
observe(timeout);
END;
output(DataChan, NAK, 1, 0);
IF SSendSeq != inc(SRack) THEN
SState := S_TIMEOUT_1;
ELSE
SState := SNext;
END;
END;
RULE "sender timeout 1"
SState = S_TIMEOUT_1
& isempty(DataChan)
==>
BEGIN
output(DataChan, DATA, inc(SRack), 0);
SState := SNext;
observe(tau);
END;
RULE "sender getpkt"
( SState = S_START | SState = S_SENDMSG_3) &
isfull(AckChan)
==>
VAR
hck : boolean;
dck : boolean;
pak : Packet;
BEGIN
SState := SNext;
input(AckChan, hck, dck, pak);
IF hck THEN
IF in_open_interval(pak.ack, SSendSeq, SRack) THEN
SRack := pak.ack;
ENDIF;
IF pak.pty = NAK THEN
IF in_open_interval(pak.seq, SSendSeq, SRack) THEN
Sseq := pak.seq;
SState := S_GETPKT_1;
ENDIF;
ENDIF;
ENDIF;
observe(tau);
END;
RULE "sender getpkt 1" -- output
SState = S_GETPKT_1 &
isempty(DataChan)
==>
BEGIN
output(DataChan, DATA, Sseq, 0);
SState := SNext;
observe(tau);
END;
----------------------------------------------------------------------
---------------- Process Receiver ----------------------------------
----------------------------------------------------------------------
RULE "receiver getpkt"
(RState = R_START | RState = R_TIMEOUT_1) &
isfull(DataChan)
==>
VAR
hck : boolean;
dck : boolean;
pak : Packet;
tmp : SequenceNumber;
BEGIN
-- set default action and state
observe(tau);
RState := R_START;
input(DataChan, hck, dck, pak);
IF hck THEN
-- handle-ack
-- proti.vpl: don't updaterack because rack === 0
/*
IF in_open_interval(pak.ack, RRack, RSendSeq) THEN
RRack := pak.ack;
END;
*/
SWITCH pak.pty
CASE DATA:
-- handle_data
IF sub(pak.seq, RLack) <= WindowSize
& pak.seq != RLack THEN
IF dck = false THEN
IF pak.seq != RRecSeq |
RRecBuf[pak.seq] |
RNakd[pak.seq] THEN
RState := R_GETPKT_1;
Rseq := pak.seq;
ENDIF;
ELSE -- dck = true
RNakd[pak.seq] := false;
IF pak.seq = inc(RRecSeq) THEN
-- expected sequence number
RRecSeq := inc(RRecSeq);
-- usr-recv!*;
observe(rrecv);
tmp := inc(RRecSeq);
WHILE RRecBuf[tmp] DO
RRecSeq := tmp;
-- usr-recv!*;
observe(rrecv);
RRecBuf[tmp] := false;
tmp := inc(tmp);
ENDWHILE;
IF sub(pak.seq, RLack) >= WindowSize/2 THEN
RState := R_GETPKT_2;
Rseq := pak.seq;
ENDIF;
ELSIF pak.seq != RRecSeq &
!RRecBuf[pak.seq] THEN
RRecBuf[pak.seq] := true;
tmp := inc(RRecSeq);
IF tmp != pak.seq THEN
Rtmp := tmp;
Rseq := pak.seq;
RState := R_GETPKT_3;
ENDIF;
ENDIF; -- pak.seq = inc(RRecSeq)
ENDIF; -- dck = false
ENDIF; --
-- CASE ACK: skip
CASE NAK:
-- handle_nak fix
IF fixed & (pak.seq = RSendSeq)
& (inc(RRack) = RSendSeq) THEN
RState := R_GETPKT_4;
ENDIF;
ENDSWITCH; -- pak.pty
ENDIF; -- hck
END;
RULE "receiver getpkt 1"
RState = R_GETPKT_1 &
isempty(AckChan)
==>
BEGIN
output(AckChan, NAK, Rseq, RRecSeq);
RLack := RRecSeq;
RNakd[Rseq] := true;
CLEAR Rseq;
RState := R_START;
observe(tau);
END;
RULE "receiver getpkt 2"
RState = R_GETPKT_2 &
isempty(AckChan)
==>
BEGIN
output(AckChan, ACK, Rseq, RRecSeq);
RLack := RRecSeq;
CLEAR Rseq;
RState := R_START;
observe(tau);
END;
RULE "receiver getpkt 3"
RState = R_GETPKT_3
==>
BEGIN
IF !RNakd[Rtmp] & !RRecBuf[Rtmp] THEN
RState := R_GETPKT_31;
ELSE
Rtmp := inc(Rtmp);
WHILE Rtmp != Rseq & (RNakd[Rtmp] | RRecBuf[Rtmp]) DO
Rtmp := inc(Rtmp);
ENDWHILE;
IF Rtmp = Rseq THEN
CLEAR Rtmp;
CLEAR Rseq;
RState := R_START;
ELSE
RState := R_GETPKT_31;
ENDIF;
ENDIF;
observe(tau);
END;
RULE "receiver getpkt 31"
RState = R_GETPKT_31 &
isempty(AckChan)
==>
BEGIN
output(AckChan, NAK, Rtmp, RRecSeq);
RLack := RRecSeq;
RNakd[Rtmp] := true;
Rtmp := inc(Rtmp);
IF Rtmp = Rseq THEN
CLEAR Rtmp;
CLEAR Rseq;
RState := R_START;
ELSE
RState := R_GETPKT_3;
ENDIF;
observe(tau);
END;
RULE "receiver getpkt 4"
RState = R_GETPKT_4 &
isempty(AckChan)
==>
BEGIN
output(AckChan, ACK, RRecSeq, RRecSeq);
RLack := RRecSeq;
RState := R_START;
observe(tau);
END;
RULE "receiver timeout"
RState = R_START &
isfull(DataChan)
==>
BEGIN
-- FORALL s: SequenceNumber DO
-- RNakd[s] := false;
-- END;
CLEAR RNakd;
RState := R_TIMEOUT_1;
observe(progress);
END;
RULE "receiver timeout 2"
RState = R_TIMEOUT_1 &
isempty(AckChan)
==>
VAR
Seq : SequenceNumber;
BEGIN
Seq := inc(RRecSeq);
output(AckChan, NAK, Seq, RRecSeq);
RNakd[Seq] := true;
RLack := RRecSeq;
RState := R_START;
observe(tau);
END;
----------------------------------------------------------------------
---------------- Liveness requirements -----------------------------
----------------------------------------------------------------------
/*
LIVENESS "data channel is active"
ALWAYS EVENTUALLY isfull(DataChan);
LIVENESS "ack channel is active"
ALWAYS EVENTUALLY isfull(AckChan);
*/
LIVENESS "no livelock"
ALWAYS EVENTUALLY (action != tau & action != timeout);
----------------------------------------------------------------------
ENDALIAS;
----------------------------------------------------------------------
STARTSTATE
-- channel states
CLEAR Channels;
-- sender states
SState := S_START;
SNext := S_START;
SSendSeq := 1;
SRack := 0;
CLEAR Sseq;
-- receiver states
RState := R_START;
RSendSeq := 1;
RRecSeq := 0;
RLack := 0;
RRack := 0;
-- FORALL s:SequenceNumber DO
-- RNakd[s] := false;
-- RRecBuf[s] := false;
-- END;
CLEAR RNakd;
CLEAR RRecBuf;
CLEAR Rseq;
CLEAR Rtmp;
-- test variables
action := tau;
END;