lustrec / test / src / kind_fmcad08 / simulation / tramway_e7_3304.lus @ 0cbf0839
History | View | Annotate | Download (3.41 KB)
1 | 0cbf0839 | ploc | |
---|---|---|---|
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 and 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 |