Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / TIMEOUT / microwave37.lus @ b8dc00eb

History | View | Annotate | Download (41.8 KB)

1
--@ ensures OK;
2
node top(KP_START: bool; 
3
      KP_CLEAR: bool; 
4
      KP_0: bool; 
5
      KP_1: bool; 
6
      KP_2: bool; 
7
      KP_3: bool; 
8
      KP_4: bool; 
9
      KP_5: bool; 
10
      KP_6: bool; 
11
      KP_7: bool; 
12
      KP_8: bool; 
13
      KP_9: bool; 
14
      DOOR_CLOSED: bool
15
) returns (OK:bool);
16

    
17
   
18
var
19
   LEFT_DIGIT: int; 
20
      SETUP: bool; 
21
      COOKING: bool; 
22
      SUSPENDED: bool; 
23
      START_PRESSED: bool; 
24
      CLEAR_PRESSED: bool; 
25
      MIDDLE_DIGIT: int; 
26
      RIGHT_DIGIT: int; 
27
      enable: bool; 
28
      STEPS_TO_COOK: int;
29
      
30
   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock: bool; 
31
   KP_01: bool; 
32
   KP_11: bool; 
33
   KP_21: bool; 
34
   KP_31: bool; 
35
   KP_41: bool; 
36
   KP_51: bool; 
37
   KP_61: bool; 
38
   KP_71: bool; 
39
   KP_81: bool; 
40
   KP_91: bool; 
41
   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step: bool; 
42
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY: int; 
43
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY: int; 
44
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY: int; 
45
   rlt__Arrow5: int; 
46
   rlt__Arrow4: int; 
47
   rlt__Arrow3: int; 
48
   rlt__Arrow2: int; 
49
   rlt__Arrow1: int; 
50
   rlt__Arrow: int; 
51
   chart_microwave_mode_logic_start: int; 
52
   chart_microwave_mode_logic_clear_off: int; 
53
   chart_microwave_mode_logic_door_closed: int; 
54
   chart_microwave_mode_logic____wakeup___: bool; 
55
   rlt_eval_microwave_mode_logic_ON_rlt_fired_1: bool; 
56
   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root: int; 
57
   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root: int; 
58
   rlt_eval_microwave_mode_logic_ON_rlt_fired_2: bool; 
59
   rlt_eval_microwave_mode_logic_ON_rlt_complete_1: bool; 
60
   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root: int; 
61
   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode: int; 
62
   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root: int; 
63
   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode: int; 
64
   rlt_eval_microwave_mode_logic_ON_rlt_fired_4: bool; 
65
   rlt_eval_microwave_mode_logic_ON_rlt_complete_2: bool; 
66
   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root: int; 
67
   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining: int; 
68
   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root: int; 
69
   rlt_eval_microwave_mode_logic_ON_rlt_fired_5: bool; 
70
   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode: int; 
71
   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root: int; 
72
   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root: int; 
73
   rlt_eval_microwave_mode_logic_ON_rlt_fired_6: bool; 
74
   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root: int; 
75
   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode: int; 
76
   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root: int; 
77
   rlt_enter_microwave_mode_logic_ON_rlt_fired_0: bool; 
78
   rlt_enter_microwave_mode_logic_ON_rlt_fired_1: bool; 
79
   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root: int; 
80
   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode: int; 
81
   rlt_enter_microwave_mode_logic_ON_rlt_fired_2: bool; 
82
   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root: int; 
83
   rlt_eval_microwave_mode_logic_rlt_fired_0: bool; 
84
   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining: int; 
85
   rlt_eval_microwave_mode_logic_rlt_fired_1: bool; 
86
   rlt_eval_microwave_mode_logic_rlt_state_2_states___root: int; 
87
   rlt_eval_microwave_mode_logic_rlt_state_3_states___root: int; 
88
   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode: int; 
89
   rlt_enter_microwave_mode_logic_rlt_state_2_states___root: int; 
90
   chart_microwave_mode_logic_rlt_evtInitStep: bool; 
91
   chart_microwave_mode_logic_begin_state_states___root: int; 
92
   chart_microwave_mode_logic_begin_state_outports_mode: int; 
93
   chart_microwave_mode_logic_begin_state_outports_steps_remaining: int; 
94
   chart_microwave_mode_logic_final_state_states___root: int; 
