lustrectests / regression_tests / lustre_files / success / Stateflow / src_Microwave / Microwave.lus @ eb639349
History  View  Annotate  Download (18.2 KB)
1 
 This file has been generated by cocoSim 

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9  
10  
11  
12  
13  
14  
15 
node RUNNING_COOKING__To__RUNNING_COOKING_1_Transition_Action(steps_remaining_1:int) 
16  
17 
returns (steps_remaining:int); 
18  
19  
20 
var steps_remaining_2:int; 
21  
22  
23 
let 
24  
25  
26  
27 
steps_remaining_2 
28 
= steps_remaining_1  1; 
29 

30  
31 
(steps_remaining) 
32 
= (steps_remaining_2); 
33 

34  
35 
tel 
36  
37  
38  
39  
40  
41  
42  
43 
node Mode_logic_SETUP__To__Mode_logic_Mode_logicJunction1348_1_Condition_Action(steps_to_cook:int; 
44 
steps_remaining_1:int) 
45  
46 
returns (steps_remaining:int); 
47  
48  
49 
var steps_remaining_2:int; 
50  
51  
52 
let 
53  
54  
55  
56 
steps_remaining_2 
57 
= steps_to_cook; 
58 

59  
60 
(steps_remaining) 
61 
= (steps_remaining_2); 
62 

63  
64 
tel 
65  
66  
67  
68  
69  
70  
71  
72  
73  
74 
 Entry action for state :RUNNING_COOKING 
75 
node RUNNING_COOKING_en(idMode_logic_RUNNING_1:int; 
76 
mode_1:int; 
77 
isInner:bool) 
78  
79 
returns (idMode_logic_RUNNING:int; 
80 
mode:int); 
81  
82  
83 
var idMode_logic_RUNNING_2:int; 
84 
mode_2:int; 
85  
86  
87 
let 
88  
89  
90  
91 
 set state as active 
92 
idMode_logic_RUNNING_2 
93 
= 1332; 
94 

95  
96 
mode_2 
97 
= if (not isInner) then 2 
98 
else mode_1; 
99 

100  
101 
(idMode_logic_RUNNING, mode) 
102 
= (idMode_logic_RUNNING_2, mode_2); 
103 

104  
105 
tel 
106  
107  
108  
109  
110  
111 
 Exit action for state :RUNNING_COOKING 
112 
node RUNNING_COOKING_ex(idMode_logic_RUNNING_1:int; 
113 
isInner:bool) 
114  
115 
returns (idMode_logic_RUNNING:int); 
116  
117  
118 
var idMode_logic_RUNNING_2:int; 
119  
120  
121 
let 
122  
123  
124  
125 
 set state as inactive 
126 
idMode_logic_RUNNING_2 
127 
= if (not isInner) then 0 else idMode_logic_RUNNING_1; 
128  
129  
130 
(idMode_logic_RUNNING) 
131 
= (idMode_logic_RUNNING_1); 
132 

133  
134 
tel 
135  
136  
137  
138  
139  
140  
141 
 Entry action for state :RUNNING_SUSPENDED 
142 
node RUNNING_SUSPENDED_en(idMode_logic_RUNNING_1:int; 
143 
mode_1:int; 
144 
isInner:bool) 
145  
146 
returns (idMode_logic_RUNNING:int; 
147 
mode:int); 
148  
149  
150 
var idMode_logic_RUNNING_2:int; 
151 
mode_2:int; 
152  
153  
154 
let 
155  
156  
157  
158 
 set state as active 
159 
idMode_logic_RUNNING_2 
160 
= 1333; 
161 

162  
163 
mode_2 
164 
= if (not isInner) then 3 
165 
else mode_1; 
166 

167  
168 
(idMode_logic_RUNNING, mode) 
169 
= (idMode_logic_RUNNING_2, mode_2); 
170 

171  
172 
tel 
173  
174  
175  
176  
177  
178 
 Exit action for state :RUNNING_SUSPENDED 
