tests.lot


LOTOS Specification

(* 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 *)


List of Processes


List of Types


HTML vertion by lot2html (ver. 0.1), Fri Sep 6 11:59:12 1996