95
   chart_microwave_mode_logic_mode: int; 
96
   chart_microwave_mode_logic_steps_remaining: int; 
97
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT: int; 
98
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT: int; 
99
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER: int; 
100
   microwave_microwave_mode_logic_mode: int; 
101
   MWI_FcnMaxI_In16: int; 
102
   MWI_FcnMaxI_In15: int; 
103
   MWI_FcnMaxI_In13: int; 
104
   MWI_FcnMaxI_In12: int; 
105
   MWI_FcnMaxI_In11: int; 
106
   MWI_FcnMaxI_In1: int; 
107
   p35: bool; 
108
   p36: bool; 
109
   p37: bool; 
110
let 
111
   rlt__Arrow5 = (639 -> 
112
      (if (not (not SETUP))
113
         then 
114
               (if (MWI_FcnMaxI_In13 > 0)
115
                  then MWI_FcnMaxI_In13
116
                  else 0)
117
         else 639));
118

    
119
   rlt__Arrow4 = (639 -> 
120
      (if (not SUSPENDED)
121
         then 
122
               (if (MWI_FcnMaxI_In12 > 0)
123
                  then MWI_FcnMaxI_In12
124
                  else 0)
125
         else 639));
126

    
127
   rlt__Arrow3 = (639 -> 
128
      (if (not (not COOKING))
129
         then 
130
               (if (MWI_FcnMaxI_In16 > 0)
131
                  then MWI_FcnMaxI_In16
132
                  else 0)
133
         else 639));
134

    
135
   rlt__Arrow2 = (639 -> 
136
      (if (not (not SUSPENDED))
137
         then 
138
               (if (MWI_FcnMaxI_In15 > 0)
139
                  then MWI_FcnMaxI_In15
140
                  else 0)
141
         else 639));
142

    
143
   rlt__Arrow1 = (639 -> 
144
      (if (not COOKING)
145
         then 
146
               (if (MWI_FcnMaxI_In11 > 0)
147
                  then MWI_FcnMaxI_In11
148
                  else 0)
149
         else 639));
150

    
151
   rlt__Arrow = (639 -> 
152
      (if (not SETUP)
153
         then 
154
               (if (MWI_FcnMaxI_In1 > 0)
155
                  then MWI_FcnMaxI_In1
156
                  else 0)
157
         else 639));
158

    
159

    
160

    
161
   p35 = (true -> ((not (enable and 
162
      (not KP_CLEAR))) or 
163
      ((not ((KP_8 and 
164
      (not (pre KP_8))) and 
165
      ((not (KP_7 and 
166
      (not (pre KP_7)))) and 
167
      ((not (KP_6 and 
168
      (not (pre KP_6)))) and 
169
      ((not (KP_5 and 
170
      (not (pre KP_5)))) and 
171
      ((not (KP_4 and 
172
      (not (pre KP_4)))) and 
173
      ((not (KP_3 and 
174
      (not (pre KP_3)))) and 
175
      ((not (KP_2 and 
176
      (not (pre KP_2)))) and 
177
      ((not (KP_1 and 
178
      (not (pre KP_1)))) and 
179
      (not (KP_0 and 
180
      (not (pre KP_0))))))))))))) or 
181
      (RIGHT_DIGIT = 8))));
182

    
183

    
184
   MIDDLE_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT;
185

    
186
   RIGHT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER;
187

    
188

    
189

    
190
   p36 = (true -> ((not (enable and 
191
      (not KP_CLEAR))) or 
192
      ((not ((KP_9 and 
193
      (not (pre KP_9))) and 
194
      ((not (KP_8 and 
195
      (not (pre KP_8)))) and 
196
      ((not (KP_7 and 
197
      (not (pre KP_7)))) and 
198
      ((not (KP_6 and 
199
      (not (pre KP_6)))) and 
200
      ((not (KP_5 and 
201
      (not (pre KP_5)))) and 
202
      ((not (KP_4 and 
203
      (not (pre KP_4)))) and 
204
      ((not (KP_3 and 
205
      (not (pre KP_3)))) and 
206
      ((not (KP_2 and 
207
      (not (pre KP_2)))) and 
208
      ((not (KP_1 and 
209
      (not (pre KP_1)))) and 
210
      (not (KP_0 and 
211
      (not (pre KP_0)))))))))))))) or 
212
      (RIGHT_DIGIT = 9))));
