Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1False / Junctions1False.lus @ 79ef5fc5

History | View | Annotate | Download (12.6 KB)

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