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
-- 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
1051