213

    
214
   MWI_FcnMaxI_In1 = ((pre rlt__Arrow) - 1);
215

    
216
   CLEAR_PRESSED = (KP_CLEAR -> (KP_CLEAR and 
217
      (not (pre KP_CLEAR))));
218

    
219
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT = ((chart_microwave_mode_logic_steps_remaining div 1) div 60);
220

    
221
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) - ((((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10) * 10));
222

    
223
   SUSPENDED = 
224
      (if (3 = microwave_microwave_mode_logic_mode)
225
         then true
226
         else false);
227

    
228

    
229
   p37 = (true -> ((not (enable and 
230
      (not KP_CLEAR))) or 
231
      (((((((((((KP_1 and 
232
      (not (pre KP_1))) or 
233
      (KP_2 and 
234
      (not (pre KP_2)))) or 
235
      (KP_3 and 
236
      (not (pre KP_3)))) or 
237
      (KP_4 and 
238
      (not (pre KP_4)))) or 
239
      (KP_5 and 
240
      (not (pre KP_5)))) or 
241
      (KP_6 and 
242
      (not (pre KP_6)))) or 
243
      (KP_7 and 
244
      (not (pre KP_7)))) or 
245
      (KP_8 and 
246
      (not (pre KP_8)))) or 
247
      (KP_9 and 
248
      (not (pre KP_9)))) or 
249
      (KP_0 and 
250
      (not (pre KP_0)))) or 
251
      (RIGHT_DIGIT = (pre RIGHT_DIGIT)))));
252

    
253
   MWI_FcnMaxI_In11 = ((pre rlt__Arrow1) - 1);
254

    
255
   MWI_FcnMaxI_In15 = ((pre rlt__Arrow2) - 1);
256

    
257

    
258

    
259

    
260
   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10);
261

    
262
   MWI_FcnMaxI_In16 = ((pre rlt__Arrow3) - 1);
263

    
264

    
265
   MWI_FcnMaxI_In12 = ((pre rlt__Arrow4) - 1);
266

    
267

    
268

    
269
   COOKING = 
270
      (if (2 = microwave_microwave_mode_logic_mode)
271
         then true
272
         else false);
273

    
274
   LEFT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT;
275

    
276
   START_PRESSED = (KP_START -> (KP_START and 
277
      (not (pre KP_START))));
278

    
279
   chart_microwave_mode_logic_start = 
280
      (if (START_PRESSED = false)
281
         then 0
282
         else 1);
283

    
284
   chart_microwave_mode_logic_clear_off = 
285
      (if (CLEAR_PRESSED = false)
286
         then 0
287
         else 1);
288

    
289
   chart_microwave_mode_logic_door_closed = 
290
      (if (DOOR_CLOSED = false)
291
         then 0
292
         else 1);
293

    
294
   chart_microwave_mode_logic____wakeup___ = true;
295

    
296
   chart_microwave_mode_logic_rlt_evtInitStep = (true -> 
297
      (if (pre chart_microwave_mode_logic____wakeup___)
298
         then false
299
         else (pre chart_microwave_mode_logic_rlt_evtInitStep)));
300

    
301
   chart_microwave_mode_logic_begin_state_states___root = (0 -> (pre chart_microwave_mode_logic_final_state_states___root));
302

    
303
   chart_microwave_mode_logic_begin_state_outports_mode = (0 -> (pre chart_microwave_mode_logic_mode));
304

    
305
   chart_microwave_mode_logic_begin_state_outports_steps_remaining = (0 -> (pre chart_microwave_mode_logic_steps_remaining));
306

    
307
   chart_microwave_mode_logic_final_state_states___root = 
308
      (if chart_microwave_mode_logic____wakeup___
309
         then 
310
               (if chart_microwave_mode_logic_rlt_evtInitStep
311
                  then rlt_enter_microwave_mode_logic_rlt_state_2_states___root
312
                  else 
313
               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 
314
                  
315
                  
316
                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 
317
                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))
318
                  then 
319
                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6
320
                           then 
321
                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))
322
                                    then 
323
                                          
324
                                          3
325
                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)
326
                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)
327
                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root))
328
         else chart_microwave_mode_logic_begin_state_states___root);
329

    
330
   chart_microwave_mode_logic_mode = 
