--- 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)