(* 
   INRES protocol specification, by K. H. Pang at INT (July 1992, V5)
   changes wrt V4
   - Added Channel loss
   - Changed Responder disconnection code to discard ipdus 
     received during disconnection
*)


Specification Inres_Protocol[ISAPini,ISAPres]:noexit

library BOOLEAN endlib
library INRES_PROTOCOL endlib

behaviour
  hide MSAP1,MSAP2 in
              Station_Ini[ISAPini,MSAP1](1 of DecNumb)
              (* maximum number of transmissions equal to 1 *)
    |[MSAP1]| Medium[MSAP1,MSAP2]
    |[MSAP2]| Station_Res[MSAP2,ISAPres]

  where

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

  process Medium [MSAP1,MSAP2] :noexit:=
       Channel[MSAP1,MSAP2]
    ||| Channel[MSAP2,MSAP1]

    where

    process Channel[a,b] :noexit:=
      a?d:MSP [isMDATreq(d)];
      (
         b!MDATind(data(d));Channel[a,b]
       []Channel[a,b]
      )
    endproc (* Channel *)
  endproc (* Medium *)

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

  process Station_Ini[ISAPini,MSAP1](max:DecNumb) :noexit:=
    hide IPdu_ini in
                    Station[ISAPini,IPdu_ini](max)
       |[IPdu_ini]| Coder[IPdu_ini,MSAP1]

    where

    (*==========================================================*)

    process Station[ISAP,IPdu](max:DecNumb) :noexit:=
      Initiator[ISAP,IPdu](max) [> Disconnection[ISAP,IPdu](max)

      where

      (*------------------------------------------------------*)

      process Initiator[ISAP,IPdu](max:DecNumb) :noexit:=
        Connectionphase[ISAP,IPdu](max)
          >> Dataphase[ISAP,IPdu] (succ(0),max)

        where

        (*..................................................*)

        process Connectionphase[ISAP,IPdu](max:DecNumb) :exit:=
          Connectrequest[ISAP,IPdu]
            >> accept z:DecNumb in Wait[ISAP,IPdu](z,max)

          where

          process Connectrequest[ISAP,IPdu] :exit(DecNumb):=
            ISAP!ICONreq;Conn2[ISAP,IPdu]

	    where

            process Conn2[ISAP,IPdu] :exit(DecNumb):=
              IPdu!CR;exit(s(0))
              (* User errors are ignored *)
            []IPdu?ipdu:IPDU[isCC(ipdu) or isAK(ipdu)];Conn2[ISAP,IPdu]
              (* DR is only accepted by process Disconnection *)
              (* System errors are ignored *)
            endproc (* Conn2 *)
          endproc (* Connectrequest *)

          process Wait[ISAP,IPdu](z,max:DecNumb) :exit:=
            IPdu?ipdu:IPDU[isCC(ipdu)];ISAP!ICONconf;exit
          []IPdu?ipdu:IPDU[isAK(ipdu)];Wait[ISAP,IPdu](z,max) 
            (* DR is only accepted by process Disconnection *)
            (* System errors are ignored *)
          []i;(
                 [z <  max]->IPdu!CR;Wait[ISAP,IPdu](s(z),max)
               [][z == max]->ISAP!IDISind;Connectionphase[ISAP,IPdu](max)
              )
              (* Timeout *)
          endproc (* Wait *)
        endproc (* Connectionphase *)

        (*..................................................*)

        process Dataphase[ISAP,IPdu](number:Sequencenumber,max:DecNumb) :noexit:=
          Readytosend[ISAP,IPdu](number) (* 1 is the first Sequencenumber *)
            >>accept z:DecNumb,number:Sequencenumber,olddata:ISDU
              in Sending[ISAP,IPdu](z,number,olddata,max)
                (* z is number of sendings. At the beginning z=1 *)

          where

          process Readytosend[ISAP,IPdu](number:Sequencenumber):
            exit(DecNumb,Sequencenumber,ISDU):=
             (choice y:ISDU []
                     ISAP !IDATreq(y);Readytosend2[ISAP,IPdu](number,y))

            where

            process Readytosend2[ISAP,IPdu](number:Sequencenumber,y:ISDU):
              exit(DecNumb,Sequencenumber,ISDU):=
              IPdu!DT(number,y);exit(s(0),number,y)
            []IPdu?ipdu:IPDU[isCC(ipdu) or isAK(ipdu)];Readytosend2[ISAP,IPdu](number,y)
            endproc (* Readytosend2 *)
          endproc (* Readytosend *)

          process Sending[ISAP,IPdu]
            (z:DecNumb,number:Sequencenumber,olddata:ISDU,max:DecNumb):noexit:=
            ( 
              IPdu?ipdu:IPDU[isAK(ipdu)];
              (
                [(num(ipdu) eq number)]->Dataphase [ISAP,IPdu](succ(number),max)
              [][(num(ipdu) ne number) and (z < max)]->Sending2[ISAP,IPdu](z,number,olddata,max)
                (* The Initiator shall not resend more than max times in case of *)
                (* faulty transmission *)
              [][(num(ipdu) ne number) and (z == max)]->ISAP!IDISind;
                                                        Initiator[ISAP,IPdu](max) 
              )
            []IPdu?ipdu:IPDU[isCC(ipdu)];Sending[ISAP,IPdu](z,number,olddata,max)
            []i;(
                  [z <  max]->IPdu!DT(number,olddata);
                              Sending[ISAP,IPdu](s(z),number,olddata,max)
                [][z == max]->ISAP!IDISind;Initiator[ISAP,IPdu](max)
                ) 
            )

            where

            process Sending2[ISAP,IPdu]
              (z:DecNumb,number:Sequencenumber,olddata:ISDU,max:DecNumb):noexit:=
              IPdu!DT(number,olddata);Sending[ISAP,IPdu](s(z),number,olddata,max)
            []IPdu?ipdu:IPDU[isCC(ipdu)];Sending2[ISAP,IPdu](z,number,olddata,max)
            endproc (* Sending2 *)
          endproc (* Sending *)
        endproc (* Dataphase *)

        (*..................................................*)

      endproc (* Initiator *)

      (*-------------------------------------------------------*)

      process Disconnection[ISAP,IPdu](max:DecNumb):noexit:=
        IPdu!DR;ISAP!IDISind;Station[ISAP,IPdu](max)
      endproc (* Disconnection *)

      (*-------------------------------------------------------*)

    endproc (* Station *)

    (*===========================================================*)

    process Coder[IPdu,MSAP] :noexit:=
      Up[IPdu,MSAP]|||Down[IPdu,MSAP]

      where

      process Up[IPdu,MSAP]:noexit:=
        MSAP!MDATind(CC);IPdu!CC;Up[IPdu,MSAP]
      []MSAP!MDATind(DR);IPdu!DR;Up[IPdu,MSAP]
      [](choice x:SequenceNumber []
                   MSAP!MDATind(AK(x));IPdu!AK(x);Up[IPdu,MSAP])
      endproc (* Up *)

      process Down[IPdu,MSAP]:noexit:=
        (IPdu!CR;MSAP!MDATreq(CR);Down[IPdu,MSAP]
      [](choice x:SequenceNumber, y:ISDU []
                   IPdu!DT(x,y);MSAP!MDATreq(DT(x,y));Down[IPdu,MSAP]))
      endproc (* Down *)
    endproc (* Coder *)

    (*===========================================================*)

  endproc (* Station_Ini *)

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

  process Station_Res[MSAP2,ISAPres] :noexit:=
    hide IPdu_res in 
                     Responder[ISAPres,IPdu_res]
        |[IPdu_res]| Coder[IPdu_res,MSAP2]

    where

    (*============================================================*)

    process Responder[ISAP,IPdu]:noexit:=
      Connectrequest[ISAP,IPdu] 
        >>(
           (Wait[ISAP,IPdu]>>Dataphase[ISAP,IPdu](succ(1)))
             [>Disconnection[ISAP,IPdu] 
          )

      where

      (*--------------------------------------------------------*)

      process Connectrequest[ISAP,IPdu]:exit:=
        (IPdu?ipdu:IPDU[isCR(ipdu)];ISAP!ICONind;exit
       []IPdu?ipdu:IPDU[isDT(ipdu)];Connectrequest[ISAP,IPdu])
            (* System errors are ignored *)
      endproc (* Connectrequest *)

      (*--------------------------------------------------------*)

      process Wait[ISAP,IPdu] :exit:=
        ISAP!ICONresp;Wait2[ISAP,IPdu]

	where

	process Wait2[ISAP,IPdu]:exit:=
	  IPdu!CC;exit
	[]IPdu?ipdu:IPDU[isCR(ipdu) or isDT(ipdu)];Wait2[ISAP,IPdu]
	endproc (* Wait2 *)
      endproc (* Wait *)

      (*--------------------------------------------------------*)

      process Dataphase[ISAP,IPdu](number:Sequencenumber):noexit:=
        (* number is the last acknowledged Sequencenumber *)
        ( 
           IPdu?ipdu:IPDU[isDT(ipdu)];
           (
             [(num(ipdu) eq succ(number))]->ISAP!IDATind(data(ipdu));
                                             IPdu!AK(num(ipdu));
                                             Dataphase[ISAP,IPdu](succ(number))
            [][(num(ipdu) eq number)]     ->IPdu!AK(num(ipdu)); 
                                             Dataphase[ISAP,IPdu](number)
           )
         []IPdu?ipdu:IPDU[isCR(ipdu)];ISAP!ICONind;Wait[ISAP,IPdu]
        )
  
        where

        process Wait[ISAP,IPdu]:noexit:=
          ISAP!ICONresp;Wait2[ISAP,IPdu]

	  where

	  process Wait2[ISAP,IPdu]:noexit:=
	    IPdu!CC;Dataphase[ISAP,IPdu](succ(1))
	  []IPdu?ipdu:IPDU[isDT(ipdu) or isCR(ipdu)];Wait2[ISAP,IPdu]
           (* System errors are ignored *)
	  endproc (* Wait2 *)
        endproc (* Wait *)
      endproc (* Dataphase *)

      (*-------------------------------------------------------*)

      process Disconnection[ISAP,IPdu] :noexit:=
        ISAP!IDISreq;Disc2[ISAP,IPdu]

	where

        (* Disc2 rejects all ipdu's while Responder is disconnecting *)
        process Disc2[ISAP,IPdu] :noexit:=
          IPdu!DR;Responder[ISAP,IPdu]
        []IPdu!CR;Disc2[ISAP,IPdu]
        [](choice x:SequenceNumber, y:ISDU [] IPdu!DT(x,y);Disc2[ISAP,IPdu])
        endproc (* Disc2 *)
      endproc (* Disconnection *)

      (*-------------------------------------------------------*)

    endproc (* Responder *)

    (*===========================================================*)

    process Coder[IPdu,MSAP] :noexit:=
      Up[IPdu,MSAP]|||Down[IPdu,MSAP]

      where

      process Up[IPdu,MSAP]:noexit:=
         MSAP!MDATind(CR);IPdu!CR;Up[IPdu,MSAP]
       [](choice x:SequenceNumber, y:ISDU []
          MSAP!MDATind(DT(x,y));IPdu!DT(x,y);Up[IPdu,MSAP])
      endproc (* Up *)

      process Down[IPdu,MSAP]:noexit:=
        IPdu!CC;MSAP!MDATreq(CC);Down[IPdu,MSAP]
      []IPdu!DR;MSAP!MDATreq(DR);Down[IPdu,MSAP]
      [](choice x:SequenceNumber  []
         IPdu!AK(x);MSAP!MDATreq(AK(x));Down[IPdu,MSAP])
      endproc (* Down *)
    endproc (* Coder *)

    (*===========================================================*)

  endproc (* Station_Res *)

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

endspec (* Inres_Protocol *)