(* TMDL-to-LOTOS Compiler, version 0.9. *)

specification Map4[Answer, Connected, Dial, ErrorDial, OffHook, Ring, Tone]:noexit

library
   Boolean, NaturalNumber
endlib

(* Tag ADT definition *)
type Tag is Boolean, NaturalNumber
sorts Tag
opns dummy_val, OK, TOut : -> Tag
     N : Tag -> Nat
     _eq_, _ne_ : Tag, Tag ->Bool
eqns forall x, y: Tag
     ofsort Nat
     N(dummy_val)= 0;   (* dummy value *)
     N(OK) = Succ(N(dummy_val));
     N(TOut) = Succ(N(OK));
     ofsort Bool
     x eq y = N(x) eq N(y);
     x ne y = not(x eq y);
endtype

behaviour

hide EndDial, GiveTone, GotDial in

   (
      ConnectionPhase[Answer, Connected, EndDial, ErrorDial, GiveTone, GotDial, OffHook, Ring]
      |[EndDial, GiveTone, GotDial]|
      Dialing[Dial, EndDial, GiveTone, GotDial, Tone]
   )

where

   process ConnectionPhase[Answer, Connected, EndDial, ErrorDial, GiveTone, GotDial, OffHook, Ring]:noexit :=

   hide CheckDB, RegInit, Sync_Time_1, TimeOut_0 in

      OffHook;
      (
         RegInit;
         GiveTone;
         (
            TimeOut_0;  (* Timeout occured *)
            Sync_Time_1 ! TOut; stop
            []
            GotDial;  (* Event occured *)
            Sync_Time_1 ! OK; stop
         )
         |[Sync_Time_1]|
         Sync_Time_1 ? TimeGotDial:Tag;
         (
            (
               [TimeGotDial eq TOut]->
               EndDial;  (* Abort event *)
               ErrorDial; stop  (* No recursion *)
            )
            []
            (
            [TimeGotDial eq OK]->
               CheckDB;
               Ring;
               Answer;
               Connected; stop  (* No recursion *)
            )
         )
      )
   endproc  (* Timethread ConnectionPhase *)

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

   process Dialing[Dial, EndDial, GiveTone, GotDial, Tone]:noexit :=
      (
         GiveTone;
         (
            Tone;
            Dial;
            GotDial; stop  (* No recursion *)
         )
      )
      [> enddial; Dialing[Dial, EndDial, GiveTone, GotDial, Tone]
   endproc  (* Timethread Dialing *)

endspec (* Map Map4 *)