179 
node RUNNING_SUSPENDED_ex(idMode_logic_RUNNING_1:int; 
180 
isInner:bool) 
181  
182 
returns (idMode_logic_RUNNING:int); 
183  
184  
185 
var idMode_logic_RUNNING_2:int; 
186  
187  
188 
let 
189  
190  
191  
192 
 set state as inactive 
193 
idMode_logic_RUNNING_2 
194 
= if (not isInner) then 0 else idMode_logic_RUNNING_1; 
195  
196  
197 
(idMode_logic_RUNNING) 
198 
= (idMode_logic_RUNNING_1); 
199 

200  
201 
tel 
202  
203  
204  
205  
206  
207  
208 
 Entry action for state :Mode_logic_RUNNING 
209 
node Mode_logic_RUNNING_en(idMode_logic_RUNNING_1:int; 
210 
idMode_logic_Mode_logic_1:int; 
211 
door_closed:bool; 
212 
mode_1:int; 
213 
isInner:bool) 
214  
215 
returns (idMode_logic_RUNNING:int; 
216 
idMode_logic_Mode_logic:int; 
217 
mode:int); 
218  
219  
220 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3, idMode_logic_RUNNING_4, idMode_logic_RUNNING_5, idMode_logic_RUNNING_6, idMode_logic_RUNNING_7:int; 
221 
idMode_logic_Mode_logic_2, idMode_logic_Mode_logic_3, idMode_logic_Mode_logic_4:int; 
222 
mode_2, mode_3, mode_4, mode_5, mode_6, mode_7:int; 
223  
224  
225 
let 
226  
227  
228  
229 
 set state as active 
230 
idMode_logic_Mode_logic_2 
231 
= 1334; 
232 

233  
234 

235  
236  
237 
 transition trace : 
238 
POINT__To__Junction1335_1, Junction1335__To__RUNNING_COOKING_1 
239 
(idMode_logic_RUNNING_2, mode_2) 
240 
= 
241 
if (( door_closed )) then 
242 
RUNNING_COOKING_en(idMode_logic_RUNNING_1, mode_1, false) 
243 
else (idMode_logic_RUNNING_1, mode_1); 
244 

245  
246  
247 
 transition trace : 
248 
POINT__To__Junction1335_1, Junction1335__To__RUNNING_SUSPENDED_2 
249 
(idMode_logic_RUNNING_3, mode_3) 
250 
= RUNNING_SUSPENDED_en(idMode_logic_RUNNING_1, mode_1, false); 
251 

252  
253 
(idMode_logic_RUNNING_4, idMode_logic_Mode_logic_3, mode_4) 
254 
= 
255  
256 
if ( idMode_logic_RUNNING_1 = 0) then 
257  
258 

259 
if (( door_closed )) then 
260 
(idMode_logic_RUNNING_2, idMode_logic_Mode_logic_2, mode_2) 
261 
else (idMode_logic_RUNNING_3, idMode_logic_Mode_logic_2, mode_3) 
262  
263 
else(idMode_logic_RUNNING_1, idMode_logic_Mode_logic_2, mode_1); 
264  
265 

266  
267 
(idMode_logic_RUNNING_5, mode_5) 
268 
= 
269 
if ( idMode_logic_RUNNING_1 = 1332) then 
270 
RUNNING_COOKING_en(idMode_logic_RUNNING_1, mode_1, false) 
271 
else (idMode_logic_RUNNING_1, mode_1); 
272  
273 

274  
275 
(idMode_logic_RUNNING_6, mode_6) 
276 
= 
277 
if ( idMode_logic_RUNNING_1 = 1333) then 
278 
RUNNING_SUSPENDED_en(idMode_logic_RUNNING_1, mode_1, false) 
279 
else (idMode_logic_RUNNING_1, mode_1); 
280  
281 

