% Sender Sliding Window

vocabulary Messages
	types 	Message tuple [data: Int, index: Int], % data contains the frame and seq holds the index value
			Ack:Int % Cummulative acknowledgement. If it receives frame 15 it sends Ack till 15.
end

imports Messages

automaton slidingsender(ws: Int)

	signature 
		input write(m: Message)
		
		input receive(a: Int)

		output  send(m: Message)
		
		internal remove
  				
	states
		sendQueue: Seq[Message],	% Buffer for receiving the messages
		tempQueue: Seq[Message],	% Temporary Sequence for transfering frames of Window Size buffer
		nextSeq: Int := 1,			% This variable is maintained to append the index of the message to the Sequence of Messages
		lar: Int := 0, 				% Last frame acknowledged by receiver, intialized to 0
		lfs: Int := 0				% Last frame sent
		
	transitions
		input write(m)
		eff
			sendQueue := sendQueue |- [m.data, nextSeq];
			tempQueue := tempQueue |- [m.data, nextSeq];
			nextSeq := nextSeq + 1
			
			
		input receive(a)
			eff 
				lar := a + 1

		internal remove
		pre
			head(sendQueue).index < lar
		eff
			sendQueue := tail(sendQueue)
			
		output send(m)
			pre m=head(tempQueue)
			eff
				if (head(tempQueue).index >= lar+ws) then
					tempQueue := sendQueue
				fi;
				tempQueue:= tail(tempQueue);
				if (tempQueue = {}) then
					tempQueue := sendQueue
				fi
				
% random scheduler
% action 1 = write, action 2 = send, action 3 = receive ack
schedule
 states
    data:Int := 1,
    action:Nat := 1,
    ack:Nat := 1,
    work:Int := 0,
    seq:Int := 1,
    msg:Message := [1,1]
 do

  while true do
    action := choose i:Nat where i>=1 /\ i<=3;
    
    if action = 1 then 
      msg := [data, nextSeq];
     fire input write(msg); 
      data := data+1
    else
      if action = 2 then
        if tempQueue ~= {} then
        	msg := head(tempQueue);
           fire output send(msg) 
        fi
      else
        if action = 3 then
          ack := choose i:Nat where i>=1 /\ i<=2;
          work := lar+ack-1;
          fire input receive(work);
          while head(sendQueue).index <=lar do
          	fire internal remove
          od
        fi
      fi
    fi
  od
od