/* Version: Window size 1, full version (i.e. corruption allowed), bug fixed.*/

{ VPL Code for the I-Protocol : Revision History:
{    Written by Oleg Sokolsky, October '94;
{    Revised by Y.S. Ramakrishna. }
{    Revised by Xiaoqun Du. }
                         
                 

value WIN_SIZE	:2  
{ this is really the range of sequence number. Window size is 1 -- Vic }
value fixed :1 { 0 = not fixed; 1 = fixed }

type sequence_number	:WIN_SIZE
type channel_number	:2
type packet_type	:3
type checksum		:2

{ types of packets }

value ACK   :0
value DATA  :1
value NAK   :2

{ To save space, we do not send checksums, but let the medium }
{ assign them arbitrarily. Thus incoming and outgoing packets }
{ will have different types as follows:                       }

{ this is a reduced version of packet, as sent to the medium }

type pak_send: record
  pty: packet_type;	      { type of the packet : ACK, DATA or NACK }
  pno: sequence_number;	      { sequence number of the packet (DATA or NACK) }
  ack: sequence_number;	      { piggyback ack (ACK) }
end

{ this is a full packet, as received from the meduim }

type pak_recv: record
  hck: checksum;	
  dck: checksum;	
  bod: pak_send;
end

network protocol
   (Lsend: synch, Rrecv: synch,
    LdropR: synch, RdropL: synch, LcorruptR: synch, RcorruptL: synch,
    Ltimeout: synch, Rtimeout: synch )
begin

{---------------------------------------------------------------------------------}
process chan
    (in: pak_send,
     out: pak_recv,
     drop: synch, corrupt: synch, full:synch, empty: synch)
begin
    var buf: pak_recv
    var isfull: boolean

procedure initialize
   begin
     isfull := false;
     select
       begin buf.hck := true; buf.dck := true end
     %
       begin buf.hck := true; buf.dck := false; corrupt!* end
     %
       begin buf.hck := false; buf.dck := true; corrupt!* end
     %
       begin buf.hck := false; buf.dck := false; corrupt!* end
     end; {select}
     buf.bod.pty := NAK;
     buf.bod.pno := 0;
     buf.bod.ack := 0
   end; { procedure initialize }


   { body of chan }
    call initialize;
    while (true=true) do
      select
        empty!*
      %
        begin
          in?buf.bod;
          select
             begin
               isfull := true;
               while ( isfull = true ) do
                 select
                   full! *
                 %
                   begin
	             out!buf ;
                     call initialize
                   end
                 end {select }
               end {while }
             end  { begin }
          %
             begin
               drop!* ;
               call initialize
             end
          end  { select }
        end { begin }
      end { select }
    end { while }
end; { process LchanR }

{---------------------------------------------------------------------------------}

{ 
  As it can be expected, send and receive are the actions to communicate with
  the user. Receive corresponds to fgot_data function call (made by the orig.
  code only once, in fiprocess_packet()), send corresponds to fisenddata, 
  which is called either by the user or by fisendcmd -- we do not distinguish
  between these two here.

  give and get are counterparts for send and receive for communication with
  the medium
}

{---------------------------------------------------------------------------------}
{ The Sender -- we now don't keep any superfluous variables associated with
{ receiving DATA packets from remote  -- note also, therefore, the change in
{ the interface }
{---------------------------------------------------------------------------------}
  process protisend
    (send: synch,
     give: pak_send, 
     get: pak_recv, timeout: synch,
     infull: synch, inempty: synch, outfull: synch, outempty: synch )
  begin
    var sendseq: sequence_number
        { next sequence number to use for a pkt to be sent }
    { recseq is not needed for sender -- it always stays at 0.}
    { lack is not needed for sender -- it always stays at 0. }
    var rack:    sequence_number
        { last sequence number acknowledged by remote
          I know remote has received all sequence numbers below this;
          Thus, rack decides current send window. }
    { recbuf is not required in the sender, for obvious reasons }
    { don't need naked }
    var pak:     pak_recv
	{ variable where newly arrived packets are stored -- interface to physical level }
    var seq: sequence_number
	{ temporary variable }
    var tmp: sequence_number
	{ temporary variable }

{---------------------------------------------------------------------------------}
    procedure initialize
      begin
        sendseq := 1;
        rack    := 0
     end;  { initialize }
{---------------------------------------------------------------------------------}
    procedure sendthenak
{ send the nak (with sequence number 1). This contains a piggyback ack
  for sequence number 0, informing remote that I am NAKing 1, but have rcvd all
  upto 0.
}
      begin
        pak.bod.pty := NAK;
	pak.bod.pno := 1;
	pak.bod.ack := 0;  { recseq is always 0 for sender }
	give! pak.bod
      end;


{---------------------------------------------------------------------------------}
   procedure updaterack
{ use piggybacked ACK info in the current packet to update my knowledge of what remote has
  received (rack) }
     begin
       tmp:= pak.bod.ack;
       if ( ~ ((tmp = sendseq) | (sendseq-tmp > WIN_SIZE/2) | (tmp-rack > WIN_SIZE/2)) ) then
       { piggybacked ACK is interesting if it's in my send window,
              and is not "obsolete" }
         rack := tmp   { update my knowledge of what remote has received }
     end;

{---------------------------------------------------------------------------------}
  { 
    getdata is called either when we just want to receive something, 
    or when we want to send, but the remote window is full. Roughly 
    corresponds to fiprocess_data() and fiprocess_packet()
  }

{---------------------------------------------------------------------------------}
    procedure getdata
      begin 
	    if (pak.hck = true) { header check OK } then begin {1}
	      { extract sequence number of the packet NACK  --
                since remote doesn't send DATA packets }
              seq := pak.bod.pno;
                
                if ( pak.bod.pty = ACK ) then
                  call updaterack   { extract ACK info & update rack }
		else if ( pak.bod.pty = NAK ) then begin {1.1}
                  call updaterack;  { extract piggybacked ack info if any }
		  if ( ~ ( (seq = sendseq) | (seq-rack > WIN_SIZE/2)
			| (sendseq-seq > WIN_SIZE/2)) ) then
		  begin { resend requested DATA packet } {1.1.1}
		    pak.bod.pty := DATA;
		    pak.bod.ack := 0;    { recseq is always 0 for sender }
                    give! pak.bod
		  end {1.1.1}
                end {1.1}
	    end {1}
  end;  { procedure getdata }


{---------------------------------------------------------------------------------}
 procedure timedout
    begin

       { send NAK for the packet we expect --- Taylor does this only if there
         is no packet from remote waiting to be received -- we are not faithful
         to that here because we can't check channels for emptiness... }
       select
          begin
             infull ? *; { receive channel full }
	     get ? pak; { a packet is received }
             call getdata
          end
       %
          {send _the_ NAK for oldest packet we are missing or expect to receive }
          begin
            inempty ? *; { receive channel is empty }
               outempty ? *; { send channel is empty }
               timeout ! *;  { i managed to timeout }
               call sendthenak;
               { resend the oldest unacknowledged packet, if such exists }
               if ( ~(sendseq = rack + 1) ) then begin
	           pak.bod.pty := DATA;
	           pak.bod.pno := rack + 1;
	           pak.bod.ack := 0;
	           give! pak.bod
               end { if }
          end { begin }
      end { select }
  end;  { procedure timedout }

{---------------------------------------------------------------------------------}
    procedure senddata
      begin 
	{ wait for an opening in remote window -- call to fiwindow_wait }
	while ( (sendseq-rack > WIN_SIZE/2) | (sendseq = rack) ) do
            { check of sendseq = rack needed at least for the case of WIN = 2 }
          select
            begin
              get?pak;
	      call getdata   { wait for message to arrive from remote }
            end
          %
              call timedout  { try to do the timeout tasks, such as retransmission }
          end { select }
	end; { while }
        tmp := 0;   { tmp = 0 indicates haven't yet sent the message }
        while ( tmp = 0 ) do
          select
            begin
              outempty ? *; { send channel empty }
	      pak.bod.pty := DATA;
	      pak.bod.pno := sendseq;
	      pak.bod.ack := 0;
	      sendseq := sendseq + 1;
	      give! pak.bod;
              tmp := 1   { to break out of while loop }
            end
          %
            begin
              get ? pak;
              call getdata;
              tmp := 0 { stay in loop }
            end { begin }
          end {select }
        end { while }
      end; { procedure senddata }

{---------------------------------------------------------------------------------}
  { body of protisend }

    call initialize;         { initialize the protocol data structures }
    while (true=true) do
      select
        begin
          send?*;
          call senddata
        end
        %
        begin
           get?pak;
           call getdata
        end
        %
          call timedout   { try to timeout }
      end { select }
    end { while }
  end; { process protisend }
{---------------------------------------------------------------------------------}



{---------------------------------------------------------------------------------}
{ The Receiver -- the receiver doesn't "senddata" }
{---------------------------------------------------------------------------------}
  process protirecv
    (give: pak_send, 
     get: pak_recv,
     receive: synch, timeout: synch,
     infull: synch, inempty: synch, outfull: synch, outempty: synch )
  begin
    { recver doesn't need sendseq, since doesn't send DATA packets }
    var recseq:  sequence_number
        { last sequence number up to which we have successfully received
          without gaps -- I know that I have all sequence numbers below this }
    var lack:    sequence_number
        { last sequence number from remote that we acknowledged
          Since acking is at 1/2 window boundaries, recseq usually leads lack;
          however, lack decides the current receive window. }
    { recver doesn't need rack -- no sending by us }
    var recbuf:  array[WIN_SIZE] of boolean
        { array of data packets received from remote -- and buffered for
          delivery to user at a later time }
    var naked:   array[WIN_SIZE] of boolean
        { array of sequence numbers for which a NAK has recently been sent
          I periodically clear these out and resend fresh NAKs if needed }
    var pak:     pak_recv
	{ variable where newly arrived packets are stored -- interface to physical level }
    var seq: sequence_number
	{ temporary variable }
    var tmp: sequence_number
	{ temporary variable }

{---------------------------------------------------------------------------------}
    procedure initialize
      begin
        recseq  := 0;
        lack    := 0;
        tmp := 0;
        recbuf[tmp]  := false;
        naked[tmp]   := false;
        tmp := 1;
        while (~( tmp=0 )) do
          recbuf[tmp]  := false;
          naked[tmp]   := false;
          tmp := tmp + 1
        end { while }
     end;  { initialize }
{---------------------------------------------------------------------------------}
    procedure sendnak
{ send a nak for the sequence number "tmp". This contains a piggyback ack
  for lack, informing remote that I am NAKing tmp, but have rcvd all upto
  lack.
}
      begin
        pak.bod.pty := NAK;
	pak.bod.pno := tmp;
	pak.bod.ack := recseq;
	naked[tmp] := true;
	give! pak.bod;
        lack := recseq
      end;


{---------------------------------------------------------------------------------}
{ no updates of rack needed since I am not sneding DATA packets  -- so no
{  procedure updaterack                                    
}
{---------------------------------------------------------------------------------}
  { 
    getdata is called either when we just want to receive something, 
    or when we want to send, but the remote window is full. Roughly 
    corresponds to fiprocess_data() and fiprocess_packet()
  }

{---------------------------------------------------------------------------------}
    procedure getdata
      begin 
	    if (pak.hck = true) { header check OK } then begin {1}
	      { extract sequence number of the packet DATA or NACK }
              seq := pak.bod.pno;
                
	      if (pak.bod.pty = DATA)  then begin {1.1}
		if ~( ( seq - lack > WIN_SIZE/2 ) | ( seq = lack ) ) then begin { seq_no within window } {1.1.1}
                     { case of seq = lack important at least for the case WIN = 2 }
                  { no piggyback ACK info, since am not sending }
                  { call updaterack; { use piggybacked ack info to update rack }
		  if (pak.dck = true) { data check OK } then begin {1.1.1.1}
		    naked[seq] := false;  { don't need to nack in future }
		    if ~(seq = recseq+1) then begin {1.1.1.1.1}
			{ the packet has unexpected seq_no }
		      if (~(seq = recseq) & (recbuf[seq] = false)) then begin {1.1.1.1.1.1}
			  { not an old packet already received }
			  { save the packet for later use, if not already received }
			 recbuf[seq] := true;
			 tmp := recseq + 1;
			 { send NAKs for all missing packets in between, if NAK not
                           recently sent }
			 while ( ~( tmp = seq ) ) do
                           if (~(naked[tmp] = true) | (recbuf[tmp] = true)) then
			     call sendnak;
			   tmp := tmp + 1
			 end {while}
                        { Oleg does recseq := seq here, which is clearly wrong }
		      end {1.1.1.1.1.1}
                    end {1.1.1.1.1}
		    else { DATA packet with expected sequence number }
			 { fiprocess_packet is called at this point }
			 { this is only the DATA part of it         }
		      begin {1.1.1.1.1}
                        recseq := seq; { DATA packet received in sequence }
			receive?*;    {a new DATA packet is returned to user}
			{ if any subsequent packets are here, buffered, return them too }
			tmp := seq + 1;
			while (recbuf[tmp] = true) do
                          recseq := tmp; { update recseq }
			  receive?*;
			  recbuf[tmp] := false;
			  tmp := tmp + 1
			end;  { while }
			{ if a half-window line is crossed, send an ACK }
			if ~(recseq-lack < WIN_SIZE/4) then begin {1.1.1.1.1.1}
			  pak.bod.pty := ACK;
			  pak.bod.ack := recseq;
			  give! pak.bod;
			  lack := recseq   { lack catches up here }
			end {1.1.1.1.1.1}
		      end {1.1.1.1.1}
		  end {1.1.1.1}
		  else { data is corrupted, send NAK if it was in our rcv-window,
                         it hasn't been received so far, and it hasn't been NAKed recently }
		    if (~(seq = recseq) & (recbuf[seq] = false) &
                         (naked[seq]=false)) then begin {1.1.1.1}
		      tmp := seq;
		      call sendnak
		    end {1.1.1.1}
		end {1.1.1}
	      end {1.1}
	      else { this is not a DATA packet: ACK or NAK }
		   { this is a part of fiprocess_packet code }
{                if pak.bod.pty = ACK then
{                  skip { no question of ACKs since I am not sending }
{                  { call updaterack   { extract ACK info & update rack }
	 	if ((fixed = 1) & (pak.bod.pty = NAK) & (seq = 1)) then begin {1.1}
                  { as in June 95 version of protocol, which, alas fixes our favourite bug :-( }
                  pak.bod.pty := ACK;
                  pak.bod.ack := recseq;
                  pak.bod.pno := recseq;
                  give! pak.bod   { send an uptodate ACK, since this NAK might mean that the sender's send window is full }
                end {1.1}
	    end {1}
  end;  { procedure getdata }


{---------------------------------------------------------------------------------}
  procedure timedout
     begin
 
        { clear the list of nak'd packets -- hope to get them is lost }
        naked[0] := false;
        tmp := 1;
        while ( ~(tmp = 0) ) do
           naked[tmp] := false;
 	  tmp := tmp + 1
        end;  { while }
        { send NAK for the packet we expect }
        select
           begin
              infull ? *;  { recv channel full }
              { receive a packet if it's waiting to be received }
              get?pak;
              call getdata
           end
        %
           begin {send NAK for oldest packet we are missing or expect to receive }
              inempty? *;
                  outempty? *; { send channel empty }
                  timeout! *;
                  tmp := recseq + 1;
                  call sendnak
           end { begin }
        end {select }
   end;  { procedure timedout }

{---------------------------------------------------------------------------------}
  { body of protirecv }

    call initialize;         { initialize the protocol data structures }
    while ( true=true ) do
       select  
         begin
           get?pak;
           call getdata         { no sending of data }
         end
         %
           call timedout  { temporarily disable this feature ? }
       end { select }
    end { while }
  end; { process protirecv }

{---------------------------------------------------------------------------------}
{ CHANNEL Declarations }
{---------------------------------------------------------------------------------}

  channel Lout: pak_send
  channel Lin: pak_recv
  channel Rout: pak_send
  channel Rin: pak_recv
  channel LfullR: synch
  channel LemptyR: synch
  channel RfullL: synch
  channel RemptyL: synch

{---------------------------------------------------------------------------------}

  protisend( Lsend, Lout, Lin, Ltimeout, RfullL, RemptyL, LfullR, LemptyR ) |
  chan( Lout, Rin, LdropR, LcorruptR, LfullR, LemptyR ) |
  protirecv( Rout, Rin, Rrecv, Rtimeout, LfullR, LemptyR, RfullL, RemptyL ) |
  chan( Rout, Lin, RdropL, RcorruptL, RfullL, RemptyL )
 
end;



{---------------------------------------------------------------------------------}