Project

General

Profile

Revision 006b37e0 tests/automata/microwave.lus

View differences:

tests/automata/microwave.lus
1 1
node microwave_basic (start, clear: bool; door_closed: bool; steps_to_cook: int) returns (mode: int);
2 2
var steps_remaining: int;
3 3
let
4
  automaton microwave_basic_automaton
5
  state BSETUP :
6
  let
7
    mode = 1;
8
    steps_remaining = steps_to_cook;
9
  tel until start && steps_to_remaining > 0 restart RUNNING
10
  
11
  state BRUNNING :
12
  unless clear && mode = 3 restart SETUP
13
  let
14
    automaton microwave_basic_running
15
    state BRUNNING_ENTRY :
16
    unless door_closed restart COOKING
17
    unless not door_closed restart SUSPENDED
18
    let
19
      -- nothing is computed
20
      mode = 1; -- but this assign is transient and invisible
21
    tel
22
    
23
    state BCOOKING :
24
    unless clear || not door_closed restart SUSPENDED
25
    let
26
      mode = 2;
27
      steps_remaining = pre steps_remaining - 1;
28
    tel
29

  
30
    state BSUSPENDED :
31
    unless start && door_closed restart COOKING
32
    let
33
      mode = 3;
34
    tel
35
  tel
36
  until steps_remaining <= 0 restart SETUP
37

  
38
  
39
tel
40

  
41
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);
42
var only_one_pushed,  none_pushed:  bool;
43
let
44
  only_one_pushed = 
45
    (kp_0 && not (kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
46
    (kp_1 && not (kp_0 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
47
    (kp_2 && not (kp_0 || kp_1 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
48
    (kp_3 && not (kp_0 || kp_1 || kp_2 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
49
    (kp_4 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
50
    (kp_5 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_6 || kp_7 || kp_8 || kp_9)) ||
51
    (kp_6 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_7 || kp_8 || kp_9)) ||
52
    (kp_7 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_8 || kp_9)) ||
53
    (kp_8 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_9)) ||
54
    (kp_9 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 ));
55

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

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

  
60
  value = if kp_0 then 0 else if kp_1 then 1 else if kp_2 then 2 else if kp_3
61
          then 3 else if kp_4 then 4 else if kp_5 then 5 else if kp_6 then 6 else
62
          if kp_7 then 7 else if kp_8 then 8 else if kp_9 then 9 else 10;
63

  
64
tel
65

  
66
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);
67
let
68
  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);
69
  left,  middle,  right = (0, 0, 0) ->
70
    if ok then
71
      (pre middle,  pre right,  value)
72
    else
73
      (pre left,  pre middle,  pre right);
74
    
75
tel
76

  
77
node microwave (kp_start, kp_clear: bool;
78
                kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool;
79
                door_closed:  bool) returns (OK:  bool);
80
var 
81
  CLEAR_PRESSED, START_PRESSED:  bool; 
82
  steps_remaining, steps_to_cook: int;
83
let
84

  
85
  CLEAR_PRESSED = kp_clear -> (kp_clear and (not (pre kp_clear)));
86
  START_PRESSED = kp_start -> (kp_start and (not (pre kp_start)));
87
  
88

  
4 89
  automaton microwave_automaton
5 90
  state SETUP :
91
  var setup_left, setup_middle, setup_right: int;
6 92
  let
7 93
    mode = 1;
94

  
95
    -- used to setup setps_to_cook
96
    left, middle, right = 
97
      if kp_clear then 
98
        (0, 0, 0) 
99
      else 
100
        keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);
101
  
102
    steps_to_cook = setup_right + setup_middle * 10  + setup_left * 60;
103
  
8 104
    steps_remaining = steps_to_cook;
9
  tel until start && steps_to_remaining > 0 restart RUNNING
105
  
106
  tel until START_PRESSED && steps_to_remaining > 0 restart RUNNING
10 107
  
11 108
  state RUNNING :
109
  var left, middle, right: int; 
12 110
  let
111
    -- we print current remaining steps
112
    left = steps_remaining div 60;
113
    middle = (steps_remaining - (left * 60)) div 10;
114
    right = steps_remaining - (left * 60) - (middle * 10);
115

  
116
    -- running automaton
13 117
    automaton microwave_running
14 118
    state RUNNING_ENTRY :
15 119
    unless door_closed restart COOKING
......
20 124
    tel
21 125
    
22 126
    state COOKING :
23
    unless clear || not door_closed restart SUSPENDED
127
    unless CLEAR_PRESSED || not door_closed restart SUSPENDED
24 128
    let
25 129
      mode = 2;
26 130
      steps_remaining = pre steps_remaining - 1;
......
28 132

  
29 133
    state SUSPENDED :
30 134
    unless start && door_closed restart COOKING
31
    unless clear restart SETUP
135
    unless CLEAR_PRESSED restart SETUP
32 136
    let
33 137
      mode = 3;
34 138
    tel
35 139
  tel
36 140
  until steps_remaining <= 0 restart SETUP
37
  
38 141
tel

Also available in: Unified diff