(* TMDL-to-LOTOS Compiler, version 0.9. *) specification TestInteractions[Event2, R1, R3, R5, Tr2, Tr4, Tr5]: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 hide Event1, Event3 in ( ( TT4[Event1, Event2, Event3, Tr4] |[Event1, Event3]| ( TT5[Event1, Event3, R5, Tr5] ) ) |[Event2]| TT2[Event2, Tr2] |[Event2]| ( TT1[Event2, R1] ||| TT3[Event2, R3] ) ) where process TT2[Event2, Tr2]:noexit := Tr2; ( Event2; stop (* No recursion *) ) endproc (* Timethread TT2 *) (*********************************************) process TT1[Event2, R1]:noexit := Event2; ( R1; stop (* No recursion *) ) endproc (* Timethread TT1 *) (*********************************************) process TT5[Event1, Event3, R5, Tr5]:noexit := Tr5; ( Event1; Event3; R5; stop (* No recursion *) ) endproc (* Timethread TT5 *) (*********************************************) process TT3[Event2, R3]:noexit := Event2; ( R3; stop (* No recursion *) ) endproc (* Timethread TT3 *) (*********************************************) process TT4[Event1, Event2, Event3, Tr4]:noexit := Tr4; ( Event1; Event3; Event2; stop (* No recursion *) ) endproc (* Timethread TT4 *) endspec (* Map TestInteractions *)