specification SlidingWindowProtocol;

{ Estelle specification of the "Sliding Window Protocol" ;
  complete P.D. version for simulation
}

default individual queue;

timescale milisecond;

{
+------------------+                            +------------------+ 
|                  |                            |                  | 
| TransmitterUser  |                            |   ReceiverUser   | 
|                  |                            |                  | 
+------ip U--------+                            +------ip-U--------+   
         |                                               ^
         |                                               |
         |                                               |
         V                                               |
+------ip U-------+                             +------ip U--------+
|                 |                             |                  |
|  Transmitter    |                             |     Receiver     |
|                 |                             |                  |
+------ip CT------+                             +------ip CR-------+
         |                                               ^
         |                                               |
         |                                               |
         |                                               |
     +--ip CT------------------------------------------ip CR--+
     |                                                        |
     |                            medium                      |
     |                                                        |
     +--------------------------------------------------------+
}

type SeqType = integer;   { sequence number type, must be >= 0 }
    UserDataType = (Data, corr, AAAA, BBBB, CCCC, DDDD, EEEE);
    DTPDU = record
        Seq: SeqType;
        Msg: UserDataType;
    end;
    AKPDU = record
        Seq: SeqType;
    end;
 
channel UT(user, provider);
    by user:
        DR(Data : UserDataType);
    by provider:
        DI(Data : UserDataType);

channel M(DTSender, DTReceiver);
    by DTSender:
        DT(PDU : DTPDU);
    by DTReceiver:
        AK(PDU : AKPDU);

module User systemprocess;
    ip U : UT(user);
end;

body UBT for User;
#include "tuser1"
end;

body UBR for User;
#include "ruser"
end;

module Cms systemprocess;
    ip CT : M(DTReceiver);
       CR : M(DTSender);
end;

body CB for Cms;
#include "med" 
end;

module T systemprocess;
    ip U  : UT(provider);
       CT : M(DTSender);
end;

{ T module body }
body TB for T;

    const tws = 7;

    type SaveBuffers = array[1..tws] of DTPDU;

    var buff : SaveBuffers;

    { save user data in buffer until acknowledgment }
    procedure BSave(s : SeqType; d : UserDataType);
     var i: integer;
     begin
      i := 1;
      while buff[i].Seq > 0 do i:=i+1;
      buff[i].Seq := s;
      buff[i].Msg := d;
     end;
           

    { free user data buffer entry after acknowledgment }
    procedure BFree(s : SeqType);
     var i: integer;
     begin
      i := 1;
      while buff[i].Seq <> s do i:=i+1;
      buff[i].Seq := 0;
      buff[i].Msg := corr;
     end;

    { retrieve user data entry from buffer }
    function BRet(s : SeqType; buff: SaveBuffers): UserDataType;
     var i: integer; re: UserDataType; 
     begin
      i := 1;
      while buff[i].Seq <> s do i:=i+1;
      re := buff[i].Msg; BRet:=re
     end;

    { construct a DT PDU from the user data and sequence number }
    function pdudt(s : SeqType; d : UserDataType) : DTPDU;
     var pd: DTPDU;
     begin
      pd.Seq := s; pd.Msg := d; pdudt := pd
     end; 

     function corrupted_ak(PDU : AKPDU): boolean;
       begin
          if PDU.Seq=0 then corrupted_ak:=true else corrupted_ak:=false
       end;

    var
        lu : SeqType;
        hs : SeqType;
        stw, timout : integer;

    initialize
            provided (tws > 0)
                var i: integer;
                begin
                    lu := 1;
                    hs := 0;
                    stw := tws;
                    timout := 1000;
                    for i:=1 to tws do
                     begin
                      buff[i].Seq := 0; buff[i].Msg := Data
                     end;
                end;

    trans

        { transmit while window not full }
            when U.DR
                provided hs - lu +1 < stw
                    begin
                        hs := hs + 1;
                        output CT.DT(pdudt(hs, Data));
                        BSave(hs, Data);
                    end;

        { receive acknowledgment }
         trans
            when CT.AK
                provided (PDU.Seq >= lu) and
                         (PDU.Seq <= hs) and
                         not corrupted_ak(PDU)
                    var S : SeqType;
                    begin
                        for S := lu to PDU.Seq do
                            begin
                                BFree(S);
                            end;
                        lu := PDU.Seq + 1;
                    end;

        { receive ack not in window }
                provided otherwise
                    begin
                     { ignore this ack }
                    end;

        { no response before timeout; retransmission }
         trans
                provided (hs >= lu)
                 delay(timout)
                    var S : SeqType;
                    begin
                        for S := lu to hs do
                            begin
                                output CT.DT(pdudt(S,
                                             BRet(S,buff)));
                            end;
                    end;

