Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Inner3 / Inner3.lus @ eb639349

History | View | Annotate | Download (18.3 KB)

1 eb639349 bourbouh
-- This file has been generated by cocoSim
2
3
4
-- System nodes
5
6
7
8
9
10
11
12
13
14
15
-- Entry action for state :A_A3
16
node A_A3_en(idInner3_A_1:int;
17
	enA3cnt_1:int;
18
	isInner:bool)
19
20
returns (idInner3_A:int;
21
	enA3cnt:int);
22
23
24
var 	idInner3_A_2:int;
25
	enA3cnt_2:int;
26
27
28
let
29
30
31
32
	-- set state as active 
33
	idInner3_A_2 
34
	= 1085;
35
	
36
37
	enA3cnt_2 
38
	= if (not isInner) then  enA3cnt_1  + 1
39
	 else enA3cnt_1;
40
	
41
42
	(idInner3_A, enA3cnt) 
43
	= (idInner3_A_2, enA3cnt_2);
44
	
45
46
tel
47
48
49
50
51
52
--During action for state :A_A3
53
node A_A3_du(duA3cnt_1:int)
54
55
returns (duA3cnt:int);
56
57
58
var 	duA3cnt_2:int;
59
60
61
let
62
63
64
65
	duA3cnt_2 
66
	=  duA3cnt_1  + 1;
67
	
68
69
	(duA3cnt) 
70
	= (duA3cnt_2);
71
	
72
73
tel
74
75
76
77
78
79
-- Exit action for state :A_A3
80
node A_A3_ex(exA3cnt_1:int;
81
	idInner3_A_1:int;
82
	isInner:bool)
83
84
returns (exA3cnt:int;
85
	idInner3_A:int);
86
87
88
var 	exA3cnt_2:int;
89
	idInner3_A_2:int;
90
91
92
let
93
94
95
96
	exA3cnt_2 
97
	= if (not isInner) then  exA3cnt_1  + 1
98
	 else exA3cnt_1;
99
	
100
101
	-- set state as inactive 
102
	idInner3_A_2
103
	 = if (not isInner) then 0 else idInner3_A_1;
104
105
106
	(exA3cnt, idInner3_A) 
107
	= (exA3cnt_2, idInner3_A_1);
108
	
109
110
tel
111
112
113
114
115
116
117
-- Entry action for state :A_A2
118
node A_A2_en(idInner3_A_1:int;
119
	enA2cnt_1:int;
120
	isInner:bool)
121
122
returns (idInner3_A:int;
123
	enA2cnt:int);
124
125
126
var 	idInner3_A_2:int;
127
	enA2cnt_2:int;
128
129
130
let
131
132
133
134
	-- set state as active 
135
	idInner3_A_2 
136
	= 1084;
137
	
138
139
	enA2cnt_2 
140
	= if (not isInner) then  enA2cnt_1  + 1
141
	 else enA2cnt_1;
142
	
143
144
	(idInner3_A, enA2cnt) 
145
	= (idInner3_A_2, enA2cnt_2);
146
	
147
148
tel
149
150
151
152
153
154
--During action for state :A_A2
155
node A_A2_du(duA2cnt_1:int)
156
157
returns (duA2cnt:int);
158
159
160
var 	duA2cnt_2:int;
161
162
163
let
164
165
166
167
	duA2cnt_2 
168
	=  duA2cnt_1  + 1;
169
	
170
171
	(duA2cnt) 
172
	= (duA2cnt_2);
173
	
174
175
tel
176
177
178
179
180
181
-- Exit action for state :A_A2
182
node A_A2_ex(exA2cnt_1:int;
183
	idInner3_A_1:int;
184
	isInner:bool)
185
186
returns (exA2cnt:int;
187
	idInner3_A:int);
188
189
190
var 	exA2cnt_2:int;
191
	idInner3_A_2:int;
192
193
194
let
195
196
197
198
	exA2cnt_2 
199
	= if (not isInner) then  exA2cnt_1  + 1
200
	 else exA2cnt_1;
201
	
202
203
	-- set state as inactive 
204
	idInner3_A_2
205
	 = if (not isInner) then 0 else idInner3_A_1;
206
207
208
	(exA2cnt, idInner3_A) 
209
	= (exA2cnt_2, idInner3_A_1);
210
	