282  
283 
(idMode_logic_RUNNING_7, idMode_logic_Mode_logic_4, mode_7) 
284 
= 
285 
if ( idMode_logic_RUNNING_1 = 0) then 
286 
(idMode_logic_RUNNING_4, idMode_logic_Mode_logic_3, mode_4) 
287 
else 
288 
if ( idMode_logic_RUNNING_1 = 1332) then 
289 
(idMode_logic_RUNNING_5, idMode_logic_Mode_logic_3, mode_5) 
290 
else 
291 
if ( idMode_logic_RUNNING_1 = 1333) then 
292 
(idMode_logic_RUNNING_6, idMode_logic_Mode_logic_3, mode_6) 
293 
else (idMode_logic_RUNNING_1, idMode_logic_Mode_logic_2, mode_1); 
294  
295  
296 
(idMode_logic_RUNNING, idMode_logic_Mode_logic, mode) 
297 
= (idMode_logic_RUNNING_7, idMode_logic_Mode_logic_4, mode_7); 
298 

299  
300 
tel 
301  
302  
303  
304  
305  
306 
 Exit action for state :Mode_logic_RUNNING 
307 
node Mode_logic_RUNNING_ex(idMode_logic_RUNNING_1:int; 
308 
idMode_logic_Mode_logic_1:int; 
309 
isInner:bool) 
310  
311 
returns (idMode_logic_RUNNING:int; 
312 
idMode_logic_Mode_logic:int); 
313  
314  
315 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3, idMode_logic_RUNNING_4, idMode_logic_RUNNING_5:int; 
316 
idMode_logic_Mode_logic_2:int; 
317  
318  
319 
let 
320  
321  
322  
323 

324 
(idMode_logic_RUNNING_2) 
325 
= 
326 
if ( idMode_logic_RUNNING_1 = 1332) then 
327 
RUNNING_COOKING_ex(idMode_logic_RUNNING_1, false) 
328 
else (idMode_logic_RUNNING_1); 
329  
330 

331  
332 
(idMode_logic_RUNNING_3) 
333 
= 
334 
if ( idMode_logic_RUNNING_1 = 1333) then 
335 
RUNNING_SUSPENDED_ex(idMode_logic_RUNNING_1, false) 
336 
else (idMode_logic_RUNNING_1); 
337  
338 

339  
340 
(idMode_logic_RUNNING_4) 
341 
= 
342 
if ( idMode_logic_RUNNING_1 = 1332) then 
343 
(idMode_logic_RUNNING_2) 
344 
else 
345 
if ( idMode_logic_RUNNING_1 = 1333) then 
346 
(idMode_logic_RUNNING_3) 
347 
else (idMode_logic_RUNNING_1); 
348  
349  
350 
 set state as inactive 
351 
idMode_logic_Mode_logic_2 
352 
= if (not isInner) then 0 else idMode_logic_Mode_logic_1; 
353  
354 
idMode_logic_RUNNING_5 
355 
= 0; 
356 

357  
358 
(idMode_logic_RUNNING, idMode_logic_Mode_logic) 
359 
= (idMode_logic_RUNNING_5, idMode_logic_Mode_logic_1); 
360 

361  
362 
tel 
363  
364  
365  
366  
367  
368  
369 
 Entry action for state :Mode_logic_SETUP 
370 
node Mode_logic_SETUP_en(idMode_logic_Mode_logic_1:int; 
371 
mode_1:int; 
372 
steps_to_cook:int; 
373 
steps_remaining_1:int; 
374 
isInner:bool) 
375  
376 
returns (idMode_logic_Mode_logic:int; 
377 
mode:int; 
378 
steps_remaining:int); 
379  
380  
381 
var idMode_logic_Mode_logic_2:int; 
382 
mode_2:int; 
383 
steps_remaining_2:int; 
384  
385  
386 
let 
387  
388  
389  
390 
 set state as active 
391 
idMode_logic_Mode_logic_2 
392 
= 1331; 
393 

394  
395 
mode_2 
396 
= if (not isInner) then 1 
397 
else mode_1; 
398 

399  
400 
steps_remaining_2 
401 
= if (not isInner) then steps_to_cook 
402 
else steps_remaining_1; 
403 

404  
405 
(idMode_logic_Mode_logic, mode, steps_remaining) 
406 
= (idMode_logic_Mode_logic_2, mode_2, steps_remaining_2); 
407 

