CristalCaveGem » LustreC » Lustrec-Tests

node edge(X: bool) returns (edge: bool);

let

  edge = false -> X or not pre(X);

tel

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

node jafter(X: bool) returns (after: bool);

let

  after = false -> pre(X);

tel

node once_from_to(A, B, X: bool) returns (OK: bool);

var

  between_A_and_X: bool;

let

  between_A_and_X = switch(false, A, jafter(X));

  OK = not (between_A_and_X and B);

tel

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

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

  env_always_ok = env_ok -> env_ok and pre(env_always_ok);

  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;

  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;

  tramway_doesnt_start_if_not_door_ok =

    edge(not in_station) => jafter(door_ok);

  door_initially_closed = not door_is_open -> true;

  initially_not_in_station = not in_station -> true;

  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_cant_become_true_when_door_is_opening =

    edge(warning_start) => not open_door;

tel

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;

  door_doesnt_open_out_of_station = door_is_open => in_station;

  door_opens_before_leaving_station =

    once_from_to(jafter(request_door and not warning_start),

                 edge(not in_station),

                 jafter(door_is_open));

tel

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

  OK = env_always_ok => prop_ok;

  prop_ok = 

    properties(door_is_open, in_station, request_door, warning_start);

  env_always_ok =

    environment(door_is_open, open_door, close_door,

                in_station, door_ok, warning_start);

  (open_door, close_door, door_ok) =

    controller(request_door, warning_start, in_station, door_is_open);

  --%MAIN;

  --%PROPERTY  OK=true;

tel