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