408  
409 
tel 
410  
411  
412  
413  
414  
415 
 Exit action for state :Mode_logic_SETUP 
416 
node Mode_logic_SETUP_ex(idMode_logic_Mode_logic_1:int; 
417 
isInner:bool) 
418  
419 
returns (idMode_logic_Mode_logic:int); 
420  
421  
422 
var idMode_logic_Mode_logic_2:int; 
423  
424  
425 
let 
426  
427  
428  
429 
 set state as inactive 
430 
idMode_logic_Mode_logic_2 
431 
= if (not isInner) then 0 else idMode_logic_Mode_logic_1; 
432  
433  
434 
(idMode_logic_Mode_logic) 
435 
= (idMode_logic_Mode_logic_1); 
436 

437  
438 
tel 
439  
440  
441 
***************************************************State :Mode_logic_RUNNING Automaton*************************************************** 
442  
443 
node Mode_logic_RUNNING_node(idMode_logic_RUNNING_1:int; 
444 
door_closed:bool; 
445 
mode_1:int; 
446 
steps_remaining_1:int; 
447 
clear:bool; 
448 
idMode_logic_Mode_logic_1:int; 
449 
steps_to_cook:int; 
450 
start:bool) 
451  
452 
returns (idMode_logic_RUNNING:int; 
453 
mode:int; 
454 
steps_remaining:int; 
455 
idMode_logic_Mode_logic:int); 
456  
457  
458 
let 
459  
460 
automaton mode_logic_running 
461  
462 
state POINTMode_logic_RUNNING: 
463 
unless (idMode_logic_RUNNING_1=0) restart POINT__TO__MODE_LOGIC_MODE_LOGICJUNCTION1335_1 
464  
465  
466  
467 
unless (idMode_logic_RUNNING_1=1332) and ( steps_remaining_1 >0 ) restart RUNNING_COOKING__TO__RUNNING_COOKING_1 
468  
469  
470  
471 
unless (idMode_logic_RUNNING_1=1332) and ( clear or not door_closed ) restart RUNNING_COOKING__TO__RUNNING_SUSPENDED_2 
472  
473  
474  
475 
unless (idMode_logic_RUNNING_1=1333) and ( clear ) restart RUNNING_SUSPENDED__TO__MODE_LOGIC_MODE_LOGICJUNCTION1349_1 
476  
477  
478  
479 
unless (idMode_logic_RUNNING_1=1333) and ( start and door_closed ) restart RUNNING_SUSPENDED__TO__RUNNING_COOKING_2 
480  
481  
482  
483 
unless (idMode_logic_RUNNING_1=1332) restart RUNNING_COOKING_IDL 
484  
485 
unless (idMode_logic_RUNNING_1=1333) restart RUNNING_SUSPENDED_IDL 
486  
487 
let 
488  
489 
(idMode_logic_RUNNING, mode, steps_remaining, idMode_logic_Mode_logic) 
490 
= (idMode_logic_RUNNING_1, mode_1, steps_remaining_1, idMode_logic_Mode_logic_1); 
491 

492  
493 
tel 
494  
495  
496  
497 
state POINT__TO__MODE_LOGIC_MODE_LOGICJUNCTION1335_1: 
498  
499 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3:int; 
500 
mode_2, mode_3:int; 
501 
let 
502  
503 

504  
505 
 transition trace : 
506 
POINT__To__Junction1335_1, Junction1335__To__RUNNING_COOKING_1 
507 
(idMode_logic_RUNNING_2, mode_2) 
508 
= 
509 
if (( door_closed )) then 
510 
RUNNING_COOKING_en(idMode_logic_RUNNING_1, mode_1, false) 
511 
else (idMode_logic_RUNNING_1, mode_1); 
512 

513  
514  
515 
 transition trace : 
516 
POINT__To__Junction1335_1, Junction1335__To__RUNNING_SUSPENDED_2 
517 
(idMode_logic_RUNNING_3, mode_3) 
518 
= RUNNING_SUSPENDED_en(idMode_logic_RUNNING_1, mode_1, false); 
519 