211
212
tel
213
214
215
216
217
218
219
-- Entry action for state :A_A1
220
node A_A1_en(idInner3_A_1:int;
221
	enA1cnt_1:int;
222
	isInner:bool)
223
224
returns (idInner3_A:int;
225
	enA1cnt:int);
226
227
228
var 	idInner3_A_2:int;
229
	enA1cnt_2:int;
230
231
232
let
233
234
235
236
	-- set state as active 
237
	idInner3_A_2 
238
	= 1083;
239
	
240
241
	enA1cnt_2 
242
	= if (not isInner) then  enA1cnt_1  + 1
243
	 else enA1cnt_1;
244
	
245
246
	(idInner3_A, enA1cnt) 
247
	= (idInner3_A_2, enA1cnt_2);
248
	
249
250
tel
251
252
253
254
255
256
--During action for state :A_A1
257
node A_A1_du(duA1cnt_1:int)
258
259
returns (duA1cnt:int);
260
261
262
var 	duA1cnt_2:int;
263
264
265
let
266
267
268
269
	duA1cnt_2 
270
	=  duA1cnt_1  + 1;
271
	
272
273
	(duA1cnt) 
274
	= (duA1cnt_2);
275
	
276
277
tel
278
279
280
281
282
283
-- Exit action for state :A_A1
284
node A_A1_ex(exA1cnt_1:int;
285
	idInner3_A_1:int;
286
	isInner:bool)
287
288
returns (exA1cnt:int;
289
	idInner3_A:int);
290
291
292
var 	exA1cnt_2:int;
293
	idInner3_A_2:int;
294
295
296
let
297
298
299
300
	exA1cnt_2 
301
	= if (not isInner) then  exA1cnt_1  + 1
302
	 else exA1cnt_1;
303
	
304
305
	-- set state as inactive 
306
	idInner3_A_2
307
	 = if (not isInner) then 0 else idInner3_A_1;
308
309
310
	(exA1cnt, idInner3_A) 
311
	= (exA1cnt_2, idInner3_A_1);
312
	
313
314
tel
315
316
317
318
319
320
321
-- Entry action for state :Inner3_A
322
node Inner3_A_en(idInner3_A_1:int;
323
	idInner3_Inner3_1:int;
324
	enAcnt_1:int;
325
	enA1cnt_1:int;
326
	enA2cnt_1:int;
327
	enA3cnt_1:int;
328
	isInner:bool)
329
330
returns (idInner3_A:int;
331
	idInner3_Inner3:int;
332
	enAcnt:int;
333
	enA1cnt:int;
334
	enA2cnt:int;
335
	enA3cnt:int);
336
337
338
var 	idInner3_A_2, idInner3_A_3, idInner3_A_4, idInner3_A_5, idInner3_A_6, idInner3_A_7:int;
339
	idInner3_Inner3_2, idInner3_Inner3_3, idInner3_Inner3_4:int;
340
	enAcnt_2, enAcnt_3, enAcnt_4:int;
341
	enA1cnt_2, enA1cnt_3, enA1cnt_4, enA1cnt_5:int;
342
	enA2cnt_2, enA2cnt_3:int;
343
	enA3cnt_2, enA3cnt_3:int;
344
345
346
let
347
348
349
350
	-- set state as active 
351
	idInner3_Inner3_2 
352
	= 1082;
353
	
354
355
	enAcnt_2 
356
	= if (not isInner) then  enAcnt_1  + 1
357
	 else enAcnt_1;
358
	
359
360
	
361
-- transition trace :
362
	--POINT__To__A_A1_1
363
		(idInner3_A_2, enA1cnt_2) 
364
	= A_A1_en(idInner3_A_1, enA1cnt_1, false);
365
		
366
367
	(idInner3_A_3, idInner3_Inner3_3, enAcnt_3, enA1cnt_3) 
368
	= 
369
370
	if ( idInner3_A_1 = 0) then
371
372
	 (idInner3_A_2, idInner3_Inner3_2, enAcnt_2, enA1cnt_2)
373
374
	 else(idInner3_A_1, idInner3_Inner3_2, enAcnt_2, enA1cnt_1);
375
376
	
377
378
	(idInner3_A_4, enA2cnt_2) 
379
	= 
380
	if ( idInner3_A_1 = 1084) then
381
	A_A2_en(idInner3_A_1, enA2cnt_1, false)
382
	 else (idInner3_A_1, enA2cnt_1);
383
384
	