331
      (if chart_microwave_mode_logic____wakeup___
332
         then 
333
               (if chart_microwave_mode_logic_rlt_evtInitStep
334
                  then 
335
                        (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))
336
                           then 1
337
                           else chart_microwave_mode_logic_begin_state_outports_mode)
338
                  else 
339
               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 
340
                  
341
                  
342
                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 
343
                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))
344
                  then 
345
                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6
346
                           then 
347
                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))
348
                                    then 3
349
                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)
350
                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)
351
                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))
352
         else chart_microwave_mode_logic_begin_state_outports_mode);
353

    
354
   chart_microwave_mode_logic_steps_remaining = 
355
      (if chart_microwave_mode_logic____wakeup___
356
         then 
357
               (if chart_microwave_mode_logic_rlt_evtInitStep
358
                  then chart_microwave_mode_logic_begin_state_outports_steps_remaining
359
                  else 
360
               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 
361
                  
362
                  
363
                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 
364
                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))
365
                  then 
366
                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5
367
                           then (rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining - 1)
368
                           else rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining)
369
                  else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining))
370
         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);
371

    
372
   
373
   
374
   rlt_eval_microwave_mode_logic_rlt_fired_0 = (chart_microwave_mode_logic_begin_state_states___root = 4);
375

    
376
   
377
   
378
   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining = 
379
      (if rlt_eval_microwave_mode_logic_rlt_fired_0
380
         then STEPS_TO_COOK
381
         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);
382

    
383
   
384
   
385
   rlt_eval_microwave_mode_logic_rlt_fired_1 = (rlt_eval_microwave_mode_logic_rlt_fired_0 and 
386
      ((chart_microwave_mode_logic_begin_state_states___root = 4) and 
387
      (
388
      (if (chart_microwave_mode_logic_start <> 0)
389
         then true
390
         else false) and 
391
      
392
      (if (
393
         (if ((STEPS_TO_COOK > 0) = false)
394
            then 0
395
            else 1) <> 0)
396
         then true
397
         else false))));
398

    
399
   
400
   
401
   rlt_eval_microwave_mode_logic_rlt_state_2_states___root = 
402
      (if rlt_eval_microwave_mode_logic_rlt_fired_1
403
         then 
404
               (if (chart_microwave_mode_logic_begin_state_states___root = 4)
405
                  then 
406
                        
407
                        0
408
                  else chart_microwave_mode_logic_begin_state_states___root)
409
         else chart_microwave_mode_logic_begin_state_states___root);
410

    
411
   
412
   
413
   rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 
414
      (if rlt_eval_microwave_mode_logic_rlt_fired_1
415
         then rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root
416
         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);
417
   
418
   
419

    
420
   
421
   
422
   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode = 
423
      (if rlt_eval_microwave_mode_logic_rlt_fired_1
424
         then 
425
               (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2
426
                  then 
427
                        (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))
428
                           then 3
429
                           else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)
430
                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)
431
         else chart_microwave_mode_logic_begin_state_outports_mode);
432
   
433
   
434

    
435
   
436
   
437
   rlt_eval_microwave_mode_logic_ON_rlt_fired_1 = (((rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2) and 
438
      (rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining <= 0)) and 
439
      (rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2));
440

    
441
   
442
   
443
   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 
444
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1
445
         then 
446
               (if 
447
                  
448
                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 
449
                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3))
450
                  then 
451
                        
452
                        0
453
                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root)
454
         else rlt_eval_microwave_mode_logic_rlt_state_3_states___root);
455

    
456
   
457
   
458
   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 
459
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1
460
         then 
461
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))
462
                  then 
463
                        
464
                        4
465
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root)
466
         else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root);
467
   
468
   
469

    
470
   
471
   
472
   rlt_eval_microwave_mode_logic_ON_rlt_fired_2 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3) and 
473
      ((
474
      (if (chart_microwave_mode_logic_start <> 0)
475
         then true
476
         else false) and 
477
      
478
      (if (chart_microwave_mode_logic_door_closed <> 0)
479
         then true
480
         else false)) and 
481
      (not rlt_eval_microwave_mode_logic_ON_rlt_fired_1)));
482

    
483
   
484
   
485
   rlt_eval_microwave_mode_logic_ON_rlt_complete_1 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_2 or 
