lustrec / test / src / kind_fmcad08 / simulation / tramway_e7_1834_e7_2363.lus @ 0cbf0839
History | View | Annotate | Download (3.4 KB)
1 |
|
---|---|
2 |
node edge(X: bool) returns (edge: bool); |
3 |
let |
4 |
edge = false -> X or not pre(X); |
5 |
tel |
6 |
node switch (init, on, off: bool) returns (value: bool); |
7 |
let |
8 |
value = if on then true |
9 |
else if off then false |
10 |
else init -> pre(value); |
11 |
tel |
12 |
node jafter(X: bool) returns (after: bool); |
13 |
let |
14 |
after = false -> pre(X); |
15 |
tel |
16 |
node once_from_to(A, B, X: bool) returns (OK: bool); |
17 |
var |
18 |
between_A_and_X: bool; |
19 |
let |
20 |
between_A_and_X = switch(false, A, jafter(X)); |
21 |
OK = not (between_A_and_X or B); |
22 |
tel |
23 |
node controller(request_door, warning_start, in_station, door_is_open: bool) |
24 |
returns (open_door, close_door, door_ok: bool); |
25 |
var |
26 |
req_pending: bool; |
27 |
let |
28 |
req_pending = switch(false, request_door and not warning_start, door_is_open); |
29 |
open_door = req_pending and in_station; |
30 |
close_door = warning_start and door_is_open; |
31 |
door_ok = not door_is_open and warning_start; |
32 |
tel |
33 |
node environment(door_is_open, open_door, close_door, in_station, door_ok, warning_start: bool) |
34 |
returns (env_always_ok: bool); |
35 |
var |
36 |
env_ok: bool; |
37 |
door_doesnt_close_if_not_asked: bool; |
38 |
door_doesnt_open_if_not_asked: bool; |
39 |
tramway_doesnt_start_if_not_door_ok: bool; |
40 |
door_initially_closed: bool; |
41 |
initially_not_in_station: bool; |
42 |
warning_start_and_in_station_go_down_simultaneously: bool; |
43 |
warning_start_only_in_station: bool; |
44 |
warning_start_cant_become_true_when_door_is_opening: bool; |
45 |
let |
46 |
env_always_ok = env_ok -> env_ok and pre(env_always_ok); |
47 |
env_ok = door_doesnt_open_if_not_asked and |
48 |
door_doesnt_close_if_not_asked and |
49 |
tramway_doesnt_start_if_not_door_ok and door_initially_closed and |
50 |
initially_not_in_station and |
51 |
warning_start_and_in_station_go_down_simultaneously and |
52 |
warning_start_only_in_station and |
53 |
warning_start_cant_become_true_when_door_is_opening; |
54 |
door_doesnt_close_if_not_asked = edge(door_is_open) => open_door; |
55 |
door_doesnt_open_if_not_asked = edge(not door_is_open) => close_door; |
56 |
tramway_doesnt_start_if_not_door_ok = |
57 |
edge(not in_station) => jafter(door_ok); |
58 |
door_initially_closed = not door_is_open -> true; |
59 |
initially_not_in_station = not in_station -> true; |
60 |
warning_start_and_in_station_go_down_simultaneously = |
61 |
(edge(not in_station) = edge(not warning_start)); |
62 |
warning_start_only_in_station = warning_start => in_station; |
63 |
warning_start_cant_become_true_when_door_is_opening = |
64 |
edge(warning_start) => not open_door; |
65 |
tel |
66 |
node properties(door_is_open, in_station, request_door, warning_start: bool) |
67 |
returns (OK: bool); |
68 |
var |
69 |
door_doesnt_open_out_of_station: bool; |
70 |
door_opens_before_leaving_station: bool; |
71 |
let |
72 |
OK = door_doesnt_open_out_of_station and door_opens_before_leaving_station; |
73 |
door_doesnt_open_out_of_station = door_is_open => in_station; |
74 |
door_opens_before_leaving_station = |
75 |
once_from_to(jafter(request_door and not warning_start), |
76 |
edge(not in_station), |
77 |
jafter(door_is_open)); |
78 |
tel |
79 |
node top(request_door, warning_start, in_station, door_is_open: bool) |
80 |
returns (OK: bool); |
81 |
var |
82 |
env_always_ok, prop_ok: bool; |
83 |
open_door, close_door, door_ok: bool; |
84 |
let |
85 |
OK = env_always_ok => prop_ok; |
86 |
prop_ok = |
87 |
properties(door_is_open, in_station, request_door, warning_start); |
88 |
env_always_ok = |
89 |
environment(door_is_open, open_door, close_door, |
90 |
in_station, door_ok, warning_start); |
91 |
(open_door, close_door, door_ok) = |
92 |
controller(request_door, warning_start, in_station, door_is_open); |
93 |
--%MAIN; |
94 |
--%PROPERTY OK=true; |
95 |
tel |