385
386
	(idInner3_A_5, enA3cnt_2) 
387
	= 
388
	if ( idInner3_A_1 = 1085) then
389
	A_A3_en(idInner3_A_1, enA3cnt_1, false)
390
	 else (idInner3_A_1, enA3cnt_1);
391
392
	
393
394
	(idInner3_A_6, enA1cnt_4) 
395
	= 
396
	if ( idInner3_A_1 = 1083) then
397
	A_A1_en(idInner3_A_1, enA1cnt_1, false)
398
	 else (idInner3_A_1, enA1cnt_1);
399
400
	
401
402
	(idInner3_A_7, idInner3_Inner3_4, enAcnt_4, enA1cnt_5, enA2cnt_3, enA3cnt_3) 
403
	= 
404
		 if ( idInner3_A_1 = 0) then 
405
		(idInner3_A_3, idInner3_Inner3_3, enAcnt_3, enA1cnt_3, enA2cnt_1, enA3cnt_1)
406
		 else
407
		 if ( idInner3_A_1 = 1084) then 
408
		(idInner3_A_4, idInner3_Inner3_3, enAcnt_3, enA1cnt_1, enA2cnt_2, enA3cnt_1)
409
		 else
410
		 if ( idInner3_A_1 = 1085) then 
411
		(idInner3_A_5, idInner3_Inner3_3, enAcnt_3, enA1cnt_1, enA2cnt_1, enA3cnt_2)
412
		 else
413
		 if ( idInner3_A_1 = 1083) then 
414
		(idInner3_A_6, idInner3_Inner3_3, enAcnt_3, enA1cnt_4, enA2cnt_1, enA3cnt_1)
415
		 else (idInner3_A_1, idInner3_Inner3_2, enAcnt_2, enA1cnt_1, enA2cnt_1, enA3cnt_1);
416
417
418
	(idInner3_A, idInner3_Inner3, enAcnt, enA1cnt, enA2cnt, enA3cnt) 
419
	= (idInner3_A_7, idInner3_Inner3_4, enAcnt_4, enA1cnt_5, enA2cnt_3, enA3cnt_3);
420
	
421
422
tel
423
424
425
426
427
428
--During action for state :Inner3_A
429
node Inner3_A_du(duAcnt_1:int)
430
431
returns (duAcnt:int);
432
433
434
var 	duAcnt_2:int;
435
436
437
let
438
439
440
441
	duAcnt_2 
442
	=  duAcnt_1  + 1;
443
	
444
445
	(duAcnt) 
446
	= (duAcnt_2);
447
	
448
449
tel
450
451
452
453
454
455
-- Exit action for state :Inner3_A
456
node Inner3_A_ex(exA2cnt_1:int;
457
	idInner3_A_1:int;
458
	exA3cnt_1:int;
459
	exA1cnt_1:int;
460
	exAcnt_1:int;
461
	idInner3_Inner3_1:int;
462
	isInner:bool)
463
464
returns (exA2cnt:int;
465
	idInner3_A:int;
466
	exA3cnt:int;
467
	exA1cnt:int;
468
	exAcnt:int;
469
	idInner3_Inner3:int);
470
471
472
var 	exA2cnt_2, exA2cnt_3:int;
473
	idInner3_A_2, idInner3_A_3, idInner3_A_4, idInner3_A_5, idInner3_A_6:int;
474
	exA3cnt_2, exA3cnt_3:int;
475
	exA1cnt_2, exA1cnt_3:int;
476
	exAcnt_2:int;
477
	idInner3_Inner3_2:int;
478
479
480
let
481
482
483
484
	
485
	(exA2cnt_2, idInner3_A_2) 
486
	= 
487
	if ( idInner3_A_1 = 1084) then
488
	A_A2_ex(exA2cnt_1, idInner3_A_1, false)
489
	 else (exA2cnt_1, idInner3_A_1);
490
491
	
492
493
	(exA3cnt_2, idInner3_A_3) 
494
	= 
495
	if ( idInner3_A_1 = 1085) then
496
	A_A3_ex(exA3cnt_1, idInner3_A_1, false)
497
	 else (exA3cnt_1, idInner3_A_1);
498
499
	
500
501
	(exA1cnt_2, idInner3_A_4) 
502
	= 
503
	if ( idInner3_A_1 = 1083) then
504
	A_A1_ex(exA1cnt_1, idInner3_A_1, false)