486
      rlt_eval_microwave_mode_logic_ON_rlt_fired_1);
487

    
488
   
489
   
490
   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 
491
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2
492
         then 
493
               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3)
494
                  then 
495
                        
496
                        1
497
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root)
498
         else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root);
499

    
500
   
501
   
502
   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode = 
503
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1
504
         then 
505
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))
506
                  then 1
507
                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode)
508
         else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode);
509

    
510
   
511
   
512
   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 
513
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2
514
         then 
515
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))
516
                  then 
517
                        
518
                        2
519
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root)
520
         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root);
521
   
522
   
523

    
524
   
525
   
526
   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode = 
527
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2
528
         then 
529
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))
530
                  then 2
531
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode)
532
         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode);
533
   
534
   
535

    
536
   
537
   
538
   rlt_eval_microwave_mode_logic_ON_rlt_fired_4 = (((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and 
539
      (
540
      (if (chart_microwave_mode_logic_clear_off <> 0)
541
         then true
542
         else false) and 
543
      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1))) and 
544
      ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and 
545
      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1)));
546

    
547
   
548
   
549
   rlt_eval_microwave_mode_logic_ON_rlt_complete_2 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_4 or 
550
      rlt_eval_microwave_mode_logic_ON_rlt_complete_1);
551

    
552
   
553
   
554
   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 
555
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4
556
         then 
557
               (if 
558
                  
559
                  ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root >= 1) and 
560
                  (rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root <= 3))
561
                  then 
562
                        
563
                        0
564
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root)
565
         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root);
566

    
567
   
568
   
569
   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining = 
570
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4
571
         then 0
572
         else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining);
573

    
574
   
575
   
576
   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 
577
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4
578
         then 
579
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))
580
                  then 
581
                        
582
                        4
583
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root)
584
         else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root);
585
   
586
   
587

    
588
   
589
   
590
   rlt_eval_microwave_mode_logic_ON_rlt_fired_5 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2) and 
591
      ((rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining > 0) and 
592
      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_2)));
593

    
594
   
595
   
596
   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode = 
597
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4
598
         then 
599
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))
600
                  then 1
601
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode)
602
         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode);
603

    
604
   
605
   
606
   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 
607
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5
608
         then 
609
               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2)
610
                  then 
611
                        
612
                        1
613
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root)
614
         else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root);
615

    
616
   
617
   
618
   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 
619
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5
620
         then 
621
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))
622
                  then 
623
                        
624
                        2
625
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root)
626
         else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root);
627
   
628
   
629

    
630
   
631
   
632
   rlt_eval_microwave_mode_logic_ON_rlt_fired_6 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2) and 
633
      ((
634
      (if (chart_microwave_mode_logic_clear_off <> 0)
635
         then true
636
         else false) or 
637
      (not 
638
      (if (chart_microwave_mode_logic_door_closed <> 0)
639
         then true
640
         else false))) and 
641
      (not (rlt_eval_microwave_mode_logic_ON_rlt_fired_5 or 
642
      rlt_eval_microwave_mode_logic_ON_rlt_complete_2))));
643

    
644
   
645
   
646
   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 
647
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6
648
         then 
649
               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2)
650
                  then 
651
                        
652
                        1
653
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root)
654
         else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root);
655

    
656
   
657
   
658
   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode = 
659
      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5
660
         then 
661
               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))
662
                  then 2
663
                  else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode)
664
         else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode);
665

    
666
   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 
667
      (if (not 
668
         
669
         ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and 
670
         (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3)))
671
         then 
672
               
673
               1
674
         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);
675

    
676
   
677
   
678
   rlt_enter_microwave_mode_logic_ON_rlt_fired_0 = ((not 
679
      
680
      ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and 
681
      (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3))) and 
682
      
683
      
684
      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and 
685
      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)));
686

    
687
   
688
   
689
   rlt_enter_microwave_mode_logic_ON_rlt_fired_1 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and 
690
      (
691
      
692
      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and 
693
      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)) and 
694
      
695
      (if (chart_microwave_mode_logic_door_closed <> 0)
696
         then true
697
         else false)));
698

    
699
   
700
   
701
   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 
702
      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1
703
         then 
704
               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))
705
                  then 
706
                        
707
                        2
708
                  else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root)
709
         else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root);
710
   
711
   
712

    
713
   
