CristalCaveGem » LustreC » Lustrec-Tests

node microwave_basic (start, clear: bool; door_closed: bool; steps_to_cook: int) returns (mode: int);

var steps_remaining: int;

let

  automaton microwave_basic_automaton

  state BSETUP :

  let

    mode = 1;

    steps_remaining = steps_to_cook;

  tel until start && steps_remaining > 0 restart BRUNNING

  state BRUNNING :

--  unless clear && pre mode = 3 restart BSETUP

  let

    automaton microwave_basic_running

    state BRUNNING_ENTRY :

    unless door_closed restart BCOOKING

    unless not door_closed restart BSUSPENDED

    let

      -- nothing is computed

      mode = 1; -- but this assign is transient and invisible

      steps_remaining = pre steps_remaining;

    tel

    state BCOOKING :

    unless clear || not door_closed restart BSUSPENDED

    let

      mode = 2;

      steps_remaining = pre steps_remaining - 1;

    tel

    state BSUSPENDED :

    unless start && door_closed restart BCOOKING

    let

      mode = 3;

      steps_remaining = pre steps_remaining;

    tel

  tel

  until steps_remaining <= 0 restart BSETUP

  until clear && mode = 3 restart BSETUP

tel

node push_n_relaxed (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool) returns (ok:  bool; value:  int);

var only_one_pushed,  none_pushed:  bool;

let

  only_one_pushed = 

    (kp_0 && not (kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_1 && not (kp_0 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_2 && not (kp_0 || kp_1 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_3 && not (kp_0 || kp_1 || kp_2 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_4 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_5 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_6 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_7 || kp_8 || kp_9)) ||

    (kp_7 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_8 || kp_9)) ||

    (kp_8 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_9)) ||

    (kp_9 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 ));

  none_pushed =  not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9);

  ok = only_one_pushed && (true -> pre none_pushed); 

  value = if kp_0 then 0 else if kp_1 then 1 else if kp_2 then 2 else if kp_3

          then 3 else if kp_4 then 4 else if kp_5 then 5 else if kp_6 then 6 else

          if kp_7 then 7 else if kp_8 then 8 else if kp_9 then 9 else 10;

tel

node keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool) returns (left,  middle,  right:  int);

var ok: bool; value: int;

let

  ok,  value = push_n_relaxed (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);

  left,  middle,  right = (0, 0, 0) ->

    if ok then

      (pre middle,  pre right,  value)

    else

      (pre left,  pre middle,  pre right);

tel

node microwave (kp_start, kp_clear: bool;

                kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool;

                door_closed:  bool) returns (light_on:  bool);

var 

  CLEAR_PRESSED, START_PRESSED:  bool; 

  steps_remaining, steps_to_cook: int;

  left, middle, right: int;

mode : int;

let

  CLEAR_PRESSED = kp_clear -> (kp_clear and (not (pre kp_clear)));

  START_PRESSED = kp_start -> (kp_start and (not (pre kp_start)));

  light_on = not door_closed || mode = 2;

  automaton microwave_automaton

  state SETUP :

  let

    mode = 1;

    -- used to setup setps_to_cook

    left, middle, right = 

      if kp_clear then 

        (0, 0, 0) 

      else 

        keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);

    steps_to_cook = right + middle * 10  + left * 60;

    steps_remaining = steps_to_cook;

  tel until START_PRESSED && steps_remaining > 0 restart RUNNING

  state RUNNING :

 -- unless CLEAR_PRESSED && mode = 3 restart SETUP

  let

    -- we print current remaining steps

    left = steps_remaining div 60;

    middle = (steps_remaining - (left * 60)) div 10;

    right = steps_remaining - (left * 60) - (middle * 10);

    steps_to_cook = pre steps_to_cook;

    -- running automaton

    automaton microwave_running

    state RUNNING_ENTRY :

    unless door_closed restart COOKING

    unless not door_closed restart SUSPENDED

    let

      -- nothing is computed

      mode = 1; -- but this assign is transient and invisible

      steps_remaining = pre steps_remaining;

    tel

    state COOKING :

    unless CLEAR_PRESSED || not door_closed restart SUSPENDED

    let

      mode = 2;

      steps_remaining = pre steps_remaining - 1;

    tel

    state SUSPENDED :			

    unless START_PRESSED && door_closed restart COOKING

    let

      mode = 3;

      steps_remaining = pre steps_remaining;

    tel

  tel

  until steps_remaining <= 0 restart SETUP

  until CLEAR_PRESSED && mode = 3 restart SETUP

tel