505
	 else (exA1cnt_1, idInner3_A_1);
506
507
	
508
509
	(exA2cnt_3, idInner3_A_5, exA3cnt_3, exA1cnt_3) 
510
	= 
511
		 if ( idInner3_A_1 = 1084) then 
512
		(exA2cnt_2, idInner3_A_2, exA3cnt_1, exA1cnt_1)
513
		 else
514
		 if ( idInner3_A_1 = 1085) then 
515
		(exA2cnt_1, idInner3_A_3, exA3cnt_2, exA1cnt_1)
516
		 else
517
		 if ( idInner3_A_1 = 1083) then 
518
		(exA2cnt_1, idInner3_A_4, exA3cnt_1, exA1cnt_2)
519
		 else (exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1);
520
521
522
	exAcnt_2 
523
	= if (not isInner) then  exAcnt_1  + 1
524
	 else exAcnt_1;
525
	
526
527
	-- set state as inactive 
528
	idInner3_Inner3_2
529
	 = if (not isInner) then 0 else idInner3_Inner3_1;
530
531
	idInner3_A_6 
532
	= 0;
533
	
534
535
	(exA2cnt, idInner3_A, exA3cnt, exA1cnt, exAcnt, idInner3_Inner3) 
536
	= (exA2cnt_3, idInner3_A_6, exA3cnt_3, exA1cnt_3, exAcnt_2, idInner3_Inner3_1);
537
	
538
539
tel
540
541
542
--***************************************************State :Inner3_A Automaton***************************************************
543
544
node Inner3_A_node(idInner3_A_1:int;
545
	enA1cnt_1:int;
546
	E:bool;
547
	duAcnt_1:int;
548
	exA1cnt_1:int;
549
	exA2cnt_1:int;
550
	exA3cnt_1:int;
551
	exAcnt_1:int;
552
	idInner3_Inner3_1:int;
553
	enA3cnt_1:int;
554
	enA2cnt_1:int;
555
	duA2cnt_1:int;
556
	duA3cnt_1:int;
557
	duA1cnt_1:int)
558
559
returns (idInner3_A:int;
560
	enA1cnt:int;
561
	exA1cnt:int;
562
	exA2cnt:int;
563
	exA3cnt:int;
564
	exAcnt:int;
565
	idInner3_Inner3:int;
566
	enA3cnt:int;
567
	enA2cnt:int;
568
	duA2cnt:int;
569
	duA3cnt:int;
570
	duA1cnt:int);
571
572
573
let
574
575
	 automaton inner3_a
576
577
	state POINTInner3_A:
578
	unless (idInner3_A_1=0) restart POINT__TO__A_A1_1
579
580
581
582
	unless true and E restart INNER3_A__TO__INNER3_INNER3JUNCTION1086_1
583
584
585
586
	unless (idInner3_A_1=1084) restart A_A2_IDL
587
588
	unless (idInner3_A_1=1085) restart A_A3_IDL
589
590
	unless (idInner3_A_1=1083) restart A_A1_IDL
591
592
	let
593
594
		(idInner3_A, enA1cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3, enA3cnt, enA2cnt, duA2cnt, duA3cnt, duA1cnt) 
595
	= (idInner3_A_1, enA1cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1, duA2cnt_1, duA3cnt_1, duA1cnt_1);
596
	
597
598
	tel
599
600
601
602
	state POINT__TO__A_A1_1:
603
604
	 var 	idInner3_A_2:int;
605
	enA1cnt_2:int;
606
	let
607
608
		-- transition trace :
609
	--POINT__To__A_A1_1
610
		(idInner3_A_2, enA1cnt_2) 
611
	= A_A1_en(idInner3_A_1, enA1cnt_1, false);
612
		
613
614
	(idInner3_A, enA1cnt) 
615
	=  (idInner3_A_2, enA1cnt_2);
616
617
	--add unused variables
618
	(duA1cnt, duA2cnt, duA3cnt, enA2cnt, enA3cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3) 
619
	= (duA1cnt_1, duA2cnt_1, duA3cnt_1, enA2cnt_1, enA3cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1);
620
	
621
622
	tel
623
624
	until true restart POINTInner3_A
625
626
627
628
	state INNER3_A__TO__INNER3_INNER3JUNCTION1086_1:
