lustrec / test / src / kind_fmcad08 / simulation / ums_e8_1032.lus @ 0cbf0839
History | View | Annotate | Download (2.44 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
node edge(X: bool) returns(Y: bool); |
7 |
let |
8 |
Y = X -> X and not pre(X); |
9 |
tel |
10 |
node after(A: bool) returns(afterA: bool); |
11 |
let |
12 |
afterA = false -> pre(A and afterA); |
13 |
tel |
14 |
node always_since(B, A: bool) returns(alwaysBsinceA: bool); |
15 |
let |
16 |
alwaysBsinceA = if A then B else if after(A) then |
17 |
B and pre(alwaysBsinceA) else true; |
18 |
tel |
19 |
node once_since(C, A: bool) returns(onceCsinceA: bool); |
20 |
let |
21 |
onceCsinceA = if A then C else if after(A) then |
22 |
C or pre(onceCsinceA) else true; |
23 |
tel |
24 |
node implies(A, B: bool) returns(AimpliesB: bool); |
25 |
let |
26 |
AimpliesB = not A or B; |
27 |
tel |
28 |
node always_from_to(B, A, C: bool) returns(X: bool); |
29 |
let |
30 |
X = implies(after(A), always_since(B, A) or once_since(C, A)); |
31 |
tel |
32 |
node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool) |
33 |
returns(grant_access, grant_exit, do_AB, do_BC: bool); |
34 |
var |
35 |
empty_section, only_on_B: bool; |
36 |
let |
37 |
grant_access = empty_section and ack_AB; |
38 |
grant_exit = only_on_B and ack_BC; |
39 |
do_AB = not ack_AB and empty_section; |
40 |
do_BC = not ack_BC and only_on_B; |
41 |
empty_section = not(on_A or on_B or on_C); |
42 |
only_on_B = on_B and not(on_A or on_C); |
43 |
tel |
44 |
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool) |
45 |
returns(OK: bool); |
46 |
var |
47 |
grant_access, grant_exit: bool; |
48 |
do_AB, do_BC: bool; |
49 |
no_collision, exclusive_req: bool; |
50 |
no_derail_AB, no_derail_BC: bool; |
51 |
empty_section, only_on_B: bool; |
52 |
env : bool; |
53 |
let |
54 |
empty_section = not(on_A or on_B or on_C); |
55 |
only_on_B = on_B and not(on_A or on_C); |
56 |
(grant_access, grant_exit, do_AB, do_BC) = |
57 |
UMS(on_A, on_B, on_C, ack_AB, ack_BC); |
58 |
env = Sofar( not(ack_AB and ack_BC) and |
59 |
always_from_to(ack_AB, ack_AB, do_BC) and |
60 |
always_from_to(ack_BC, ack_BC, do_AB) and |
61 |
(empty_section -> true) and |
62 |
(true -> implies(edge(not empty_section), pre grant_access)) and |
63 |
(true -> implies(edge(on_C), pre grant_exit)) and |
64 |
implies(edge(not on_A), on_B) and |
65 |
implies(edge(not on_B), on_A or on_C) ); |
66 |
no_collision = implies(grant_access, empty_section); |
67 |
exclusive_req = not(do_AB and do_BC); |
68 |
no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B); |
69 |
no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section); |
70 |
OK = env => no_collision and exclusive_req and |
71 |
no_derail_AB and no_derail_BC; |
72 |
--%MAIN; |
73 |
--%PROPERTY OK=true; |
74 |
tel |