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

imports Messages
automaton SlidingWindowReceiver(window:Nat)

signature
	input receive(m: Message, const A:Role, B:Role)
	       
	output  send(m: Message, const B:Role, A:Role),
		read(data:Data)
	
states
	receiveBuf:Array[Int, Message] := constant([0,0,0]),
	lastFrameReceived:Int := 0,
	lastAcceptableFrame:Int := window,
	lastFrameRead:Int := 0
	
transitions
	% compute the cumulative ack, ie, the largest sequence number such that 
	% every smaller sequence number has appeared in a received message
	input receive(m, s, t; local consecutive:Bool, hack:Set[Nat])
	eff 
		if m.seq > lastFrameReceived /\ m.seq <= lastAcceptableFrame then
			receiveBuf[m.seq] := m
		fi;
		consecutive := true;
		for i:Nat in hack do %(lastFrameRead+1)..lastAcceptableFrame do 
			if consecutive /\ receiveBuf[lastFrameReceived].seq > 0 then 
		   		lastFrameReceived := lastFrameReceived+1
		   	else
		   		consecutive := false
			fi;
		od
			
	output read(x; local msg:Message)
	pre
	  receiveBuf[lastFrameRead+1].seq > 0 
	  /\ x = receiveBuf[lastFrameRead+1].data  
	eff
		lastFrameRead := lastFrameRead+1;
		lastAcceptableFrame := lastAcceptable+1
	
	output send(m, s, t)
	pre
		m.ack <= lastFrameReceived