629
630
	 var 	idInner3_A_2, idInner3_A_3, idInner3_A_4, idInner3_A_5, idInner3_A_6, idInner3_A_7:int;
631
	enA1cnt_2:int;
632
	exA1cnt_2, exA1cnt_3, exA1cnt_4:int;
633
	exA2cnt_2, exA2cnt_3, exA2cnt_4:int;
634
	exA3cnt_2, exA3cnt_3, exA3cnt_4:int;
635
	exAcnt_2, exAcnt_3, exAcnt_4:int;
636
	idInner3_Inner3_2, idInner3_Inner3_3, idInner3_Inner3_4:int;
637
	enA3cnt_2:int;
638
	enA2cnt_2:int;
639
	let
640
641
		
642
643
-- transition trace :
644
	--Inner3_A__To__Junction1086_1, Junction1086__To__A_A3_1
645
		(exA2cnt_2, idInner3_A_2, exA3cnt_2, exA1cnt_2, exAcnt_2, idInner3_Inner3_2) 
646
	= 
647
		 if ((  duAcnt_1  mod 3=2 )) then 
648
		Inner3_A_ex(exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1, true)
649
		 else (exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1);
650
		
651
652
		(idInner3_A_3, enA3cnt_2) 
653
	= 
654
		 if ((  duAcnt_1  mod 3=2 )) then 
655
		A_A3_en(idInner3_A_2, enA3cnt_1, false)
656
		 else (idInner3_A_2, enA3cnt_1);
657
		
658
659
660
-- transition trace :
661
	--Inner3_A__To__Junction1086_1, Junction1086__To__A_A2_2
662
		(exA2cnt_3, idInner3_A_4, exA3cnt_3, exA1cnt_3, exAcnt_3, idInner3_Inner3_3) 
663
	= 
664
		 if ((  duAcnt_1  mod 3=1 )) then 
665
		Inner3_A_ex(exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1, true)
666
		 else (exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1);
667
		
668
669
		(idInner3_A_5, enA2cnt_2) 
670
	= 
671
		 if ((  duAcnt_1  mod 3=1 )) then 
672
		A_A2_en(idInner3_A_4, enA2cnt_1, false)
673
		 else (idInner3_A_4, enA2cnt_1);
674
		
675
676
677
-- transition trace :
678
	--Inner3_A__To__Junction1086_1, Junction1086__To__A_A1_3
679
		(exA2cnt_4, idInner3_A_6, exA3cnt_4, exA1cnt_4, exAcnt_4, idInner3_Inner3_4) 
680
	= 
681
		 if ((  duAcnt_1  mod 3=0 )) then 
682
		Inner3_A_ex(exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1, true)
683
		 else (exA2cnt_1, idInner3_A_1, exA3cnt_1, exA1cnt_1, exAcnt_1, idInner3_Inner3_1);
684
		
685
686
		(idInner3_A_7, enA1cnt_2) 
687
	= 
688
		 if ((  duAcnt_1  mod 3=0 )) then 
689
		A_A1_en(idInner3_A_6, enA1cnt_1, false)
690
		 else (idInner3_A_6, enA1cnt_1);
691
		
692
693
	(idInner3_A, enA1cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3, enA3cnt, enA2cnt) 
694
	= 
695
		 if ((  duAcnt_1  mod 3=2 )) then 
696
		(idInner3_A_3, enA1cnt_1, exA1cnt_2, exA2cnt_2, exA3cnt_2, exAcnt_2, idInner3_Inner3_2, enA3cnt_2, enA2cnt_1)
697
		 else
698
		 if ((  duAcnt_1  mod 3=1 )) then 
699
		(idInner3_A_5, enA1cnt_1, exA1cnt_3, exA2cnt_3, exA3cnt_3, exAcnt_3, idInner3_Inner3_3, enA3cnt_1, enA2cnt_2)
700
		 else
701
		 if ((  duAcnt_1  mod 3=0 )) then 
702
		(idInner3_A_7, enA1cnt_2, exA1cnt_4, exA2cnt_4, exA3cnt_4, exAcnt_4, idInner3_Inner3_4, enA3cnt_1, enA2cnt_1)
703
		 else (idInner3_A_1, enA1cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1);
704
705
	--add unused variables
706
	(duA1cnt, duA2cnt, duA3cnt) 
707
	= (duA1cnt_1, duA2cnt_1, duA3cnt_1);
708
	
709
710
	tel
