{This is an AbraProtocol, completed for simulation with
 unreliable medium and two symmetrical users (in case of "ABuser"
 include). The specification of the protocol part itself is directly
 composed of AbraService and SWP Transmitter/Receiver (with windows =1)
 interfaced through a CoderDecoder module coding and decoding
 the AbraService primitives}

specification ABPSim;

(******************ABPSim External Modules' Interfaces***************)

default individual queue;
timescale milisecond;

type
     UserDataType = (AAAA, BBBB, CCCC, DDDD, EEEE, Data, corr); 
     PDUType = (CRr, DT, CC, DR, DC);
     SDUType = record
                PDU:   PDUType;
                UData: UserDataType
               end;

     SeqType = integer;
     DTPDU = record
              Seq: SeqType;
              Msg: SDUType;
             end;
     AKPDU = record
              Seq: SeqType;
             end;

channel USAB(user, provider);
    by user:
        ConReq;
        ConResp;
        DatReq(SDU : UserDataType);
        DisReq;
    by provider:
        ConInd;
        ConConf;
        DatInd(SDU : UserDataType);
        DisInd;

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

(****************************ABPSim Modules***********************)


module ABuser systemprocess;
    ip UA: USAB (user);
end;
body ABuserBody for ABuser;
{An outermost user for Abra (Service or Protocol)
 that repeats, after receiving ConConf or ConInd,
 m times k DatReq, for each k, UserData
 are different;}

    const m=1; k=2;
   
    var Dat: array[1..5] of UserDataType; 
        a, test: boolean;
	r : real;
	u : integer;
	p : real;

	(* ################## CHOICE ####################### *)

procedure choice(m: integer;var j: integer);
(* This procedure draws a random integer between 0 and m-1 *)
 begin
  u := (16807*u) mod 2147483647;
  j := u mod m
 end;

	(* ################### DRAW ######################## *)

procedure draw(p: real;var test: boolean);
(* This procedure draws TRUE with a probalility p*)
 begin
  r := 16807*r-trunc(16807*r);
  if r<=p then test := true else test := false
 end;

state DISC, CONN;
stateset AL =[DISC, CONN];

initialize to DISC
    var i: integer;
    begin 
     r := 0.175555987;
     u := 377003616; p := 0.25;
     Dat[1]:=AAAA; Dat[2]:=BBBB;
     Dat[3]:=CCCC; Dat[4]:=DDDD; 
     Dat[5]:=EEEE; a:= true
    end;

trans    
 from AL to CONN
   when UA.ConInd
     begin output UA.ConResp end;
 from AL to CONN
   when UA.ConConf
     begin end;
 from AL to same
   when UA.DatInd
     begin end;
 from AL to DISC
   when UA.DisInd
     begin end;
 from DISC to same
     begin output UA.ConReq end;
 from CONN to DISC
     begin output UA.DisReq end;
 from CONN to same
       var i,j: integer;
       begin
        for i := 1 to m do
          for j:=1 to k do
           output UA.DatReq(Dat[j]);
       end;
end;

module AbraProtocol;
    ip UA: USAB (provider);
       CT : M(DTSender);
       CR : M(DTReceiver);
end;
body AbraProtocolBody for AbraProtocol;
{specification of the AbraProtocol which is directly
 composed of AbraService and SWP Transmitter/Receiver (with windows =1)
 interfaced through a CoderDecoder module coding and decoding
 the AbraService primitives}

(******************AbraProtocol Outermost Interface******************)
{
type UserDataType = ...;
 
     PDUType = (CR, DT, CC, DR, DC);
     SDUType = record
                PDU:   PDUType;
                UData: UserDataType
               end;

    SeqType = integer;
     DTPDU = record
              Seq: SeqType;
              Msg: SDUType;
             end;
     AKPDU = record
              Seq: SeqType;
             end;

channel USAB(user, provider);
    by user:
        ConReq;
        ConResp;
        DatReq(SDU : UserDataType);
        DisReq;
    by provider:
        ConInd;
        ConConf;
        DatInd(SDU : UserDataType);
        DisInd;

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

module AbraProtocol;
    ip UA: USAB (provider);
       CT : M(DTSender);
       CR : M(DTReceiver);
end;

body AbraProtocolBody for AbraProtocol;
}
(*****************************************************************)

(******************AbraProtocol Internal Interfaces***************)
channel ABCD(AB, CD);
    by AB, CD:
        ConReq;
        ConResp;
        DatReq(SDU : UserDataType);
        DisReq;
        ConInd;
        ConConf;
        DatInd(SDU : UserDataType);
        DisInd;

channel UT(user, provider);
    by user:
        DR(Data : SDUType);
    by provider:
        DI(Data : SDUType);
(*****************************************************************)

(******************AbraProtocol Internal Modules******************)

module AbraServ systemprocess;
    ip 
      UA:  USAB (provider);
      UB:  ABCD (AB);
end;
body AbraServBody for AbraServ; 
{ Estelle specification of the "Abracadabra Service" (abs.stl)
  modified to be used directly (included) as a part 
  of AbraProtocol specification (ABprotArch)}
 

(******************AbraServ Outermost Interface******************)
{
default individual queue;

type UserDataType = ...;

channel USAB(user, provider);
    by user:
        ConReq;
        ConResp;
        DatReq(SDU : UserDataType);
        DisReq;
    by provider:
        ConInd;
        ConConf;
        DatInd(SDU : UserDataType);
        DisInd;

module AbraServ systemprocess;
    ip 
      UA:  USAB (provider);
      UB:  USAB (provider);
end;

body AbraServBody for AbraServ;
}
(*****************************************************************)

state DISCONNECTED, A_CALLING_B, B_CALLING_A, CONNECTED;
stateset 
   ACTIVE = [A_CALLING_B, B_CALLING_A, CONNECTED];
   A_ConReqIgnore = [CONNECTED, A_CALLING_B];
   A_ConRespIgnore = [DISCONNECTED, CONNECTED, A_CALLING_B];
   B_ConReqIgnore = [CONNECTED, B_CALLING_A];
   B_ConRespIgnore = [DISCONNECTED, CONNECTED, B_CALLING_A];
   DatReqIgnore = [DISCONNECTED, A_CALLING_B, B_CALLING_A];
   DisReqIgnore = [DISCONNECTED];

initialize
    to DISCONNECTED
        begin
        end;

trans
    from DISCONNECTED to A_CALLING_B
        when UA.ConReq
             begin
               output UB.ConReq
             end;
    from DISCONNECTED to B_CALLING_A
        when UB.ConReq
             begin
               output UA.ConInd
             end;

    from B_CALLING_A to CONNECTED
           when UA.ConResp
              begin
                output UB.ConResp;
              end;
    from A_CALLING_B to CONNECTED
           when UB.ConResp
              begin
                output UA.ConConf;
              end;

    from B_CALLING_A to CONNECTED
           when UA.ConReq
              begin
               output UA.ConConf;
               output UB.ConReq;
              end;
    from A_CALLING_B to CONNECTED
           when UB.ConReq
              begin
               output UA.ConConf;
               output UB.ConConf;
              end;

    from CONNECTED to same
           when UA.DatReq(SDU)
              begin
                output UB.DatReq(SDU)
              end;
           when UB.DatReq(SDU)
              begin
                output UA.DatInd(SDU)
              end;

    from ACTIVE to DISCONNECTED
           when UA.DisReq
              begin
                output UB.DisReq
              end;
           when UB.DisReq
              begin
                output UA.DisInd
              end;
           {when UA.DisReq & UB.DisReq  not in Estelle
              begin
              end;}

    from ACTIVE to DISCONNECTED
              begin
                output UA.DisInd;
                output UB.DisInd
              end;

    from A_ConReqIgnore to same
           when UA.ConReq
               begin
               end;
    from B_ConReqIgnore to same
           when UB.ConReq
               begin
               end;
    from A_ConRespIgnore to same
           when UA.ConResp
               begin
               end;
    from B_ConRespIgnore to same
           when UB.ConResp
               begin
               end;
    from DatReqIgnore to same
           when UA.DatReq 
               begin
               end;
    from DisReqIgnore to same
           when UA.DisReq
               begin
               end;
    from DatReqIgnore to same
           when UB.DatReq 
               begin
               end;
    from DisReqIgnore to same
           when UB.DisReq
               begin
               end;

{end;} 
(*****************************************************************)

end;

module CodeDecode systemprocess;
    ip 
      UB:  ABCD (CD);
      CDSend, CDRecv: UT(user); 
end;
body CodeDecodeBody for CodeDecode;
{body CodeDecodeBody for CodeDecode;}

const adata = Data; {any UserDataType;}

var Z: SDUType;

procedure CodeSDU (X: PDUType; Y: UserDataType; var Z: SDUType);
begin
   Z.PDU := X; Z.UData := Y
end;

initialize begin end;

trans
when UB.ConReq
 begin CodeSDU(CRr, adata, Z); output CDSend.DR(Z) end;

when UB.ConResp
 begin CodeSDU(CC, adata, Z); output CDSend.DR(Z)  end;

when UB.DatReq(SDU)
 begin CodeSDU(DT, SDU, Z); output CDSend.DR(Z)  end;

when UB.DisReq
 begin CodeSDU(DR, adata, Z); output CDSend.DR(Z)  end;

when UB.ConConf
 begin CodeSDU(CC, adata, Z); output CDSend.DR(Z)  end;

when UB.DisInd
 begin CodeSDU(DC, adata, Z); output CDSend.DR(Z)  end;

when CDRecv.DI(Data)
 begin
   if Data.PDU = CRr then output UB.ConReq;
   if Data.PDU = DT then output UB.DatReq(Data.UData);
   if Data.PDU = CC then output UB.ConResp;
   if Data.PDU = DR then output UB.DisReq;
   if Data.PDU = DC then;
 end;

{end;}
end;
 
module Transmitter systemprocess;
    ip U  : UT(provider);
       CT : M(DTSender);
end;
body TransmitterBody for Transmitter;
{specification SlidingWindowProtocol;

  Estelle specification of the "Sliding Window Protocol" 
  Transmitter to be directly used (included) into 
  AbraProtocol specification as a part assuring reliability
  of transmission (window size =1 to emulate AlternatingBit
  to some extent - no limit on number of retransmissions)
}
(*****************Transmitter Outermost Interface************)

{
timescale milisecond;


type SeqType = integer; 

channel UT(user, provider);
    by user:
        DR(Data : SDUType);
    by provider:
        DI(Data : SDUType);
 
channel M(DTSender, DTReceiver);
    by DTSender:
        DT(PDU : DTPDU);
    by DTReceiver:
        AK(PDU : AKPDU);
 
module Transmitter systemprocess;
    ip U  : UT(provider);
       CT : M(DTSender);
end;
body TransmitterBody for Transmitter;
}
(**********************************************************)

    const tws = 1;

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

    var buff : SaveBuffers;

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

     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;
     end;

    { retrieve user data entry from buffer }
    function BRet(s : SeqType; buff: SaveBuffers): SDUType;
     var i: integer; re: SDUType; 
     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 : SDUType) : DTPDU;
     var pd: DTPDU;
     begin
      pd.Seq := s; pd.Msg.PDU := d.PDU;
      pd.Msg.UData := d.UData; 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;
                     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;}
(*****************************************************************)
end;

module Receiver systemprocess;
    ip U  : UT(provider);
       CR : M(DTReceiver);
end;
body ReceiverBody for Receiver;
{ Estelle specification of the "Sliding Window Protocol" 
  Rceiver to be directly used (included) into 
  AbraProtocol specification as a part assuring reliability
  of transmission (window size =1 to emulate AlternatingBit
  to some extent - no limit on number of retransmissions) }

(*****************Receiver Outermost Interface*************)

{
timescale milisecond;


type SeqType = integer; 

channel UT(user, provider);
    by user:
        DR(Data : SDUType);
    by provider:
        DI(Data : SDUType);
 
channel M(DTSender, DTReceiver);
    by DTSender:
        DT(PDU : DTPDU);
    by DTReceiver:
        AK(PDU : AKPDU);

module Receiver systemprocess;
    ip U  : UT(provider);
       CR : M(DTReceiver);
end;
body ReceiverBody for Receiver; 
}
(**********************************************************)

    const rws = 1;

    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; 
      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;
     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.UData = 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;
                     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; }