520  
521 
(idMode_logic_RUNNING, mode) 
522 
= 
523 
if (( door_closed )) then 
524 
(idMode_logic_RUNNING_2, mode_2) 
525 
else (idMode_logic_RUNNING_3, mode_3); 
526  
527 
add unused variables 
528 
(idMode_logic_Mode_logic, steps_remaining) 
529 
= (idMode_logic_Mode_logic_1, steps_remaining_1); 
530 

531  
532 
tel 
533  
534 
until true restart POINTMode_logic_RUNNING 
535  
536  
537  
538 
state RUNNING_COOKING__TO__RUNNING_COOKING_1: 
539  
540 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3:int; 
541 
mode_2:int; 
542 
steps_remaining_2:int; 
543 
let 
544  
545 
 transition trace : 
546 
RUNNING_COOKING__To__RUNNING_COOKING_1 
547 
(idMode_logic_RUNNING_2) 
548 
= RUNNING_COOKING_ex(idMode_logic_RUNNING_1, false); 
549 

550  
551 
(steps_remaining_2) 
552 
= RUNNING_COOKING__To__RUNNING_COOKING_1_Transition_Action(steps_remaining_1); 
553 

554  
555 
(idMode_logic_RUNNING_3, mode_2) 
556 
= RUNNING_COOKING_en(idMode_logic_RUNNING_2, mode_1, false); 
557 

558  
559 
(idMode_logic_RUNNING, mode, steps_remaining) 
560 
= (idMode_logic_RUNNING_3, mode_2, steps_remaining_2); 
561  
562 
add unused variables 
563 
(idMode_logic_Mode_logic) 
564 
= (idMode_logic_Mode_logic_1); 
565 

566  
567 
tel 
568  
569 
until true restart POINTMode_logic_RUNNING 
570  
571  
572  
573 
state RUNNING_COOKING__TO__RUNNING_SUSPENDED_2: 
574  
575 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3:int; 
576 
mode_2:int; 
577 
let 
578  
579 
 transition trace : 
580 
RUNNING_COOKING__To__RUNNING_SUSPENDED_2 
581 
(idMode_logic_RUNNING_2) 
582 
= RUNNING_COOKING_ex(idMode_logic_RUNNING_1, false); 
583 

584  
585 
(idMode_logic_RUNNING_3, mode_2) 
586 
= RUNNING_SUSPENDED_en(idMode_logic_RUNNING_2, mode_1, false); 
587 

588  
589 
(idMode_logic_RUNNING, mode, steps_remaining) 
590 
= (idMode_logic_RUNNING_3, mode_2, steps_remaining_1); 
591  
592 
add unused variables 
593 
(idMode_logic_Mode_logic) 
594 
= (idMode_logic_Mode_logic_1); 
595 

596  
597 
tel 
598  
599 
until true restart POINTMode_logic_RUNNING 
600  
601  
602  
603 
state RUNNING_SUSPENDED__TO__MODE_LOGIC_MODE_LOGICJUNCTION1349_1: 
604  
605 
var idMode_logic_RUNNING_2:int; 
606 
mode_2:int; 
607 
steps_remaining_2:int; 
608 
idMode_logic_Mode_logic_2, idMode_logic_Mode_logic_3:int; 
609 
let 
610  
611 

612  
613 
 transition trace : 
614 
RUNNING_SUSPENDED__To__Junction1349_1, Junction1349__To__Mode_logic_SETUP_1 
615 
(idMode_logic_RUNNING_2, idMode_logic_Mode_logic_2) 
616 
= Mode_logic_RUNNING_ex(idMode_logic_RUNNING_1, idMode_logic_Mode_logic_1, false); 
617 

618  
619 
(idMode_logic_Mode_logic_3, mode_2, steps_remaining_2) 
620 
= Mode_logic_SETUP_en(idMode_logic_Mode_logic_2, mode_1, steps_to_cook, steps_remaining_1, false); 
621 

