axioms NonDet

type Message = tuple of seq:Int, ack:Int, adv:Int, msg:Seq[Int], syn:Bool

% The buffer size for received messages is given by bufsize
% The maximum segment size is given by MSS
% The round trip time is RTT (treated as fixed here - no estimations)
automaton tcp(process:Int, bufsize:Int, MSS:Int, RTT:Int)

signature
	output send(m:Message, const process, receiver:Int)

        internal tick, 	                  % simulates clock
                 application(n:Int),      % application reading data

                 % the following internal actions implement loops
                 fill,             % put bytes in segment to be sent
                 markBytes,               % mark bytes received
                 findNBE                  % find next byte expected

	input receive(m:Message, sender:Int, const process)

states
	buffer:Array[Int,Bool] := constant(false),
        now:Int := 0,           % current time
        synsent:Bool := false,
        synrcvd:Bool := false,

        % for retransmission
        segments:Map[Int, Seq[Int]]:=empty,
        timeouts:Map[Int, Int]:=empty,

        % sender variables
	nextSeq:Int := 0,       % sender's next byte to send
        lar:Int := -1,          % left side of window
        stop:Int := -1,         % right side of window

        % receiver variables
        rcvLeft:Int := 0,       % left side of window
	nbe:Int := 0,           % next byte expected
	lab:Int := bufsize-1,   % last acceptable byte
 
        % auxiliary variables used in internal transitions for implementing
        % loops       
        nextSegment:Seq[Int] := {},
        sIndex:Int := 0,
        sBegin:Int:=0,
        sEnd:Int:=0,
        rIndex:Int := 0,
        rBegin:Int:=0,
        rEnd:Int:=0,
        mark:Bool:=false,
        find:Bool:=false,           % true if receiver needs to update nbe

        % for debugging
        timedout:Bool:=false