(*****************************************************************)

end;

(*****************************************************************)

(*************AbraProtocol Internal Module Structure**************)
modvar
    ABInst: AbraServ;
    CDInst: CodeDecode;
    TInst: Transmitter;
    RInst: Receiver;

initialize
    begin
        init ABInst with AbraServBody;
        init CDInst with CodeDecodeBody;
        init TInst with TransmitterBody;
        init RInst with ReceiverBody;
        attach UA to ABInst.UA;
        attach CT to TInst.CT;
        attach CR to RInst.CR;
        connect ABInst.UB to CDInst.UB;
        connect CDInst.CDSend to TInst.U;
        connect CDInst.CDRecv to RInst.U;
    end;

(*****************************************************************)
{
end;
}
end;

module Medium systemprocess;
    ip 
       CT: M(DTReceiver);
       CR: M(DTSender);
end;
body MediumBody for Medium;
    var save : DTPDU;
    
    initialize
       begin save.Seq:=0 end;
     
    trans
      when CT.DT
        name norm_data:
        begin 
         output CR.DT(PDU);
         if save.Seq>0 then
          begin output CR.DT(save);save.Seq:=0 end
        end;
      when CT.DT
        name corr_data:
        begin 
         PDU.Msg.UData :=corr;output CR.DT(PDU);
         if save.Seq>0 then
          begin output CR.DT(save);save.Seq:=0 end 
        end;
      when CT.DT
        name lost_data:
        begin 
         if save.Seq>0 then 
          begin output CR.DT(save);save.Seq:=0 end
        end;
      when CT.DT
        name dupl_data:        
        begin 
         output CR.DT(PDU); output CR.DT(PDU);
         if save.Seq>0 then
          begin output CR.DT(save);save.Seq:=0 end 
        end;
      when CT.DT
        name reor_data:
        begin 
         if save.Seq>0 then 
          begin output CR.DT(save);save:=PDU end         
        end;

     trans
       when CR.AK
         name norm_ak:
         begin output CT.AK(PDU) end;
       when CR.AK
         name lost_ak:
         begin  end;
end;
(*****************************************************************)

(******************ABPSim Modules' Structure******************)

modvar
    APInst1, APInst2: AbraProtocol;
    UInst1, UInst2: ABuser;
    MInst1, MInst2: Medium;

initialize
    begin
        init APInst1 with AbraProtocolBody;
        init APInst2 with AbraProtocolBody;
        init UInst1 with ABuserBody;
        init UInst2 with ABuserBody;
        init MInst1 with MediumBody;
        init MInst2 with MediumBody;
        connect APInst1.UA to UInst1.UA;
        connect APInst2.UA to UInst2.UA;
        connect APInst1.CT to MInst1.CT;
        connect APInst2.CT to MInst2.CT;
        connect APInst1.CR to MInst2.CR;
        connect APInst2.CR to MInst1.CR;
    end;
end.