Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / automata / microwave.lus @ 006b37e0

History | View | Annotate | Download (4.51 KB)

1
node microwave_basic (start, clear: bool; door_closed: bool; steps_to_cook: int) returns (mode: int);
2
var steps_remaining: int;
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

    
89
  automaton microwave_automaton
90
  state SETUP :
91
  var setup_left, setup_middle, setup_right: int;
92
  let
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
  
104
    steps_remaining = steps_to_cook;
105
  
106
  tel until START_PRESSED && steps_to_remaining > 0 restart RUNNING
107
  
108
  state RUNNING :
109
  var left, middle, right: int; 
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
117
    automaton microwave_running
118
    state RUNNING_ENTRY :
119
    unless door_closed restart COOKING
120
    unless not door_closed restart SUSPENDED
121
    let
122
      -- nothing is computed
123
      mode = 1; -- but this assign is transient and invisible
124
    tel
125
    
126
    state COOKING :
127
    unless CLEAR_PRESSED || not door_closed restart SUSPENDED
128
    let
129
      mode = 2;
130
      steps_remaining = pre steps_remaining - 1;
131
    tel
132

    
133
    state SUSPENDED :
134
    unless start && door_closed restart COOKING
135
    unless CLEAR_PRESSED restart SETUP
136
    let
137
      mode = 3;
138
    tel
139
  tel
140
  until steps_remaining <= 0 restart SETUP
141
tel