714
   
715
   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode = 
716
      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1
717
         then 
718
               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))
719
                  then 2
720
                  else chart_microwave_mode_logic_begin_state_outports_mode)
721
         else chart_microwave_mode_logic_begin_state_outports_mode);
722
   
723
   
724

    
725
   
726
   
727
   rlt_enter_microwave_mode_logic_ON_rlt_fired_2 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and 
728
      (
729
      
730
      ((rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root >= 1) and 
731
      (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root <= 3)) and 
732
      (not rlt_enter_microwave_mode_logic_ON_rlt_fired_1)));
733

    
734
   
735
   
736
   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root = 
737
      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2
738
         then 
739
               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))
740
                  then 
741
                        
742
                        3
743
                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root)
744
         else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root);
745
   
746
   
747

    
748
   
749
   
750
   rlt_enter_microwave_mode_logic_rlt_state_2_states___root = 
751
      (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))
752
         then 
753
               
754
               4
755
         else chart_microwave_mode_logic_begin_state_states___root);
756
   
757
   
758

    
759
   microwave_microwave_mode_logic_mode = chart_microwave_mode_logic_mode;
760

    
761

    
762
   MWI_FcnMaxI_In13 = ((pre rlt__Arrow5) - 1);
763

    
764

    
765
   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock = enable;
766

    
767
   KP_01 = KP_0;
768

    
769
   KP_11 = KP_1;
770

    
771
   KP_21 = KP_2;
772

    
773
   KP_31 = KP_3;
774

    
775
   KP_41 = KP_4;
776

    
777
   KP_51 = KP_5;
778

    
779
   KP_61 = KP_6;
780

    
781
   KP_71 = KP_7;
782

    
783
   KP_81 = KP_8;
784

    
785
   KP_91 = KP_9;
786

    
787
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY = (0 -> 
788
      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock
789
         then 
790
               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step
791
                  then 0
792
                  else 
793
               (if KP_CLEAR
794
                  then 0
795
                  else 
796
               (if 
797
                  (if (
798
                     (if (KP_01 and 
799
                        (not (pre KP_01)))
800
                        then 0
801
                        else 
802
                     (if (KP_11 and 
803
                        (not (pre KP_11)))
804
                        then 1
805
                        else 
806
                     (if (KP_21 and 
807
                        (not (pre KP_21)))
808
                        then 2
809
                        else 
810
                     (if (KP_31 and 
811
                        (not (pre KP_31)))
812
                        then 3
813
                        else 
814
                     (if (KP_41 and 
815
                        (not (pre KP_41)))
816
                        then 4
817
                        else 
818
                     (if (KP_51 and 
819
                        (not (pre KP_51)))
820
                        then 5
821
                        else 
822
                     (if (KP_61 and 
823
                        (not (pre KP_61)))
824
                        then 6
825
                        else 
826
                     (if (KP_71 and 
827
                        (not (pre KP_71)))
828
                        then 7
829
                        else 
830
                     (if (KP_81 and 
831
                        (not (pre KP_81)))
832
                        then 8
833
                        else 
834
                     (if (KP_91 and 
835
                        (not (pre KP_91)))
836
                        then 9
837
                        else 10)))))))))) <= 9)
838
                     then true
839
                     else false)
840
                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)
841
                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY))))
842
         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY)));
843

    
844
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY = (0 -> 
845
      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock
846
         then 
847
               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step
848
                  then 0
849
                  else 
850
               (if KP_CLEAR
851
                  then 0
852
                  else 
853
               (if 
854
                  (if (
855
                     (if (KP_01 and 
856
                        (not (pre KP_01)))
857
                        then 0
858
                        else 
859
                     (if (KP_11 and 
860
                        (not (pre KP_11)))
861
                        then 1
862
                        else 
863
                     (if (KP_21 and 
864
                        (not (pre KP_21)))
865
                        then 2
866
                        else 
867
                     (if (KP_31 and 
868
                        (not (pre KP_31)))
869
                        then 3
870
                        else 
871
                     (if (KP_41 and 
872
                        (not (pre KP_41)))
873
                        then 4
874
                        else 
875
                     (if (KP_51 and 
876
                        (not (pre KP_51)))
877
                        then 5
878
                        else 
879
                     (if (KP_61 and 
880
                        (not (pre KP_61)))
881
                        then 6
882
                        else 
883
                     (if (KP_71 and 
884
                        (not (pre KP_71)))
885
                        then 7
886
                        else 
887
                     (if (KP_81 and 
888
                        (not (pre KP_81)))
889
                        then 8
890
                        else 
891
                     (if (KP_91 and 
892
                        (not (pre KP_91)))
893
                        then 9
894
                        else 10)))))))))) <= 9)
895
                     then true
896
                     else false)
897
                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)
898
                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY))))
