% Sliding Window: A reliable sender.

% For use with an unreliable channel

% no timeouts

vocabulary Messages
	types Data:Int,
		Message tuple [data:Int, seq:Int, ack:Int],
		Role enumeration  [A, B]
end

imports Messages
automaton SlidingWindowSender(window:Nat, timeout:Real)

signature
	output send(m: Message, const B:Role, A:Role)
	       
	input  receive(m: Message, const A:Role, B:Role),
	       write(x: Int)
	
states
	sendBuf:Array[Int, Message] := constant([0,0,0]) ,
	lastFrameWritten:Int := 0,							% highest sequence number of a buffered frame
	lastFrameSent:Int := 0,								% highest sequence number of a sent frame
	lastAckReceived:Int := 0,							% highest consecutive ack
	index:Int := 1,
	now:Real := 0
	
transitions
	input write(x)
	eff 
		lastFrameWritten := lastFrameWritten + 1;
		sendBuf[lastFrameWritten] := [x, lastFrameWritten, 1]
	
	% cumulative acknowledgment assumed, as described in lecture notes
	% for non-cumulative acks, the condition is "m.ack = lastAckReceived+1"	
	input receive(m, A, B) 
	eff
		if m.ack > lastAckReceived then
		  if m.ack <= lastFrameSent then
			lastAckReceived := m.ack
		  fi
		fi

	% Sends the frame in sendBuf[index]
	% index starts at first unacked frame and counts up to end of window 
	% or last available frame, then starts over.
	output send(m, B, A)
	pre
		m = sendBuf[index] /\ index <= lastFrameWritten /\ index <= lastAckReceived+window
	eff
		if m.seq > lastFrameSent then 
			lastFrameSent := m.seq
		fi;
		if index < lastAckReceived+window /\ index < lastFrameWritten then 
		  index := index+1 
		else 
		  index := lastAckReceived+1
		fi

% random scheduler
% action 1 = write, action 2 = send, action 3 = receive ack
schedule
 states
    data:Int := 1,
    action:Nat := 1,
    ack:Nat := 1,
    seq:Nat := 1
 do

  while true do
    if lastFrameSent > lastAckReceived then
       action := choose i:Nat where i>=1 /\ i<=3
    else  
       action := choose i:Nat where i>=1 /\ i<=2
    fi;
    
    if action = 1 then 
      fire input write(data); 
      data := data+1
    else
      if action = 2 then
        if lastFrameWritten>=index then
            fire output send(sendBuf[index], B, A) 
        fi
      else
        if action = 3 then
          ack := choose i:Nat where i>=1 /\ i<=2;
          fire input receive([0,0,lastAckReceived+ack-1], A, B)
        fi
      fi
    fi
  od
od