622  
623 
(idMode_logic_RUNNING, mode, steps_remaining, idMode_logic_Mode_logic) 
624 
= (idMode_logic_RUNNING_2, mode_2, steps_remaining_2, idMode_logic_Mode_logic_3); 
625  
626  
627 
tel 
628  
629 
until true restart POINTMode_logic_RUNNING 
630  
631  
632  
633 
state RUNNING_SUSPENDED__TO__RUNNING_COOKING_2: 
634  
635 
var idMode_logic_RUNNING_2, idMode_logic_RUNNING_3:int; 
636 
mode_2:int; 
637 
let 
638  
639 
 transition trace : 
640 
RUNNING_SUSPENDED__To__RUNNING_COOKING_2 
641 
(idMode_logic_RUNNING_2) 
642 
= RUNNING_SUSPENDED_ex(idMode_logic_RUNNING_1, false); 
643 

644  
645 
(idMode_logic_RUNNING_3, mode_2) 
646 
= RUNNING_COOKING_en(idMode_logic_RUNNING_2, mode_1, false); 
647 

648  
649 
(idMode_logic_RUNNING, mode, steps_remaining, idMode_logic_Mode_logic) 
650 
= (idMode_logic_RUNNING_3, mode_2, steps_remaining_1, idMode_logic_Mode_logic_1); 
651  
652  
653 
tel 
654  
655 
until true restart POINTMode_logic_RUNNING 
656  
657  
658  
659 
state RUNNING_COOKING_IDL: 
660  
661 
let 
662  
663 

664  
665 
(idMode_logic_RUNNING, mode, steps_remaining, idMode_logic_Mode_logic) 
666 
= (idMode_logic_RUNNING_1, mode_1, steps_remaining_1, idMode_logic_Mode_logic_1); 
667 

668  
669 
tel 
670  
671 
until true restart POINTMode_logic_RUNNING 
672  
673  
674  
675 
state RUNNING_SUSPENDED_IDL: 
676  
677 
let 
678  
679 

680  
681 
(idMode_logic_RUNNING, mode, steps_remaining, idMode_logic_Mode_logic) 
682 
= (idMode_logic_RUNNING_1, mode_1, steps_remaining_1, idMode_logic_Mode_logic_1); 
683 

684  
685 
tel 
686  
687 
until true restart POINTMode_logic_RUNNING 
688  
689  
690  
691 
tel 
692  
693  
694 
***************************************************State :Mode_logic_Mode_logic Automaton*************************************************** 
695  
696 
node Mode_logic_Mode_logic_node(idMode_logic_Mode_logic_1:int; 
697 
mode_1:int; 
698 
steps_remaining_1:int; 
699 
steps_to_cook:int; 
700 
start:bool; 
701 
door_closed:bool; 
702 
idMode_logic_RUNNING_1:int; 
703 
clear:bool) 
704  
705 
returns (idMode_logic_Mode_logic:int; 
706 
mode:int; 
707 
steps_remaining:int; 
708 
idMode_logic_RUNNING:int); 
709  
710  
711 
let 
712  
713 
automaton mode_logic_mode_logic 
714  
715 
state POINTMode_logic_Mode_logic: 
716 
unless (idMode_logic_Mode_logic_1=0) restart POINT__TO__MODE_LOGIC_SETUP_1 
717  
718  
719  
720 
unless (idMode_logic_Mode_logic_1=1331) restart MODE_LOGIC_SETUP__TO__MODE_LOGIC_MODE_LOGICJUNCTION1348_1 
721  
722  
723  
724 
unless (idMode_logic_Mode_logic_1=1334) and ( steps_remaining_1 <=0 ) restart MODE_LOGIC_RUNNING__TO__MODE_LOGIC_MODE_LOGICJUNCTION1349_1 
725  
726  
727  
728 
unless (idMode_logic_Mode_logic_1=1331) restart MODE_LOGIC_SETUP_IDL 
729  
730 
unless (idMode_logic_Mode_logic_1=1334) restart MODE_LOGIC_RUNNING_IDL 
731  
732 
let 
733  
734 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
735 
= (idMode_logic_Mode_logic_1, mode_1, steps_remaining_1, idMode_logic_RUNNING_1); 
736 

