--- First exercise, sliding window protocol using an unreliable and unordered
--- communication medium. I'm borrowing a bit of the "first protocol" from the
--- lecture notes. Unlimited number of sequence numbers.
load full-maude
--- First the message types: (lecture notes)
(omod MESSAGES is protecting STRING .
sort MsgContent .
subsort String < MsgContent . --- our "main" messages are just strings!
op ack : -> MsgContent [ctor] . --- acknowledgment message
--- sequence number wrapper:
msg _withSeqNo_ : MsgContent Nat -> Msg .
--- the final envelope: sender and receiver
msg msg_from_to_ : Msg Oid Oid -> Msg .
endom)
--- Module for LISTS of messages:
(omod MSG-LIST is protecting MESSAGES .
sort MsgList .
subsort Msg < MsgList .
op empty : -> MsgList [ctor] .
op _::_ : MsgList MsgList -> MsgList [ctor assoc id: empty] .
op _existsIn_ : Nat MsgList -> Bool .
vars N N' : Nat .
var ML : MsgList .
var M : Msg .
var S : String .
eq N existsIn empty = false .
eq N existsIn (S withSeqNo N') :: ML = if (N == N') or (N existsIn ML)
then true else false fi .
endom)
--- A module for LISTS of Strings: (lecture notes)
(fmod STRING-LIST is protecting STRING .
sort StringList .
subsort String < StringList .
op nil : -> StringList [ctor] .
op _++_ : StringList StringList -> StringList [ctor assoc id: nil] .
endfm)
--- Model the possibilities for loss and duplication of messages:
--- (lecture notes)
(omod UNRELIABILITY is protecting MESSAGES .
var M : Msg .
vars O O' : Oid .
--- Loss of a message of the given kind:
rl [messageLoss] :
msg M from O to O' => none .
--- Duplication of swimming messages:
--- rl [duplicateMsg] :
--- msg M from O to O' => (msg M from O to O') (msg M from O to O') .
endom)
--- Sliding window protocol.
(omod SLIDING-WINDOW is
including STRING-LIST .
including MESSAGES .
including UNRELIABILITY .
including MSG-LIST .
--- ***** Sender protocol ***** ---
class Sender | msgsToSend : StringList, --- messages not sent yet
currentSeqNo : Nat, --- seq no to current msg
receiver : Oid , --- receiver address
szOfWindow : Nat , --- size of the window
msgsInWindow : Nat , --- number of messages in the window
window : MsgList , --- window is a list of messages
lowSeqWin : Nat , --- lowest seq in window
currentSeqWin : Nat . --- counter used for the window
vars N N' N2 N3 N4 N5 N6 : Nat .
var NZ : NzNat .
vars O O' : Oid .
var S S' S'' : String .
var SL : StringList .
var M M' : Msg .
var ML ML' : MsgList .
var B : Bool .
--- Take a msg from the messages not yet sent, wrap them up and add to window.
crl [addMsgToWindow] :
< O : Sender | msgsToSend : S ++ SL, msgsInWindow : N, currentSeqNo : N',
szOfWindow : N2, window : ML >
=>
< O : Sender | msgsToSend : SL, msgsInWindow : N + 1,
window : ML :: (S withSeqNo N'), currentSeqNo : N' + 1 >
if N <= N2 .
--- Take a message from the window, wrap it up, and send it into the eternity.
--- Hopefully someone will eventually find it.
crl [sendMsg] :
< O : Sender | currentSeqWin : N, lowSeqWin : N', msgsInWindow : N2,
window : ML :: (S withSeqNo (N3)) :: ML', receiver : O' >
=>
< O : Sender | currentSeqWin : (N + 1) rem N2 >
msg (S withSeqNo (N3)) from O to O'
if (N + N') = N3 .
--- Receive an acknowledgement from the receiver.
crl [receiveAck] :
(msg (ack withSeqNo N) from O' to O)
< O : Sender | lowSeqWin : N' >
=>
< O : Sender | lowSeqWin : N + 1, currentSeqWin : 0 >
if (N >= N') .
--- Ignore the acknowledgement if it's too old.
crl [receiveOldAck] :
(msg (ack withSeqNo N) from O' to O)
< O : Sender | lowSeqWin : N' >
=>
< O : Sender | >
if (N < N') .
--- Clean the window. A dirty window means there are packages in it which the
--- receiver has already acknowledged.
crl [cleanWindow] :
< O : Sender | lowSeqWin : N, window : (S withSeqNo N') :: ML,
msgsInWindow : s N2 >
=>
< O : Sender | window : ML, msgsInWindow : N2 >
if N > N' .
--- ***** Receiver protocol ***** ---
class Receiver | greatestSeqNoRcvd : Nat, --- Greatest seq received
sender : Oid, --- Sender
szOfWindow : Nat, --- Size of the window
msgsInWindow : Nat, --- Number of messages in the window
window : MsgList, --- Window is a list of messages
msgsRcvd : StringList, --- Messages that has been received
nextSeq : Nat,
active : Bool .
--- Receive the first packet. When we've received the first packet we can start
--- sending acknowledgements.
rl [rcvFirstPacket] :
(msg (S withSeqNo 0) from O' to O)
< O : Receiver | msgsRcvd : SL, active : false, window : ML >
=>
< O : Receiver | active : true, window : (S withSeqNo 0) :: ML > .
--- Receive a packet.
crl [rcvNewPacket] :
(msg (S withSeqNo NZ) from O' to O)
< O : Receiver | msgsInWindow : N3, szOfWindow : N4, window : ML,
nextSeq : N' >
=>
< O : Receiver | window : ML :: (S withSeqNo NZ), msgsInWindow : s N3 >
if NZ >= N' and NZ < (N' + N4) and N3 < N4 and not(NZ existsIn ML) .
--- Throw away duplicate packet.
crl [rcvDupPacket] :
(msg (S withSeqNo N) from O' to O)
< O : Receiver | window : ML :: (S' withSeqNo N') :: ML' >
=>
< O : Receiver | >
if N == N' .
--- Update window .
rl [rcvUpdateWindow] :
< O : Receiver | window : ML :: (S withSeqNo N) :: ML', nextSeq : N,
msgsRcvd : SL, msgsInWindow : s N3 >
=>
< O : Receiver | window : ML :: ML', msgsRcvd : SL ++ S,
msgsInWindow : N3, nextSeq : s N > .
--- Send acknowledgement.
rl [sendAck] :
< O : Receiver | nextSeq : N, sender : O', active : true >
=>
< O : Receiver | >
msg (ack withSeqNo N) from O to O' .
--- receive/ignore a packet with an *old* sequence number:
crl [rcvOldPacket] :
(msg (S withSeqNo N) from O' to O)
< O : Receiver | nextSeq : N' >
=>
< O : Receiver | >
if N < N' .
endom)
--- Initial states
(omod TEST is including SLIDING-WINDOW .
subsort String < Oid .
var N : Nat .
op lol : -> Configuration . --- a suitable initial state
eq lol =
< "Sender" : Sender | msgsToSend : "Obligen" ++ "er" ++ "utrolig" ++
"spennende" ++ "og" ++ "inspirerende",
currentSeqNo : 0,
receiver : "Receiver",
szOfWindow : 4,
msgsInWindow : 0,
window : empty,
lowSeqWin : 0,
currentSeqWin : 0 >
< "Receiver" : Receiver | msgsRcvd : nil,
sender : "Sender",
msgsInWindow : 0,
szOfWindow : 4,
window : empty,
nextSeq : 0,
active : false > .
endom)
Comments