transitions

        % Send the segment once it has been filled
        % Updating variables:
        %     seq (next byte to send) to byte beyond end of this segment
        %     sBegin (next byte to fill in next segment) to byte beyond end 
        %             of this segment
        %     sEnd (last byte to fill in next segment) to min(stop, seq+MSS)
        % Note that if the sender is allowed to send more bytes (ie, the
        % sender hasn't sent all bytes allowed by the receiver window) then
        % the sender can start filling a new segment as soon as this segment
        % has been sent.
        output send(m, process, j)
        pre  
           % initial send
           (m.syn /\ m.seq=0 /\ m.ack=0 /\ m.adv=bufsize /\ m.msg={})
           \/
           %retransmit segment on timeout
           (defined(timeouts,lar) /\ timeouts[lar] <= now /\ ~find /\ ~mark /\
            m.msg = segments[lar] /\ m.seq=lar /\ 
            m.ack=nbe /\ m.adv=(lab+1)-nbe)
           \/
           %normal send
           (sIndex=sEnd /\ len(nextSegment)>0 /\ ~find /\ ~mark /\
            m.msg=nextSegment /\ m.seq=nextSeq /\             
            m.ack=nbe /\ m.adv=(lab+1)-nbe)
        eff
           if m.syn then 
              synsent := true 

           elseif m.seq=nextSeq then
              % remember segment sent and set timeout
              timedout := false;
              segments := update(segments, nextSeq, nextSegment);
              timeouts := update(timeouts, nextSeq, now+(2*RTT));

              % update variables for sender side of process
              nextSegment := {};
              nextSeq := sEnd;
              sBegin := sEnd;
              if synsent /\ synrcvd then
                 % set sEnd to smaller of stop+1 or seq+MSS
                 if (nextSeq+MSS) < (stop+1) then 
                    sEnd := nextSeq+MSS 
                 else 
                    sEnd := stop+1
                 fi
              fi

           else              % this must be a re-send on a timeout
              timedout := true;
              timeouts := update(timeouts, lar, now+(2*RTT))
           fi;

        % Fill a segment with bytes containing their position in the stream
        internal fill
        pre
           sIndex >= sBegin /\ sIndex < sEnd
        eff
           nextSegment := nextSegment |- sIndex;
           sIndex := sIndex+1

        % Receive a segment
        % Ignore the segment unless all bytes are within the current window
        % Update variables:
        %     rBegin: received segment starts here; must mark received bytes
        %     rEnd: end of received segment
        %     mark: true if there are any received bytes to mark
        %     nbe: if segment starts at current nbe, new nbe will be beyond end
        %          of segment
        %
        %     lar: remember last byte acknowledged, to set left side of send
        %          window
        %     stop: compute this from m.ack and m.adv
        %     sEnd: last byte to be sent in next segment (used by fill);
        %           should be updated here because stop may have moved right
	input receive(m, i, process)
	eff
           if m.syn then synrcvd := true fi;

           % check that message is in window and not a duplicate

           if m.seq >= rcvLeft /\ (m.seq+(len(m.msg)-1))<=lab /\
              ~buffer[m.seq] then 

              % update variables for receiver part of process
              rBegin := m.seq;
              rIndex := m.seq;
              rEnd := m.seq+len(m.msg);
              if len(m.msg)>0 then
                mark := true;
                if m.seq = nbe then
                   nbe := nbe+len(m.msg);
                fi
              fi
            fi;

            % update variables for sender part of process
            lar := m.ack;
            stop := (m.ack+m.adv)-1;  % can send up to m.adv unacked bytes
            if synsent /\ synrcvd then
               if (nextSeq+MSS) < (stop+1) then 
                  sEnd := nextSeq+MSS 
                else 
                  sEnd := stop+1
                fi
            fi
            

        % clock ticks; add 1 to time now
        internal tick
        eff
           now := now+1

        % application reads first n bytes in receiver buffer
        internal application(n)
        pre
          (rcvLeft+n) <= nbe /\           % n is valid
          ~find /\ ~mark /\ sIndex=sEnd   % loops not executing
        eff
          rcvLeft := rcvLeft+n;
          lab := lab+n

        % for each received byte, mark the corresponding position in buffer
        % as true
        internal markBytes
        pre
           mark /\ rIndex>=rBegin /\ rIndex < rEnd
        eff
           buffer[rIndex] := true;
           rIndex := rIndex+1;
           if rIndex = rEnd then 
              mark := false;
              if buffer[nbe] then find := true fi
           fi

        % find the first position of buffer containing false (no byte received)
        internal findNBE
        pre
           find /\ ~mark /\ buffer[nbe]
        eff
           nbe := nbe+1;
           if ~buffer[nbe] then find := false fi


% reliable channel from i to j
automaton ReliableChannel(i, j: Int)
  signature
    input send(m: Message, const i, const j) 
    output receive(m: Message, const i, const j) 
  states
    buffer: Seq[Message] := {}
  transitions
    input send(m, i, j)
      eff buffer := buffer |- m
    output receive(m, i, j)
      pre buffer ~= {} /\ m = head(buffer)
      eff buffer := tail(buffer)

%this is a lossy channel (see input send)
automaton LossyChannel(i, j: Int)  

signature    
   input send(m: Message, const i, const j)    
   output receive(m: Message, const i, const j)   

states           
   buffer: Seq[Message] := {},
   lost: Int:=-1 

transitions    
   input send(m, i, j)      
      eff           
         % throw a 3-sided die to decide whether to lose the message        
         if randomInt(1,3)<3 then 
            buffer := buffer |- m 
         else
            lost := m.seq
         fi 

   output receive(m, i, j)       
      pre buffer ~= {} /\ m = head(buffer)      
      eff buffer := tail(buffer)            

automaton Session
  components C[m:Int, n:Int]: LossyChannel(m, n) 
             where 1 <= n /\ n <= 2 /\ 1<= m /\ m<= 2;
             P[i:Int]:tcp(i, 10, 3, 1)  where 1 <= i /\ i <= 2


% The scheduler follows the rules:
%
% 1) If any loop is being executed, finish it 
%
% 2) Pick a process or channel
%    If a process was picked:
%    a) If there is a timeout, send the earliest unacknowledged message
%    b) Pick an action.  Then randomly decide whether to send a new message
%       or to give the application some data.
%    c) Add 1 to the clock (fire tick action).
%
%    If a channel was picked: deliver a message

schedule 
states
  rndm:Int,
  prcs:Int,     % process number
  chan:Int,     % channel number
  actn:Int,     % action number
  n:Int         % number of bytes for application to read
  
with 
     P1 = P[1], C12 = C[1,2], 
     P2 = P[2], C21 = C[2,1]
do

  % get the tcp connection started by exchanging SYN messages
  % this doesn't quite work, because of lost messages; re-run if it aborts

  % P1 sends SYN message to P2
  fire output P1.send([0, 0, P1.lab+1, {}, true], 1, 2);
  % keep trying if message was lost
  while C12.buffer={} do
     fire output P1.send([0, 0, P1.lab+1, {}, true], 1, 2)
  od;
  fire output C12.receive(head(C12.buffer), 1, 2);

  % P2 sends SYN message back to P1
  fire output P2.send([0, 0, P2.lab+1, {}, true], 2, 1);
  % keep trying if message was lost
  while C21.buffer={} do
     fire output P2.send([0, 0, P2.lab+1, {}, true], 2, 1)
  od;
  fire output C21.receive(head(C21.buffer), 2, 1);

