(* 
   Original specification of the service, by D. Hogrefe (April 1991)
   No loss
   No retransmission
   No time out
   One ISDU type
*)

specification Inres_service[ISAPini, ISAPres]:noexit

library INRES_SERVICE endlib

behaviour
	(ICEPini[ISAPini]
	|||
	ICEPres[ISAPres])
	||
	EndtoEnd[ISAPini,ISAPres]

where
process ICEPini[g]:noexit:=
	(ConnectionphaseIni[g]
	>>
	DataphaseIni[g])
	[>
	DisconnectionIni[g]
where
	process ConnectionphaseIni[g]:exit:=
		g !ICONreq;
		g !ICONconf;
		exit
	endproc (* ConnectionphaseIni *)

	process DataphaseIni[g]:noexit:=
		g !IDATreq ?var:ISDU;
		DataphaseIni[g]
	endproc (* DataphaseIni *)

	process DisconnectionIni[g]:noexit:=
		g !IDISind;
		ICEPini[g]
	endproc (* DisconnectionIni *)

endproc (* ICEPini *)

process ICEPres[g]:noexit:=
	ConnectionphaseRes[g]
	>>
        (
         (WaitRes[g]>>DataphaseRes[g])
	 [>
	 DisconnectionRes[g]
        )
where
	process ConnectionphaseRes[g]:exit:=
		g !ICONind;
		exit
	endproc (* ConnectionphaseRes *)

        process WaitRes[g]:exit:=
                g !ICONresp;
                exit
        endproc
	process DataphaseRes[g]:noexit:=
		g !IDATind ?var:ISDU;
		DataphaseRes[g]
	endproc (* DataphaseRes *)

	process DisconnectionRes[g]:noexit:=
		g !IDISreq;
		ICEPres[g]
	endproc (* DisconnectionRes *)

endproc (* ICEPres *)

process EndtoEnd[ini,res]:noexit:=
	( ConnectionphaseEte[ini,res]
          >>
          DataphaseEte[ini,res]
        )
        [>
        DisconnectionEte[ini,res]

	where

	  process ConnectionphaseEte[ini,res]:exit:=
            ( ini! ICONreq;
	      res! ICONind;
              exit
            )
            |||
            ( res! ICONresp;
              ini! ICONconf;
              exit
            )
          endproc (* ConnectionphaseEte *)

          process DataphaseEte[ini,res]:noexit:=
	    ini! IDATreq?var:ISDU;
	    res! IDATind!var;
	    DataphaseEte[ini,res]
	  endproc (* DataphaseEte *)

	  process DisconnectionEte[ini,res]:noexit:=
	    res! IDISreq;
	    ini! IDISind;
	    EndtoEnd[ini,res]
	    []
	    i;
	    ini! IDISind;
	    EndtoEnd[ini,res]
	  endproc (* DisconnectionEte *)

	endproc (* EndtoEnd *)

endspec (* Inres_service *)