899
         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)));
900

    
901
   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY = (
902
      (if KP_CLEAR
903
         then 0
904
         else 
905
      (if 
906
         (if (
907
            (if KP_01
908
               then 0
909
               else 
910
            (if KP_11
911
               then 1
912
               else 
913
            (if KP_21
914
               then 2
915
               else 
916
            (if KP_31
917
               then 3
918
               else 
919
            (if KP_41
920
               then 4
921
               else 
922
            (if KP_51
923
               then 5
924
               else 
925
            (if KP_61
926
               then 6
927
               else 
928
            (if KP_71
929
               then 7
930
               else 
931
            (if KP_81
932
               then 8
933
               else 
934
            (if KP_91
935
               then 9
936
               else 10)))))))))) <= 9)
937
            then true
938
            else false)
939
         then 
940
               (if KP_01
941
                  then 0
942
                  else 
943
               (if KP_11
944
                  then 1
945
                  else 
946
               (if KP_21
947
                  then 2
948
                  else 
949
               (if KP_31
950
                  then 3
951
                  else 
952
               (if KP_41
953
                  then 4
954
                  else 
955
               (if KP_51
956
                  then 5
957
                  else 
958
               (if KP_61
959
                  then 6
960
                  else 
961
               (if KP_71
962
                  then 7
963
                  else 
964
               (if KP_81
965
                  then 8
966
                  else 
967
               (if KP_91
968
                  then 9
969
                  else 10))))))))))
970
         else 0)) -> 
971
      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock
972
         then 
973
               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step
974
                  then 
975
                        (if KP_CLEAR
976
                           then 0
977
                           else 
978
                        (if 
979
                           (if (
980
                              (if KP_01
981
                                 then 0
982
                                 else 
983
                              (if KP_11
984
                                 then 1
985
                                 else 
986
                              (if KP_21
987
                                 then 2
988
                                 else 
989
                              (if KP_31
990
                                 then 3
991
                                 else 
992
                              (if KP_41
993
                                 then 4
994
                                 else 
995
                              (if KP_51
996
                                 then 5
997
                                 else 
998
                              (if KP_61
999
                                 then 6
1000
                                 else 
1001
                              (if KP_71
1002
                                 then 7
1003
                                 else 
1004
                              (if KP_81
1005
                                 then 8
1006
                                 else 
1007
                              (if KP_91
1008
                                 then 9
1009
                                 else 10)))))))))) <= 9)
1010
                              then true
1011
                              else false)
1012
                           then 
1013
                                 (if KP_01
1014
                                    then 0
1015
                                    else 
1016
                                 (if KP_11
1017
                                    then 1
1018
                                    else 
1019
                                 (if KP_21
1020
                                    then 2
1021
                                    else 
1022
                                 (if KP_31
1023
                                    then 3
1024
                                    else 
1025
                                 (if KP_41
1026
                                    then 4
1027
                                    else 
1028
                                 (if KP_51
1029
                                    then 5
1030
                                    else 
1031
                                 (if KP_61
1032
                                    then 6
1033
                                    else 
1034
                                 (if KP_71
1035
                                    then 7
1036
                                    else 
1037
                                 (if KP_81
1038
                                    then 8
1039
                                    else 
1040
                                 (if KP_91
1041
                                    then 9
1042
                                    else 10))))))))))
1043
                           else 0))
1044
                  else 
1045
               (if KP_CLEAR
1046
                  then 0
1047
                  else 
1048
               (if 
1049
                  (if (
1050
                     (if (KP_01 and 
1051
                        (not (pre KP_01)))
1052
                        then 0
1053
                        else 
1054
                     (if (KP_11 and 
1055
                        (not (pre KP_11)))
1056
                        then 1
1057
                        else 
1058
                     (if (KP_21 and 
1059
                        (not (pre KP_21)))
1060
                        then 2
1061
                        else 
1062
                     (if (KP_31 and 
1063
                        (not (pre KP_31)))
1064
                        then 3
1065
                        else 
1066
                     (if (KP_41 and 
1067
                        (not (pre KP_41)))
1068
                        then 4
1069
                        else 
1070
                     (if (KP_51 and 
1071
                        (not (pre KP_51)))
1072
                        then 5
1073
                        else 
1074
                     (if (KP_61 and 
1075
                        (not (pre KP_61)))
1076
                        then 6
1077
                        else 
1078
                     (if (KP_71 and 
1079
                        (not (pre KP_71)))
1080
                        then 7
1081
                        else 
1082
                     (if (KP_81 and 
1083
                        (not (pre KP_81)))
1084
                        then 8
1085
                        else 
1086
                     (if (KP_91 and 
1087
                        (not (pre KP_91)))
1088
                        then 9
1089
                        else 10)))))))))) <= 9)
1090
                     then true
1091
                     else false)
1092
                  then 
1093
                        (if (KP_01 and 
1094
                           (not (pre KP_01)))
1095
                           then 0
1096
                           else 
1097
                        (if (KP_11 and 
1098
                           (not (pre KP_11)))
1099
                           then 1
1100
                           else 
1101
                        (if (KP_21 and 
1102
                           (not (pre KP_21)))
1103
                           then 2
1104
                           else 
1105
                        (if (KP_31 and 
1106
                           (not (pre KP_31)))
1107
                           then 3
1108
                           else 
1109
                        (if (KP_41 and 
1110
                           (not (pre KP_41)))
1111
                           then 4
1112
                           else 
1113
                        (if (KP_51 and 
1114
                           (not (pre KP_51)))
1115
                           then 5
1116
                           else 
1117
                        (if (KP_61 and 
1118
                           (not (pre KP_61)))
1119
                           then 6
1120
                           else 
1121
                        (if (KP_71 and 
1122
                           (not (pre KP_71)))
1123
                           then 7
1124
                           else 
1125
                        (if (KP_81 and 
1126
                           (not (pre KP_81)))
1127
                           then 8
1128
                           else 
1129
                        (if (KP_91 and 
1130
                           (not (pre KP_91)))
1131
                           then 9
1132
                           else 10))))))))))
1133
                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY))))
