### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / tramway.lus @ 2d37a1e1

 1 ```-- Implementation by Matthieu Moy ``` ```-- Lustre assignment: correction. ``` ```-- Comments starting with [explain] are just reminders of the course, ``` ```-- they should not appear in a real-life program. ``` ``` -- Positive edge detection ``` ```node edge(X: bool) returns (edge: bool); ``` ```let ``` ``` edge = false -> X and not pre(X); ``` ```tel ``` ``` -- becomes true if "on" is true, false if "off" is true. ``` ``` -- Initially, everything happens as if the previous value was ``` ``` -- "init". ``` ``` -- "on" takes precedence over "off" in the case both are true. ``` ```node switch (init, on, off: bool) returns (value: bool); ``` ```let ``` ``` value = if on then true ``` ``` else if off then false ``` ``` else init -> pre(value); ``` ```tel ``` ``` -- Well initialized unit memory. ``` ```node jafter(X: bool) returns (after: bool); ``` ```let ``` ``` after = false -> pre(X); ``` ```tel ``` ``` -- Check whether X occurs once before A and B. ``` ```node once_from_to(A, B, X: bool) returns (OK: bool); ``` ``` -- false if B occurs after A without an X in between. ``` ```var ``` ``` between_A_and_X: bool; ``` ```let ``` ``` -- A | . | T | . | . | . | . | ``` ``` -- X | . | . | . | . | T | . | ``` ``` -- pre(X) | . | . | . | . | . | T | ``` ``` -- between_A_and_X | . | T | T | T | T | . | ``` ``` between_A_and_X = switch(false, A, jafter(X)); ``` ``` OK = not (between_A_and_X and B); ``` ```tel ``` ``` -- The controller itself. ``` ```node controller(request_door, warning_start, in_station, door_is_open: bool) ``` ```returns (open_door, close_door, door_ok: bool); ``` ```var ``` ``` req_pending: bool; ``` ```let ``` ``` req_pending = switch(false, request_door and not warning_start, door_is_open); ``` ``` open_door = req_pending and in_station; ``` ``` close_door = warning_start and door_is_open; ``` ``` door_ok = not door_is_open and warning_start; ``` ```tel ``` ``` -- Assumptions on the environment. ``` ```node environment(door_is_open, open_door, close_door, in_station, door_ok, warning_start: bool) ``` ```returns (env_always_ok: bool); ``` ```var ``` ``` env_ok: bool; ``` ``` door_doesnt_close_if_not_asked: bool; ``` ``` door_doesnt_open_if_not_asked: bool; ``` ``` tramway_doesnt_start_if_not_door_ok: bool; ``` ``` door_initially_closed: bool; ``` ``` initially_not_in_station: bool; ``` ``` warning_start_and_in_station_go_down_simultaneously: bool; ``` ``` warning_start_only_in_station: bool; ``` ``` warning_start_cant_become_true_when_door_is_opening: bool; ``` ```let ``` ``` -- [explain] Environment has always been OK _up to now_ ``` ``` env_always_ok = env_ok -> env_ok and pre(env_always_ok); ``` ``` -- [explain] Environment is OK _Now_ ``` ``` env_ok = door_doesnt_open_if_not_asked and ``` ``` door_doesnt_close_if_not_asked and ``` ``` tramway_doesnt_start_if_not_door_ok and door_initially_closed and ``` ``` initially_not_in_station and ``` ``` warning_start_and_in_station_go_down_simultaneously and ``` ``` warning_start_only_in_station and ``` ``` warning_start_cant_become_true_when_door_is_opening; ``` ``` -- The door is assumed to work properly. ``` ``` door_doesnt_close_if_not_asked = edge(door_is_open) => open_door; ``` ``` door_doesnt_open_if_not_asked = edge(not door_is_open) => close_door; ``` ``` -- The tramway is assumed to work property too: it won't start ``` ``` -- unless door_ok is true. ``` ``` -- (edge(...) becomes true at the time the tramway has already left, ``` ``` -- so door_ok must have. ``` ``` tramway_doesnt_start_if_not_door_ok = ``` ``` edge(not in_station) => jafter(door_ok); ``` ``` -- unrealistic assumption: the tramway is initially running, with ``` ``` -- doors closed. ``` ``` door_initially_closed = not door_is_open -> true; ``` ``` initially_not_in_station = not in_station -> true; ``` ``` -- Tramway stops warning_start when leaving station, and starts it ``` ``` -- only when in station. ``` ``` warning_start_and_in_station_go_down_simultaneously = ``` ``` (edge(not in_station) = edge(not warning_start)); ``` ``` warning_start_only_in_station = warning_start => in_station; ``` ``` -- warning_start is supposed to be raised when the tramway can ``` ``` -- prepare to leave. We assume it's not the case when the door is ``` ``` -- being opened. ``` ``` warning_start_cant_become_true_when_door_is_opening = ``` ``` edge(warning_start) => not open_door; ``` ```tel ``` ``` -- properties to verify. ``` ```node properties(door_is_open, in_station, request_door, warning_start: bool) ``` ```returns (OK: bool); ``` ```var ``` ``` door_doesnt_open_out_of_station: bool; ``` ``` door_opens_before_leaving_station: bool; ``` ```let ``` ``` OK = door_doesnt_open_out_of_station and door_opens_before_leaving_station; ``` ``` -- Basic property to check: the door never opens out of station. ``` ``` door_doesnt_open_out_of_station = door_is_open => in_station; ``` ``` -- Slightly more elaborated: the door opens once between the time ``` ``` -- the request is issued and the tramway leaving the station. ``` ``` door_opens_before_leaving_station = ``` ``` once_from_to(jafter(request_door and not warning_start), ``` ``` edge(not in_station), ``` ``` jafter(door_is_open)); ``` ``` -- Many other are possible ... ``` ```tel ``` ``` -- [explain] A node for verification with a model-checker like lesar ``` ``` -- [explain] is always similar to this: the program, the environment ``` ``` -- [explain] and the property altogether. ``` ``` -- [explain] +------------+ ``` ``` -- [explain] +---------------+-->| environment|--> ``` ``` -- [explain] | +---------+ | +------------+ ``` ``` -- [explain]--+->| program +--+ ``` ``` -- [explain] | +---------+ | +------------+ ``` ``` -- [explain] +---------------+-->| property |--> ``` ``` -- [explain] +------------+ ``` ```node top(request_door, warning_start, in_station, door_is_open: bool) ``` ```returns (OK: bool); ``` ```--@ contract guarantees OK; ``` ```var ``` ``` env_always_ok, prop_ok: bool; ``` ``` open_door, close_door, door_ok: bool; ``` ```let ``` ``` -- [explain] Thing to check: ``` ``` -- [explain] "If the environment has always been OK up to now, then ``` ``` -- [explain] the property mustn't have been violated" ``` ``` OK = env_always_ok => prop_ok; ``` ``` -- [explain] the property ``` ``` prop_ok = ``` ``` properties(door_is_open, in_station, request_door, warning_start); ``` ``` -- [explain] The environment: assumptions under which the program ``` ``` -- [explain] should work properly. ``` ``` env_always_ok = ``` ``` environment(door_is_open, open_door, close_door, ``` ``` in_station, door_ok, warning_start); ``` ``` -- [explain] The program itself. ``` ``` (open_door, close_door, door_ok) = ``` ``` controller(request_door, warning_start, in_station, door_is_open); ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```