end; { TB }


module R systemprocess;
    ip U  : UT(provider);
       CR : M(DTReceiver);
end;

{ Receiver module body }
body RB for R;

    const rws = 4;

    type SaveBuffers = array[1..rws] of DTPDU;

    var rbuff : SaveBuffers;

    { construct an AK PDU, given the sequence number }
    function pduak(S : SeqType) : AKPDU;
     var pd: AKPDU;
     begin pd.Seq := S; pduak:=pd end;

    { retrieve the PDU of sequence number S from the buffer.  If it
      is not in the buffer, return a PDU with seq number set to 0 }
    procedure pdur(S : SeqType; var pd: DTPDU);
     var i: integer; 
     begin
      pd.Seq := 0; 
      pd.Msg := Data; 
      i := 1;
      while (i <= rws) DO 
       begin
        if rbuff[i].Seq=S then
         begin
          pd.Seq := rbuff[i].Seq;
          pd.Msg := rbuff[i].Msg;
         end;
        i:=i+1;
       end;
      end;

   { remove from the buffer }
    procedure RBFree(s : SeqType);
     var i: integer;
     begin
      i:=1;
      while rbuff[i].Seq <> s do i:=i+1;
      rbuff[i].Seq:=0;
      rbuff[i].Msg:=Data;
     end;

    { Save the PDU in the buffer }
    procedure PDUSave(PDU : DTPDU);
     var i: integer;
     begin
      i := 1;
      while rbuff[i].Seq > 0 do i:=i+1;
      rbuff[i].Seq := PDU.Seq;
      rbuff[i].Msg := PDU.Msg;
     end;

    { returns true if the PDU is corrupted }
    function corrup(PDU: DTPDU) : boolean;
     begin
      if PDU.Msg = corr 
         then corrup := true
         else corrup := false;
     end;

    function received(s: SeqType; rws: integer; rbuff: SaveBuffers): boolean;
     var i : integer;
      begin
       received:=false;
       i := 1;
       while(i<=rws) do
        begin
         if rbuff[i].Seq=s  
          then received:=true;
         i:=i+1;
        end;
      end;

    var
        next : SeqType;
        hr : SeqType;
        srw : integer;

    initialize
            provided rws > 0
                var i :integer;
                begin
                    next := 1;
                    hr := 0;
                    srw := rws;
                    for i:=1 to srw do
                     begin
                      rbuff[i].Seq := 0; rbuff[i].Msg := Data
                     end;
                end;

    trans

        { receive message in window }
            when CR.DT
                provided (PDU.Seq >= next) and
                         (PDU.Seq <  next + srw) and
                         not corrup(PDU) and
                         not received(PDU.Seq, rws, rbuff)
                    var
                        S    : SeqType;
                        UD : DTPDU;
                        Done : boolean;
                    begin
                        PDUSave(PDU);
                        S := next;
                        srw := srw-1;
                        Done := false;
                        { Retrieve each PDU from buffer and send it
                          to the user.  Stop when we reach the first
                          gap in the buffer, i.e., the first PDU that
                          has not been received.  pdur returns
                          a PDU with sequence number 0 if the desired
                          PDU is not in the buffer. }
                        repeat
                            pdur(S, UD);
                            if UD.Seq = S then
                                begin
                                    { extract user data from PDU and
                                      send to user }
                                    output U.DI(UD.Msg);
                                    RBFree(S);
                                    srw := srw+1;
                                    S := S + 1;
                                end
                            else
                                { reached gap in buffer }
                                Done := true;
                        until Done;
                        next := S;
                        output CR.AK(pduak(next - 1));
                    end;

                { receive message not in window or is corrupted }
                provided otherwise
                    begin
                        output CR.AK(pduak(next - 1));
                    end;

end; { RB }

{ main body for Sliding Window specification }
modvar
    TIns : T;
    RIns : R;
    TUserIns, RUserIns : User;
    CmsIns : Cms;

    initialize
        begin
            init TUserIns with UBT;
            init RUserIns with UBR;
            init TIns with TB;
            init RIns with RB;
            init CmsIns with CB;
            connect TUserIns.U to TIns.U;
            connect RUserIns.U to RIns.U;
            connect TIns.CT to CmsIns.CT;
            connect RIns.CR to CmsIns.CR;
        end;
end. { specification SlidingWindowProtocol }