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

specification Tests[Ab1, Ab2, Act1, Act10, Act11, Act12, Act13, Act3, Act4, Act5, Act6, Act7, Act8, Act9, R1, R2, R3, R4, R5, R6, R7, R8, Rfork1, Rfork2, Rfork3, Rfork4, Rfork5, T1, T2, T3, T4, T5, T6, T7, T8]:noexit

library
   Boolean, NaturalNumber
endlib

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

behaviour
   (
      (
         TestAbort[Ab1, Ab2, R1, T1]
         |[Ab1, Ab2]|
         (
            TestAborted1[Ab1, R2, T2]
            |||
            TestAborted2[Ab2, R3, T3]
         )
      )
      |||
      TestChoice[Act1, Act3, R4, T4]
      |||
      TestPar[Act4, Act5, Act6, R5, T5]
      |||
      TestForks[Act7, Act8, R6, Rfork1, Rfork2, Rfork3, Rfork4, Rfork5, T6]
      |||
      TestLoops[Act10, Act11, Act9, R7, T7]
      |||
      TestWP[Act12, Act13, R8, T8]
   )

where

   process TestAbort[Ab1, Ab2, R1, T1]:noexit :=
      T1;
      (
         Ab1;  (* Abort event *)
         Ab2;  (* Abort event *)
         R1; stop  (* No recursion *)
      )
   endproc  (* Timethread TestAbort *)

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

   process TestAborted1[Ab1, R2, T2]:noexit :=
      (
         T2;
         (
            R2; TestAborted1[Ab1, R2, T2]  (* End recursion *)
         )
      )
      [> ab1; TestAborted1[Ab1, R2, T2]
   endproc  (* Timethread TestAborted1 *)

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

   process TestAborted2[Ab2, R3, T3]:noexit :=
      (
         T3;
         (
            R3; stop
            |||
            TestAborted2[Ab2, R3, T3]  (* Parallel recursion *)
         )
      )
      [> ab2; TestAborted2[Ab2, R3, T3]
   endproc  (* Timethread TestAborted2 *)

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

   process TestChoice[Act1, Act3, R4, T4]:noexit :=

   hide Sync_Or_0, Sync_Or_1 in

      T4 ? Cond:Tag;
      (
         (
            (
               [Cond eq Yes]->
               Act1;
               Sync_Or_0 ! Cond;stop
            )
            []
            (
               (
                  (
                     Sync_Or_1 ! Cond;stop
                  )
                  []
                  (
                     [(Cond ne Yes) implies (not(Cond eq No))]->
                     (
                        Act3 ! Cond; stop
                        |||
                        Sync_Or_1 ! Cond;stop
                     )
                  )
               )
               |[Sync_Or_1]|
               Sync_Or_1 ? Cond:Tag;
               Sync_Or_0 ! Cond;stop
            )
         )
         |[Sync_Or_0]|
         Sync_Or_0 ? Cond:Tag;
         R4; stop  (* No recursion *)
      )
   endproc  (* Timethread TestChoice *)

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

   process TestPar[Act4, Act5, Act6, R5, T5]:noexit :=

   hide Sync_And_2, Sync_And_3 in

      T5 ? Cond:Tag;
      (
         (
            (
               Act4;
               Sync_And_2 ! Cond;stop
            )
            |[Sync_And_2]|
            (
               (
                  (
                     (
                        Act5 ! Cond; stop
                        |||
                        Sync_And_3 ! Cond;stop
                     )
                  )
                  |[Sync_And_3]|
                  (
                     Act6;
                     Sync_And_3 ! Cond;stop
                  )
               )
               |[Sync_And_3]|
               Sync_And_3 ? Cond:Tag;
               Sync_And_2 ! Cond;stop
            )
         )
         |[Sync_And_2]|
         Sync_And_2 ? Cond:Tag;
         R5; stop  (* No recursion *)
      )
   endproc  (* Timethread TestPar *)

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

   process TestForks[Act7, Act8, R6, Rfork1, Rfork2, Rfork3, Rfork4, Rfork5, T6]:noexit :=
      T6 ? Cond1:Tag ? Cond2:Tag;
      (
         (
            (
               (
                  Act7;
                  Rfork1; stop
                  |||
                  Rfork2 ! Cond1; stop
                  |||
                  Act8;
                  Rfork3; stop
                  |||
                  Rfork4; stop  (* No recursion *)
               )
            )
            []
            (
               Rfork5; stop  (* No recursion *)
            )
            []
            (
            [Cond2 ne No]->
               R6; stop  (* No recursion *)
            )
         )
      )
   endproc  (* Timethread TestForks *)

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

   process TestLoops[Act10, Act11, Act9, R7, T7]:noexit :=
      T7 ? Cond:Tag;
      (
         (
            Loop_4[Act10, Act11, Act9, R7, T7](Cond) >>
               accept Cond :Tag  in 
            R7; stop
            |||
            TestLoops[Act10, Act11, Act9, R7, T7]  (* Parallel recursion *)
         )
      )

   where
      process Loop_5[Act10, Act11, Act9, R7, T7](Cond :Tag)  : exit(Tag)  :=
         Act10;
         (
            (
               Act11;
               Loop_5[Act10, Act11, Act9, R7, T7](Cond) 
            )
            []
            (
                     exit(Cond)   (* Exit Loop *)
            )
         )
      endproc  (* Loop_5 *)

      process Loop_4[Act10, Act11, Act9, R7, T7](Cond :Tag)  : exit(Tag)  :=
         Act9;
         (
            (
               [Cond eq No]->
               (
                  Loop_5[Act10, Act11, Act9, R7, T7](Cond) >>
                     accept Cond :Tag  in 
                  Loop_4[Act10, Act11, Act9, R7, T7](Cond) 
               )
            )
            []
            (
               [Cond ne No]->
               exit(Cond)   (* Exit Loop *)
            )
         )
      endproc  (* Loop_4 *)

   endproc  (* Timethread TestLoops *)

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

   process TestWP[Act12, Act13, R8, T8]:noexit :=

   hide Delay_8, Sync_Signal_9, Sync_Time_7, TimeOut_6 in

      (
         TimeOut_6;  (* Timeout occured *)
         Sync_Time_7 ! TOut; stop
         []
         T8;  (* Event occured *)
         Sync_Time_7 ! OK; stop
      )
      |[Sync_Time_7]|
      Sync_Time_7 ? TimeT8:Tag;
      (
         Delay_8;  (* Internal delay *)
         Act12;
         (
            Act13; Sync_Signal_9 ! TimeT8 ! Yes; stop  (* Signal occured *)
            []
            Sync_Signal_9 ! TimeT8 ! No; stop  (* No signal occured *)
         )
         |[Sync_Signal_9]|
         Sync_Signal_9 ? TimeT8:Tag ? SigAct13:Tag;
         R8 ! TimeT8 ! SigAct13; stop  (* No recursion *)
      )
   endproc  (* Timethread TestWP *)

endspec (* Map Tests *)