711
712
	until true restart POINTInner3_A
713
714
715
716
	state A_A2_IDL:
717
718
	 var 	duA2cnt_2:int;
719
	let
720
721
		
722
	(duA2cnt_2) 
723
	= A_A2_du(duA2cnt_1);
724
725
		
726
727
728
	(idInner3_A, enA1cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3, enA3cnt, enA2cnt, duA2cnt) 
729
	= (idInner3_A_1, enA1cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1, duA2cnt_2);
730
	
731
	--add unused variables
732
	(duA1cnt, duA3cnt) 
733
	= (duA1cnt_1, duA3cnt_1);
734
	
735
736
	tel
737
738
	until true restart POINTInner3_A
739
740
741
742
	state A_A3_IDL:
743
744
	 var 	duA3cnt_2:int;
745
	let
746
747
		
748
	(duA3cnt_2) 
749
	= A_A3_du(duA3cnt_1);
750
751
		
752
753
754
	(idInner3_A, enA1cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3, enA3cnt, enA2cnt, duA2cnt, duA3cnt) 
755
	= (idInner3_A_1, enA1cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1, duA2cnt_1, duA3cnt_2);
756
	
757
	--add unused variables
758
	(duA1cnt) 
759
	= (duA1cnt_1);
760
	
761
762
	tel
763
764
	until true restart POINTInner3_A
765
766
767
768
	state A_A1_IDL:
769
770
	 var 	duA1cnt_2:int;
771
	let
772
773
		
774
	(duA1cnt_2) 
775
	= A_A1_du(duA1cnt_1);
776
777
		
778
779
780
	(idInner3_A, enA1cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt, idInner3_Inner3, enA3cnt, enA2cnt, duA2cnt, duA3cnt, duA1cnt) 
781
	= (idInner3_A_1, enA1cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1, duA2cnt_1, duA3cnt_1, duA1cnt_2);
782
	
783
784
	tel
785
786
	until true restart POINTInner3_A
787
788
789
790
tel
791
792
793
--***************************************************State :Inner3_Inner3 Automaton***************************************************
794
795
node Inner3_Inner3_node(idInner3_Inner3_1:int;
796
	enA1cnt_1:int;
797
	enA2cnt_1:int;
798
	enA3cnt_1:int;
799
	enAcnt_1:int;
800
	idInner3_A_1:int;
801
	duAcnt_1:int;
802
	E:bool;
803
	duA1cnt_1:int;
804
	duA2cnt_1:int;
805
	duA3cnt_1:int;
806
	exA1cnt_1:int;
807
	exA2cnt_1:int;
808
	exA3cnt_1:int;
809
	exAcnt_1:int)
810
811
returns (idInner3_Inner3:int;
812
	enA1cnt:int;
813
	enA2cnt:int;
814
	enA3cnt:int;
815
	enAcnt:int;
816
	idInner3_A:int;
817
	duAcnt:int;
818
	duA1cnt:int;
819
	duA2cnt:int;
820
	duA3cnt:int;
821
	exA1cnt:int;
822
	exA2cnt:int;
823
	exA3cnt:int;
824
	exAcnt:int);
825
826
827
let
828
829
	 automaton inner3_inner3
830
831
	state POINTInner3_Inner3:
832
	unless (idInner3_Inner3_1=0) restart POINT__TO__INNER3_A_1
833
834
835
836
	unless (idInner3_Inner3_1=1082) restart INNER3_A_IDL
837
838
	let
839
840
		(idInner3_Inner3, enA1cnt, enA2cnt, enA3cnt, enAcnt, idInner3_A, duAcnt, duA1cnt, duA2cnt, duA3cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt) 
841
	= (idInner3_Inner3_1, enA1cnt_1, enA2cnt_1, enA3cnt_1, enAcnt_1, idInner3_A_1, duAcnt_1, duA1cnt_1, duA2cnt_1, duA3cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1);
842
	
843
844
	tel
845
846
847
848
	state POINT__TO__INNER3_A_1:
849
850
	 var 	idInner3_Inner3_2:int;
851
	enA1cnt_2:int;
852
	enA2cnt_2:int;
853
	enA3cnt_2:int;
854
	enAcnt_2:int;
855
	idInner3_A_2:int;
856
	let
857
858
		-- transition trace :
859
	--POINT__To__Inner3_A_1
