Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / tramway_e7_1834_e8_3192.lus @ 22fe1c93

History | View | Annotate | Download (3.41 KB)

1

    
2
node edge(X: bool) returns (edge: bool);
3
let
4
  edge = false -> X and 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