Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / automata / without_properties / microwave.lus @ 02d89bbb

History | View | Annotate | Download (4.85 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_remaining > 0 restart BRUNNING
10
  
11
  state BRUNNING :
12
--  unless clear && pre mode = 3 restart BSETUP
13
  let
14
    automaton microwave_basic_running
15
    state BRUNNING_ENTRY :
16
    unless door_closed restart BCOOKING
17
    unless not door_closed restart BSUSPENDED
18
    let
19
      -- nothing is computed
20
      mode = 1; -- but this assign is transient and invisible
21
      steps_remaining = pre steps_remaining;
22
    tel
23
    
24
    state BCOOKING :
25
    unless clear || not door_closed restart BSUSPENDED
26
    let
27
      mode = 2;
28
      steps_remaining = pre steps_remaining - 1;
29
    tel
30

    
31
    state BSUSPENDED :
32
    unless start && door_closed restart BCOOKING
33
    let
34
      mode = 3;
35
      steps_remaining = pre steps_remaining;
36
    tel
37
  tel
38
  until steps_remaining <= 0 restart BSETUP
39
  until clear && mode = 3 restart BSETUP
40

    
41
  
42
tel
43

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

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

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

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

    
67
tel
68

    
69
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);
70
var ok: bool; value: int;
71
let
72
  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);
73
  left,  middle,  right = (0, 0, 0) ->
74
    if ok then
75
      (pre middle,  pre right,  value)
76
    else
77
      (pre left,  pre middle,  pre right);
78
    
79
tel
80

    
81
node microwave (kp_start, kp_clear: bool;
82
                kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool;
83
                door_closed:  bool) returns (light_on:  bool);
84
var 
85
  CLEAR_PRESSED, START_PRESSED:  bool; 
86
  steps_remaining, steps_to_cook: int;
87
  left, middle, right: int;
88
mode : int;
89
let
90

    
91
  CLEAR_PRESSED = kp_clear -> (kp_clear and (not (pre kp_clear)));
92
  START_PRESSED = kp_start -> (kp_start and (not (pre kp_start)));
93
  light_on = not door_closed || mode = 2;
94

    
95
  automaton microwave_automaton
96
  state SETUP :
97
  let
98
    mode = 1;
99

    
100
    -- used to setup setps_to_cook
101
    left, middle, right = 
102
      if kp_clear then 
103
        (0, 0, 0) 
104
      else 
105
        keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);
106
  
107
    steps_to_cook = right + middle * 10  + left * 60;
108
  
109
    steps_remaining = steps_to_cook;
110
  
111
  tel until START_PRESSED && steps_remaining > 0 restart RUNNING
112
  
113
  state RUNNING :
114
 -- unless CLEAR_PRESSED && mode = 3 restart SETUP
115
  let
116
    -- we print current remaining steps
117
    left = steps_remaining div 60;
118
    middle = (steps_remaining - (left * 60)) div 10;
119
    right = steps_remaining - (left * 60) - (middle * 10);
120
    steps_to_cook = pre steps_to_cook;
121

    
122
    -- running automaton
123
    automaton microwave_running
124
    state RUNNING_ENTRY :
125
    unless door_closed restart COOKING
126
    unless not door_closed restart SUSPENDED
127
    let
128
      -- nothing is computed
129
      mode = 1; -- but this assign is transient and invisible
130
      steps_remaining = pre steps_remaining;
131
    tel
132
    
133
    state COOKING :
134
    unless CLEAR_PRESSED || not door_closed restart SUSPENDED
135
    let
136
      mode = 2;
137
      steps_remaining = pre steps_remaining - 1;
138
    tel
139

    
140
    state SUSPENDED :			
141
    unless START_PRESSED && door_closed restart COOKING
142
    let
143
      mode = 3;
144
      steps_remaining = pre steps_remaining;
145
    tel
146
  tel
147
  until steps_remaining <= 0 restart SETUP
148
  until CLEAR_PRESSED && mode = 3 restart SETUP
149
tel