% loop forever, sending and receiving messages
  while true do

   % if any loops need to be executed, execute them
   while P1.mark /\ P1.rIndex >= P1.rBegin /\ P1.rIndex < P1.rEnd do
      fire internal P1.markBytes
   od;
   while P1.find /\ ~P1.mark /\ P1.buffer[P1.nbe] do
      fire internal P1.findNBE
   od;
   while P1.sIndex>=P1.sBegin/\P1.sIndex<P1.sEnd do 
      fire internal P1.fill 
   od;
   while P2.mark /\ P2.rIndex >= P2.rBegin /\ P2.rIndex < P2.rEnd do
      fire internal P2.markBytes
   od;
   while P2.find /\ ~P2.mark /\ P2.buffer[P2.nbe] do
      fire internal P2.findNBE
   od;
   while P2.sIndex>=P2.sBegin/\P2.sIndex<P2.sEnd do 
      fire internal P2.fill 
   od;
           
    % pick a process
    % let 1-4 represent process 1, 5-8 represent process 2, 
    % 9 represent Channel[1,2] and 10 represent Channel[2,1]
    rndm := randomInt(1,10);    
    if rndm <= 8 then
      if rndm <= 4 then prcs:=1 else prcs:=2 fi;

      % now pick a locally controlled action:
      % 1=send, 2=application, 
      actn := randomInt(1,10);

      % if no message is enabled for sending or receiving, 
      % add 1 to the time at each process
      if C12.buffer={} /\ C21.buffer={} /\ 
         ((defined(P1.timeouts, P1.lar) /\ P1.timeouts[P1.lar] > P1.now) 
                 \/ P1.stop < P1.lar) /\ 
         ((defined(P2.timeouts, P2.lar) /\ P2.timeouts[P2.lar] > P2.now)
                 \/ P2.stop < P2.lar) /\ 
         len(P1.nextSegment)=0 /\ len(P2.nextSegment)=0
      then
         fire internal P1.tick; fire internal P2.tick
      fi;

      % process 1 takes a step
      if prcs=1 then

         % if there was a timeout, send the earliest unacked segment
         if defined(P1.timeouts, P1.lar) /\ P1.timeouts[P1.lar] <= P1.now 
            /\ ~P1.find /\ ~P1.mark /\ P1.sIndex=P1.sEnd then
            % in case of a timeout, this is a re-send
            fire internal P1.tick;
            fire output P1.send([P1.lar, P1.nbe, (P1.lab+1)-P1.nbe, 
                                 P1.segments[P1.lar], false], 1, 2)
         fi;
   
         if actn=1 then          
           % send a segment
           if (P1.sIndex=P1.sEnd /\ len(P1.nextSegment)>0 /\ 
                   ~P1.find /\ ~P1.mark) then
              % this is the original send, once a segment has been filled
              fire internal P1.tick;
              fire output P1.send([P1.nextSeq, P1.nbe, (P1.lab+1)-P1.nbe,
                                 P1.nextSegment, false],1,2)
           fi

         elseif actn=2 then      
         % application reads some data from the receive buffer
            if P1.rcvLeft < P1.nbe /\ ~P1.find /\ ~P1.mark /\ 
               P1.sIndex=P1.sEnd then
               % limit data read to at most 3 bytes at a time
               if (P1.nbe-P1.rcvLeft) < 3 then
                 n := randomInt(1, P1.nbe-P1.rcvLeft)
               else
                 n := randomInt(1,3)
               fi;
               fire internal P1.tick;
               fire internal P1.application(n)
            fi

         fi

      % process 2 takes a step
      elseif prcs=2 then

         % if there was a timeout, send earliest unacked segment
         if defined(P2.timeouts, P2.lar) /\ P2.timeouts[P2.lar] <= P2.now 
            /\ ~P2.find /\ ~P2.mark /\ P2.sIndex=P2.sEnd then
            % in case of a timeout, this is a re-send
            fire internal P2.tick;
            fire output P2.send([P2.lar, P2.nbe, (P2.lab+1)-P2.nbe, 
                                P2.segments[P2.lar], false], 2, 1)
         fi;

         if actn=1 then          

           % send a segment
           if P2.sIndex=P2.sEnd /\ len(P2.nextSegment)>0 /\ 
                  ~P2.find /\ ~P2.mark then
              % this is the original send, once a segment has been filled
              fire internal P2.tick;
              fire output P2.send([P2.nextSeq, P2.nbe, (P2.lab+1)-P2.nbe,
                                 P2.nextSegment, false], 2, 1)
           fi

         % application reads some data from the receive buffer
         elseif actn=2 then      % application
            if P2.rcvLeft < P2.nbe /\ ~P2.find /\ ~P2.mark /\ 
               P2.sIndex=P2.sEnd then
               % limit data read to at most 3 bytes at a time
               if (P2.nbe-P2.rcvLeft) < 3 then
                 n := randomInt(1, P2.nbe-P2.rcvLeft)
               else
                 n := randomInt(1,3)
               fi;
               fire internal P2.tick;
               fire internal P2.application(n)
            fi
         fi
      fi

    else
      
      % a channel takes a step
      % 9 is the channel from 1 to 2; 10 is the channel from 2 to 1
      chan := rndm;
      if chan=9 /\ C12.buffer ~= {} then
        fire internal P1.tick;
        fire output C12.receive(head(C12.buffer),1,2)
      elseif chan=10 /\ C21.buffer ~= {} then
        fire internal P2.tick;
        fire output C21.receive(head(C21.buffer),2,1)
      fi

    fi
    
  od
od