737  
738 
tel 
739  
740  
741  
742 
state POINT__TO__MODE_LOGIC_SETUP_1: 
743  
744 
var idMode_logic_Mode_logic_2:int; 
745 
mode_2:int; 
746 
steps_remaining_2:int; 
747 
let 
748  
749 
 transition trace : 
750 
POINT__To__Mode_logic_SETUP_1 
751 
(idMode_logic_Mode_logic_2, mode_2, steps_remaining_2) 
752 
= Mode_logic_SETUP_en(idMode_logic_Mode_logic_1, mode_1, steps_to_cook, steps_remaining_1, false); 
753 

754  
755 
(idMode_logic_Mode_logic, mode, steps_remaining) 
756 
= (idMode_logic_Mode_logic_2, mode_2, steps_remaining_2); 
757  
758 
add unused variables 
759 
(idMode_logic_RUNNING) 
760 
= (idMode_logic_RUNNING_1); 
761 

762  
763 
tel 
764  
765 
until true restart POINTMode_logic_Mode_logic 
766  
767  
768  
769 
state MODE_LOGIC_SETUP__TO__MODE_LOGIC_MODE_LOGICJUNCTION1348_1: 
770  
771 
var idMode_logic_Mode_logic_2, idMode_logic_Mode_logic_3:int; 
772 
mode_2:int; 
773 
steps_remaining_2:int; 
774 
idMode_logic_RUNNING_2:int; 
775 
let 
776  
777 

778  
779 
 transition trace : 
780 
Mode_logic_SETUP__To__Junction1348_1, Junction1348__To__Mode_logic_RUNNING_1 
781 
 condition Action : steps_remaining=steps_to_cook; 
782 

783 
(steps_remaining_2) 
784 
= Mode_logic_SETUP__To__Mode_logic_Mode_logicJunction1348_1_Condition_Action(steps_to_cook, steps_remaining_1); 
785 

786  
787 
(idMode_logic_Mode_logic_2) 
788 
= 
789 
if (( start and steps_remaining_2 >0 )) then 
790 
Mode_logic_SETUP_ex(idMode_logic_Mode_logic_1, false) 
791 
else (idMode_logic_Mode_logic_1); 
792 

793  
794 
(idMode_logic_RUNNING_2, idMode_logic_Mode_logic_3, mode_2) 
795 
= 
796 
if (( start and steps_remaining_2 >0 )) then 
797 
Mode_logic_RUNNING_en(idMode_logic_RUNNING_1, idMode_logic_Mode_logic_2, door_closed, mode_1, false) 
798 
else (idMode_logic_RUNNING_1, idMode_logic_Mode_logic_2, mode_1); 
799 

800  
801 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
802 
= 
803 
if (( start and steps_remaining_2 >0 )) then 
804 
(idMode_logic_Mode_logic_3, mode_2, steps_remaining_2, idMode_logic_RUNNING_2) 
805 
else (idMode_logic_Mode_logic_1, mode_1, steps_remaining_2, idMode_logic_RUNNING_1); 
806  
807  
808 
tel 
809  
810 
until true restart POINTMode_logic_Mode_logic 
811  
812  
813  
814 
state MODE_LOGIC_RUNNING__TO__MODE_LOGIC_MODE_LOGICJUNCTION1349_1: 
815  
816 
var idMode_logic_Mode_logic_2, idMode_logic_Mode_logic_3:int; 
817 
mode_2:int; 
818 
steps_remaining_2:int; 
819 
idMode_logic_RUNNING_2:int; 
820 
let 
821  
822 

823  
824 
 transition trace : 
825 
Mode_logic_RUNNING__To__Junction1349_1, Junction1349__To__Mode_logic_SETUP_1 
826 
(idMode_logic_RUNNING_2, idMode_logic_Mode_logic_2) 
827 
= Mode_logic_RUNNING_ex(idMode_logic_RUNNING_1, idMode_logic_Mode_logic_1, false); 
828 