1134
         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)));
1135

    
1136
   STEPS_TO_COOK = (
1137
      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and 
1138
         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))
1139
         then 0
1140
         else ((((microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY * 1) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY * 10)) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY * 60)) * 1)) -> 
1141
      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and 
1142
         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))
1143
         then 0
1144
         else 
1145
      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock
1146
         then ((((microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY * 1) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY * 10)) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY * 60)) * 1)
1147
         else (pre STEPS_TO_COOK))));
1148

    
1149
   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step = (true -> 
1150
      (if (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)
1151
         then true
1152
         else 
1153
      (if (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)
1154
         then false
1155
         else (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step))));
1156

    
1157
   SETUP = 
1158
      (if (1 = microwave_microwave_mode_logic_mode)
1159
         then true
1160
         else false);
1161

    
1162
   enable = (true -> 
1163
      (if (1 = (pre microwave_microwave_mode_logic_mode))
1164
         then true
1165
         else false));
1166

    
1167

    
1168

    
1169

    
1170
   OK = (true -> ((not (enable and 
1171
      (not KP_CLEAR))) or 
1172
      ((not ((KP_7 and 
1173
      (not (pre KP_7))) and 
1174
      ((not (KP_6 and 
1175
      (not (pre KP_6)))) and 
1176
      ((not (KP_5 and 
1177
      (not (pre KP_5)))) and 
1178
      ((not (KP_4 and 
1179
      (not (pre KP_4)))) and 
1180
      ((not (KP_3 and 
1181
      (not (pre KP_3)))) and 
1182
      ((not (KP_2 and 
1183
      (not (pre KP_2)))) and 
1184
      ((not (KP_1 and 
1185
      (not (pre KP_1)))) and 
1186
      (not (KP_0 and 
1187
      (not (pre KP_0)))))))))))) or 
1188
      (RIGHT_DIGIT = 7))));
1189

    
1190

    
1191
  --%PROPERTY OK=true;
1192
  --%MAIN;
1193

    
1194
tel
1195