connect.lot

• LOTOS Specification
• Process list
• Type list

LOTOS Specification

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

specification SimpleConnection[Answer, BusyTone, Connected, Dial, OffHook, Ring, Tone]:noexit

library
   Boolean, NaturalNumber
endlib

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

behaviour
   (
      ConnectionPhase[Answer, BusyTone, Connected, Dial, OffHook, Ring, Tone]
   )

where

   process ConnectionPhase[Answer, BusyTone, Connected, Dial, OffHook, Ring, Tone]:noexit :=

   hide CheckDB, RegInit in

      OffHook;
      (
         RegInit;
         Tone;
         Dial;
         CheckDB;
         (
            (
               BusyTone; stop  (* No recursion *)
            )
            []
            (
               Ring;
               Answer;
               Connected; stop  (* No recursion *)
            )
         )
      )
   endproc  (* Timethread ConnectionPhase *)

endspec (* Map SimpleConnection *)

List of Processes

• process ConnectionPhase
  

List of Types

• type Tag