% simplified swp model; does not model timeout resends or recycling of seqNums
% Joel Kammet 2/24/07

% Msg is a tuple rather than an int just for illustrative purposes; its header is not used in this algorithm
% if a Frame f is ONLY an ack, f.data.data = -1
vocabulary Message
  types
    Msg tuple [header: Int, data: Int],
    Frame tuple [seqNum: Int, ackNum: Int, data: Msg]
end

automaton SWP
  imports Message

  signature
    input    receive(m: Frame)
    output   send(m: Frame)

  states
 % sender states:
	% messages from higher layer waiting to be sent (I'm not modeling the transactions with the
    % 	client protocol -- just assuming the messages to be sent are already here); using these
    %  	Msg tuples just to try out something a little more interesting than simple Int
    fromHL: Seq[Msg] := {}|- [1, 100001] |- [2, 100002] |- [3, 100003] |- [4, 100004] |- [5, 100005] |- [6, 100006]
                          |- [7, 100007] |- [8, 100008] |- [9, 100009] |- [10, 100010] |- [11, 100011] |- [12, 100012],
    % send window size
    SWS: Nat := 4,
    % last ack received
    LAR:  Int := -1,
    % last frame sent
    LFS: Int := -1,
    % buffer of Frames sent, whose acks have not been received
    sentBuffer: Seq[Frame] := {},
     

% receiver states:
    readyToAck: Bool := false,
    % sequence number of next act to be sent
    nextToAck: Int := 0,
    % receive window size
    RWS: Nat := 4,
    % last (contiguous) frame received
    LFR: Int := -1,
    % buffer of msgs received; msgs immediately saved here if they are within the window
	  %  (the Map is seqNum -> data)
    recvBuffer: Map[Int, Msg] := empty,
    % buffer of message contents ready for higher level protocol; msgs are
    %   moved here from recvBuffer only if all lower-seq-num msgs have been received
    %   I'm not modeling the transaction with the higher layer, so msgs just accumulate here
    %   (could have simply thrown them away rather than saving them here)
    toHL: Seq[Msg] := {}
    
	
transitions
  input  receive(m)
    eff
      % if m fits in the window ...
      if m.seqNum > LFR /\ m.seqNum <= (LFR + RWS) 
        then
          if m.data.data ~= -1
            then
              recvBuffer := update(recvBuffer, m.seqNum, m.data)
          fi;
          if m.ackNum > LAR
            then
              LAR := m.ackNum - 1
          fi
      fi;
      %see if ready to ack & move message data from recvBuffer to toHL
      if defined(recvBuffer,(LFR + 1))
        then
          toHL := toHL |- recvBuffer[LFR + 1];
          recvBuffer := remove(recvBuffer, (LFR + 1));
          LFR := LFR + 1;
          % note that the seqNum in the ack is the next frame EXPECTED
          nextToAck := LFR + 1;
          if defined(recvBuffer,(LFR + 1))
            then
              toHL := toHL |- recvBuffer[LFR + 1];
              recvBuffer := remove(recvBuffer, (LFR + 1));
              LFR := LFR + 1;
              readyToAck := true;
              nextToAck := LFR + 1;
              if defined(recvBuffer,(LFR + 1))
                then
                  toHL := toHL |- recvBuffer[LFR + 1];
                  recvBuffer := remove(recvBuffer, (LFR + 1));
                  LFR := LFR + 1;
                  nextToAck := LFR + 1;
                  if defined(recvBuffer,(LFR + 1))
                    then
                      toHL := toHL |- recvBuffer[LFR + 1];
                      recvBuffer := remove(recvBuffer, (LFR + 1));
                      LFR := LFR + 1;
                      nextToAck := LFR + 1;
                  fi
              fi
          fi
      fi
      % if m is outside the receive window we ignore it


  output send(m)
    % first disjunct is a new outgoing message -- still within the send window
    pre ((fromHL ~= {} /\ LFS <= LAR + SWS) /\ m = [LFS + 1, nextToAck, head(fromHL)])
    % next is a re-send - either nothing new to send or outside the send window AND there
    %   are messages that have been sent but not yet acked
        \/ ((fromHL = {} \/ LFS > LAR + SWS) /\ sentBuffer ~= {} /\ m = [head(sentBuffer).seqNum,
                                                            nextToAck, head(sentBuffer).data])
    % finally, nothing new to be sent, all sent msgs have been acked & we have an ack to send
        \/ (fromHL = {} /\ sentBuffer = {} /\ readyToAck = true /\ m = [LFS + 1, nextToAck, [-1, -1]])
    eff 
      if (fromHL ~= {} /\ LFS <= LAR + SWS)
        then
% send a new message
          sentBuffer := sentBuffer |- m;
          LFS := LFS + 1;
          readyToAck := false
      elseif ((fromHL = {} \/ LFS > LAR + SWS) /\ sentBuffer ~= {})
        then
% this is a resend; if expiration times were included in this model, we would also reset the expTime
%   of the re-sent frame here
          readyToAck := false
      else
% just sending an ack
        readyToAck := false
      fi