860
		(idInner3_A_2, idInner3_Inner3_2, enAcnt_2, enA1cnt_2, enA2cnt_2, enA3cnt_2) 
861
	= Inner3_A_en(idInner3_A_1, idInner3_Inner3_1, enAcnt_1, enA1cnt_1, enA2cnt_1, enA3cnt_1, false);
862
		
863
864
	(idInner3_Inner3, enA1cnt, enA2cnt, enA3cnt, enAcnt, idInner3_A) 
865
	=  (idInner3_Inner3_2, enA1cnt_2, enA2cnt_2, enA3cnt_2, enAcnt_2, idInner3_A_2);
866
867
	--add unused variables
868
	(duA1cnt, duA2cnt, duA3cnt, duAcnt, exA1cnt, exA2cnt, exA3cnt, exAcnt) 
869
	= (duA1cnt_1, duA2cnt_1, duA3cnt_1, duAcnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1);
870
	
871
872
	tel
873
874
	until true restart POINTInner3_Inner3
875
876
877
878
	state INNER3_A_IDL:
879
880
	 var 	idInner3_Inner3_2:int;
881
	enA1cnt_2:int;
882
	enA2cnt_2:int;
883
	enA3cnt_2:int;
884
	idInner3_A_2:int;
885
	duAcnt_2:int;
886
	duA1cnt_2:int;
887
	duA2cnt_2:int;
888
	duA3cnt_2:int;
889
	exA1cnt_2:int;
890
	exA2cnt_2:int;
891
	exA3cnt_2:int;
892
	exAcnt_2:int;
893
	let
894
895
		
896
	(duAcnt_2) 
897
	= Inner3_A_du(duAcnt_1);
898
899
		
900
901
	(idInner3_A_2, enA1cnt_2, exA1cnt_2, exA2cnt_2, exA3cnt_2, exAcnt_2, idInner3_Inner3_2, enA3cnt_2, enA2cnt_2, duA2cnt_2, duA3cnt_2, duA1cnt_2) 
902
	= Inner3_A_node(idInner3_A_1, enA1cnt_1, E, duAcnt_2, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1, idInner3_Inner3_1, enA3cnt_1, enA2cnt_1, duA2cnt_1, duA3cnt_1, duA1cnt_1);
903
904
		
905
906
907
	(idInner3_Inner3, enA1cnt, enA2cnt, enA3cnt, enAcnt, idInner3_A, duAcnt, duA1cnt, duA2cnt, duA3cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt) 
908
	= (idInner3_Inner3_2, enA1cnt_2, enA2cnt_2, enA3cnt_2, enAcnt_1, idInner3_A_2, duAcnt_2, duA1cnt_2, duA2cnt_2, duA3cnt_2, exA1cnt_2, exA2cnt_2, exA3cnt_2, exAcnt_2);
909
	
910
911
	tel
912
913
	until true restart POINTInner3_Inner3
914
915
916
917
tel
918
919
920
--***************************************************State :Inner3_Inner3 Automaton***************************************************
921
922
node Inner3_Inner3(E:bool)
923
924
returns (exAcnt:int;
925
	enAcnt:int;
926
	duAcnt:int;
927
	enA1cnt:int;
928
	duA1cnt:int;
929
	exA1cnt:int;
930
	enA2cnt:int;
931
	duA2cnt:int;
932
	exA2cnt:int;
933
	enA3cnt:int;
934
	duA3cnt:int;
935
	exA3cnt:int);
936
937
938
var exAcnt_1: int;
939
940
	enAcnt_1: int;
941
942
	duAcnt_1: int;
943
944
	enA1cnt_1: int;
945
946
	duA1cnt_1: int;
947
948
	exA1cnt_1: int;
949
950
	enA2cnt_1: int;
951
952
	duA2cnt_1: int;
953
954
	exA2cnt_1: int;
955
956
	enA3cnt_1: int;
957
958
	duA3cnt_1: int;
959
960
	exA3cnt_1: int;
961
962
	idInner3_Inner3, idInner3_Inner3_1: int;
963
964
	idInner3_A, idInner3_A_1: int;
965
966
	let
967
968
	exAcnt_1 = 0 -> pre exAcnt;
969
970
	enAcnt_1 = 0 -> pre enAcnt;
971
972
	duAcnt_1 = 0 -> pre duAcnt;
973
974
	enA1cnt_1 = 0 -> pre enA1cnt;