829  
830 
(idMode_logic_Mode_logic_3, mode_2, steps_remaining_2) 
831 
= Mode_logic_SETUP_en(idMode_logic_Mode_logic_2, mode_1, steps_to_cook, steps_remaining_1, false); 
832 

833  
834 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
835 
= (idMode_logic_Mode_logic_3, mode_2, steps_remaining_2, idMode_logic_RUNNING_2); 
836  
837  
838 
tel 
839  
840 
until true restart POINTMode_logic_Mode_logic 
841  
842  
843  
844 
state MODE_LOGIC_SETUP_IDL: 
845  
846 
let 
847  
848 

849  
850 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
851 
= (idMode_logic_Mode_logic_1, mode_1, steps_remaining_1, idMode_logic_RUNNING_1); 
852 

853  
854 
tel 
855  
856 
until true restart POINTMode_logic_Mode_logic 
857  
858  
859  
860 
state MODE_LOGIC_RUNNING_IDL: 
861  
862 
var idMode_logic_Mode_logic_2:int; 
863 
mode_2:int; 
864 
steps_remaining_2:int; 
865 
idMode_logic_RUNNING_2:int; 
866 
let 
867  
868 

869 
(idMode_logic_RUNNING_2, mode_2, steps_remaining_2, idMode_logic_Mode_logic_2) 
870 
= Mode_logic_RUNNING_node(idMode_logic_RUNNING_1, door_closed, mode_1, steps_remaining_1, clear, idMode_logic_Mode_logic_1, steps_to_cook, start); 
871  
872 

873  
874  
875 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
876 
= (idMode_logic_Mode_logic_2, mode_2, steps_remaining_2, idMode_logic_RUNNING_2); 
877 

878  
879 
tel 
880  
881 
until true restart POINTMode_logic_Mode_logic 
882  
883  
884  
885 
tel 
886  
887  
888 
***************************************************State :Mode_logic_Mode_logic Automaton*************************************************** 
889  
890 
node Microwave_Mode_logic(start:bool; 
891 
clear:bool; 
892 
steps_to_cook:int; 
893 
door_closed:bool) 
894  
895 
returns (mode:int; 
896 
steps_remaining:int); 
897  
898  
899 
var mode_1: int; 
900  
901 
steps_remaining_1: int; 
902  
903 
idMode_logic_Mode_logic, idMode_logic_Mode_logic_1: int; 
904  
905 
idMode_logic_RUNNING, idMode_logic_RUNNING_1: int; 
906  
907 
let 
908  
909 
mode_1 = 0 > pre mode; 
910  
911 
steps_remaining_1 = 0 > pre steps_remaining; 
912  
913 
idMode_logic_Mode_logic_1 = 0 > pre idMode_logic_Mode_logic; 
914  
915 
idMode_logic_RUNNING_1 = 0 > pre idMode_logic_RUNNING; 
916  
917 

918  
919  
920  
921 
(idMode_logic_Mode_logic, mode, steps_remaining, idMode_logic_RUNNING) 
922 
= Mode_logic_Mode_logic_node(idMode_logic_Mode_logic_1, mode_1, steps_remaining_1, steps_to_cook, start, door_closed, idMode_logic_RUNNING_1, clear); 
923  
924  
925 
unused outputs 
926 

927  
928 
tel 
929  
930  
931  
932 
node Microwave (start_1_1 : bool; clear_1_1 : bool; steps_to_cook_1_1 : int; door_closed_1_1 : bool) 
933 
returns (mode_1_1 : int; 
934 
steps_remaining_2_1 : int); 
935 
var 
936 
Mode_logic_1_1 : int; Mode_logic_2_1 : int; 
937 
i_virtual_local : real; 
938 
let 
939 
(Mode_logic_1_1, Mode_logic_2_1) = Microwave_Mode_logic(start_1_1, clear_1_1, steps_to_cook_1_1, door_closed_1_1); 
940 
mode_1_1 = Mode_logic_1_1; 
941 
steps_remaining_2_1 = Mode_logic_2_1; 
942 
i_virtual_local= 0.0 > 1.0; 
943 
tel 
944 