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