975
976
	duA1cnt_1 = 0 -> pre duA1cnt;
977
978
	exA1cnt_1 = 0 -> pre exA1cnt;
979
980
	enA2cnt_1 = 0 -> pre enA2cnt;
981
982
	duA2cnt_1 = 0 -> pre duA2cnt;
983
984
	exA2cnt_1 = 0 -> pre exA2cnt;
985
986
	enA3cnt_1 = 0 -> pre enA3cnt;
987
988
	duA3cnt_1 = 0 -> pre duA3cnt;
989
990
	exA3cnt_1 = 0 -> pre exA3cnt;
991
992
	idInner3_Inner3_1 = 0 -> pre idInner3_Inner3;
993
994
	idInner3_A_1 = 0 -> pre idInner3_A;
995
996
	
997
998
999
1000
	(idInner3_Inner3, enA1cnt, enA2cnt, enA3cnt, enAcnt, idInner3_A, duAcnt, duA1cnt, duA2cnt, duA3cnt, exA1cnt, exA2cnt, exA3cnt, exAcnt)
1001
	 = 
1002
1003
	 if E then Inner3_Inner3_node(idInner3_Inner3_1, enA1cnt_1, enA2cnt_1, enA3cnt_1, enAcnt_1, idInner3_A_1, duAcnt_1, E, duA1cnt_1, duA2cnt_1, duA3cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1)
1004
1005
	 else (idInner3_Inner3_1, enA1cnt_1, enA2cnt_1, enA3cnt_1, enAcnt_1, idInner3_A_1, duAcnt_1, duA1cnt_1, duA2cnt_1, duA3cnt_1, exA1cnt_1, exA2cnt_1, exA3cnt_1, exAcnt_1);
1006
1007
	
1008
1009
1010
--unused outputs
1011
	
1012
1013
tel
1014
1015
1016
1017
node Inner3 (E_1_1 : real)
1018
returns (exAcnt_1_1 : int;
1019
	enAcnt_2_1 : int;
1020
	duAcnt_3_1 : int;
1021
	enA1cnt_4_1 : int;
1022
	duA1cnt_5_1 : int;
1023
	exA1cnt_6_1 : int;
1024
	enA2cnt_7_1 : int;
1025
	duA2cnt_8_1 : int;
1026
	exA2cnt_9_1 : int;
1027
	enA3cnt_10_1 : int;
1028
	duA3cnt_11_1 : int;
1029
	exA3cnt_12_1 : int); 
1030
var
1031
	Inner3_1_1 : int; Inner3_2_1 : int; Inner3_3_1 : int; Inner3_4_1 : int; Inner3_5_1 : int; Inner3_6_1 : int; Inner3_7_1 : int; Inner3_8_1 : int; Inner3_9_1 : int; Inner3_10_1 : int; Inner3_11_1 : int; Inner3_12_1 : int;
1032
	i_virtual_local : real;
1033
	Inner3E_1_1_event: bool;
1034
let 
1035
	Inner3E_1_1_event = false -> ((pre(E_1_1) > 0.0 and E_1_1 <= 0.0) or (pre(E_1_1) <= 0.0 and E_1_1 > 0.0));
1036
	(Inner3_1_1, Inner3_2_1, Inner3_3_1, Inner3_4_1, Inner3_5_1, Inner3_6_1, Inner3_7_1, Inner3_8_1, Inner3_9_1, Inner3_10_1, Inner3_11_1, Inner3_12_1) =  Inner3_Inner3(Inner3E_1_1_event);
1037
	exAcnt_1_1 = Inner3_1_1;
1038
	enAcnt_2_1 = Inner3_2_1;
1039
	duAcnt_3_1 = Inner3_3_1;
1040
	enA1cnt_4_1 = Inner3_4_1;
1041
	duA1cnt_5_1 = Inner3_5_1;
1042
	exA1cnt_6_1 = Inner3_6_1;
1043
	enA2cnt_7_1 = Inner3_7_1;
1044
	duA2cnt_8_1 = Inner3_8_1;
1045
	exA2cnt_9_1 = Inner3_9_1;
1046
	enA3cnt_10_1 = Inner3_10_1;
1047
	duA3cnt_11_1 = Inner3_11_1;
1048
	exA3cnt_12_1 = Inner3_12_1;
1049
	i_virtual_local= 0.0 -> 1.0;
1050
tel