Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (5.96 KB)

1
-- Implementation by Matthieu Moy
2

    
3
-- Lustre assignment: correction.
4
-- Comments starting with [explain] are just reminders of the course,
5
-- they should not appear in a real-life program.
6

    
7
  -- Positive edge detection
8
node edge(X: bool) returns (edge: bool);
9
let
10
  edge = false -> X and not pre(X);
11
tel
12

    
13
  -- becomes true if "on" is true, false if "off" is true.
14
  -- Initially, everything happens as if the previous value was
15
  -- "init".
16
  -- "on" takes precedence over "off" in the case both are true.
17
node switch (init, on, off: bool) returns (value: bool);
18
let
19
  value = if on then true
20
          else if off then false
21
               else init -> pre(value);
22
tel
23

    
24
  -- Well initialized unit memory.
25
node jafter(X: bool) returns (after: bool);
26
let
27
  after = false -> pre(X);
28
tel
29

    
30
  -- Check whether X occurs once before A and B.
31
node once_from_to(A, B, X: bool) returns (OK: bool);
32
  -- false if B occurs after A without an X in between.
33
var
34
  between_A_and_X: bool;
35
let
36
  -- A               | . | T | . | . | . | . |
37
  -- X               | . | . | . | . | T | . |
38
  -- pre(X)          | . | . | . | . | . | T |
39
  -- between_A_and_X | . | T | T | T | T | . |
40
  between_A_and_X = switch(false, A, jafter(X));
41
  OK = not (between_A_and_X and B);
42
tel
43

    
44
  -- The controller itself.
45
node controller(request_door, warning_start, in_station, door_is_open: bool)
46
returns (open_door, close_door, door_ok: bool);
47
var
48
  req_pending: bool;
49
let
50
  req_pending = switch(false, request_door and not warning_start, door_is_open);
51
  open_door = req_pending and in_station;
52
  close_door = warning_start and door_is_open;
53
  door_ok = not door_is_open and warning_start;
54
tel
55

    
56
  -- Assumptions on the environment.
57
node environment(door_is_open, open_door, close_door, in_station, door_ok, warning_start: bool)
58
returns (env_always_ok: bool);
59
var
60
  env_ok: bool;
61
  door_doesnt_close_if_not_asked: bool;
62
  door_doesnt_open_if_not_asked: bool;
63
  tramway_doesnt_start_if_not_door_ok: bool;
64
  door_initially_closed: bool;
65
  initially_not_in_station: bool;
66
  warning_start_and_in_station_go_down_simultaneously: bool;
67
  warning_start_only_in_station: bool;
68
  warning_start_cant_become_true_when_door_is_opening: bool;
69
let
70
  -- [explain] Environment has always been OK _up to now_
71
  env_always_ok = env_ok -> env_ok and pre(env_always_ok);
72

    
73
  -- [explain] Environment is OK _Now_
74
  env_ok = door_doesnt_open_if_not_asked and
75
    door_doesnt_close_if_not_asked and
76
      tramway_doesnt_start_if_not_door_ok and door_initially_closed and
77
        initially_not_in_station and
78
          warning_start_and_in_station_go_down_simultaneously and
79
            warning_start_only_in_station and
80
              warning_start_cant_become_true_when_door_is_opening;
81

    
82
  -- The door is assumed to work properly.
83
  door_doesnt_close_if_not_asked = edge(door_is_open) => open_door;
84
  door_doesnt_open_if_not_asked = edge(not door_is_open) => close_door;
85

    
86
  -- The tramway is assumed to work property too: it won't start
87
  -- unless door_ok is true.
88
  -- (edge(...) becomes true at the time the tramway has already left,
89
  -- so door_ok must have.
90
  tramway_doesnt_start_if_not_door_ok =
91
    edge(not in_station) => jafter(door_ok);
92

    
93
  -- unrealistic assumption: the tramway is initially running, with
94
  -- doors closed.
95
  door_initially_closed = not door_is_open -> true;
96
  initially_not_in_station = not in_station -> true;
97

    
98
  -- Tramway stops warning_start when leaving station, and starts it
99
  -- only when in station.
100
  warning_start_and_in_station_go_down_simultaneously =
101
    (edge(not in_station) = edge(not warning_start));
102
  warning_start_only_in_station = warning_start => in_station;
103

    
104
  -- warning_start is supposed to be raised when the tramway can
105
  -- prepare to leave. We assume it's not the case when the door is
106
  -- being opened.
107
  warning_start_cant_become_true_when_door_is_opening =
108
    edge(warning_start) => not open_door;
109
tel
110

    
111
  -- properties to verify.
112
node properties(door_is_open, in_station, request_door, warning_start: bool)
113
returns (OK: bool);
114
var
115
  door_doesnt_open_out_of_station: bool;
116
  door_opens_before_leaving_station: bool;
117
let
118
  OK = door_doesnt_open_out_of_station and door_opens_before_leaving_station;
119

    
120
  -- Basic property to check: the door never opens out of station.
121
  door_doesnt_open_out_of_station = door_is_open => in_station;
122

    
123
  -- Slightly more elaborated: the door opens once between the time
124
  -- the request is issued and the tramway leaving the station.
125
  door_opens_before_leaving_station =
126
    once_from_to(jafter(request_door and not warning_start),
127
                 edge(not in_station),
128
                 jafter(door_is_open));
129

    
130
  -- Many other are possible ...
131
tel
132

    
133
  -- [explain] A node for verification with a model-checker like lesar
134
  -- [explain] is always similar to this: the program, the environment
135
  -- [explain] and the property altogether.
136
  -- [explain]                      +------------+
137
  -- [explain]  +---------------+-->| environment|-->
138
  -- [explain]  |  +---------+  |   +------------+
139
  -- [explain]--+->| program +--+
140
  -- [explain]  |  +---------+  |   +------------+
141
  -- [explain]  +---------------+-->| property   |-->
142
  -- [explain]                      +------------+
143
node top(request_door, warning_start, in_station, door_is_open: bool)
144
returns (OK: bool);
145
var
146
  env_always_ok, prop_ok: bool;
147
  open_door, close_door, door_ok: bool;
148
let
149
  -- [explain] Thing to check:
150
  -- [explain] "If the environment has always been OK up to now, then
151
  -- [explain] the property mustn't have been violated"
152
  OK = env_always_ok => prop_ok;
153

    
154
  -- [explain] the property
155
  prop_ok = 
156
    properties(door_is_open, in_station, request_door, warning_start);
157

    
158
  -- [explain] The environment: assumptions under which the program
159
  -- [explain] should work properly.
160
  env_always_ok =
161
    environment(door_is_open, open_door, close_door,
162
                in_station, door_ok, warning_start);
163

    
164
  -- [explain] The program itself.
165
  (open_door, close_door, door_ok) =
166
    controller(request_door, warning_start, in_station, door_is_open);
167
  --%MAIN;
168
  --%PROPERTY OK=true;
169
tel