Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / SAFE / ccp09.lus @ b8dc00eb

History | View | Annotate | Download (44.2 KB)

1

    
2

    
3
--@ ensures OK;
4
node top(onOff: bool; 
5
      decelSet: bool; 
6
      accelResume: bool; 
7
      cancel: bool; 
8
      brakePedal: bool; 
9
      carGear: int ; 
10
      carSpeed: real; 
11
      validInputs: bool) returns (OK: bool);
12

    
13
var
14
   mode: int ; 
15
      cruiseThrottle: real; 
16
      desiredSpeed: real; 
17
      VRP1: bool; 
18
      VRP2: bool; 
19
      CP8a: bool; 
20
      VRP4: bool; 
21
      SP4: bool; 
22
      SP5: bool; 
23
      SP6: bool; 
24
      SP7: bool; 
25
      SP3b: bool; 
26
      SP3c: bool; 
27
      SP3: bool; 
28
      SP3a: bool; 
29
      SP2: bool; 
30
      SP1: bool; 
31
      SP8: bool; 
32
      SP9: bool; 
33
      SP10: bool; 
34
      SP11: bool;
35
   zz0: bool; 
36
   zz1: bool; 
37
   zz2: real; 
38
   zz3: bool; 
39
   zz4: bool; 
40
   zz5: real; 
41
   zz6: int ; 
42
   zz7: int ; 
43
   zz8: int ; 
44
   zz9: int ; 
45
   zz10: int ; 
46
   zz11: int ; 
47
   zz12: int ; 
48
   zz13: int ; 
49
   zz14: int ; 
50
   zz15: bool; 
51
   zz16: int ; 
52
   zz17: int ; 
53
   zz18: int ; 
54
   zz19: bool; 
55
   zz20: int ; 
56
   zz21: int ; 
57
   zz22: int ; 
58
   zz23: bool; 
59
   zz24: bool; 
60
   zz25: int ; 
61
   zz26: bool; 
62
   zz27: bool; 
63
   zz28: int ; 
64
   zz29: int ; 
65
   zz30: bool; 
66
   zz31: bool; 
67
   zz32: int ; 
68
   zz33: bool; 
69
   zz34: int ; 
70
   zz35: int ; 
71
   zz36: bool; 
72
   zz37: bool; 
73
   zz38: int ; 
74
   zz39: bool; 
75
   zz40: int ; 
76
   zz41: int ; 
77
   zz42: bool; 
78
   zz43: bool; 
79
   zz44: int ; 
80
   zz45: int ; 
81
   zz46: int ; 
82
   zz47: bool; 
83
   zz48: bool; 
84
   zz49: int ; 
85
   zz50: int ; 
86
   zz51: int ; 
87
   zz52: bool; 
88
   zz53: int ; 
89
   zz54: int ; 
90
   zz55: int ; 
91
   zz56: bool; 
92
   zz57: bool; 
93
   zz58: int ; 
94
   zz59: int ; 
95
   zz60: int ; 
96
   zz61: int ; 
97
   zz62: int ; 
98
   zz63: int ; 
99
   zz64: bool; 
100
   zz65: bool; 
101
   zz66: int ; 
102
   zz67: int ; 
103
   zz68: int ; 
104
   zz69: int ; 
105
   zz70: int ; 
106
   zz71: int ; 
107
   zz72: bool; 
108
   zz73: bool; 
109
   zz74: int ; 
110
   zz75: int ; 
111
   zz76: int ; 
112
   zz77: int ; 
113
   zz78: int ; 
114
   zz79: int ; 
115
   zz80: int ; 
116
   zz81: int ; 
117
   zz82: bool; 
118
   zz83: int ; 
119
   zz84: int ; 
120
   zz85: int ; 
121
   zz86: int ; 
122
   zz87: bool; 
123
   zz88: bool; 
124
   zz89: int ; 
125
   zz90: bool; 
126
   zz91: int ; 
127
   zz92: int ; 
128
   zz93: bool; 
129
   zz94: bool; 
130
   zz95: int ; 
131
   zz96: bool; 
132
   zz97: int ; 
133
   zz98: int ; 
134
   zz99: bool; 
135
   zz100: bool; 
136
   zz101: int ; 
137
   zz102: int ; 
138
   zz103: int ; 
139
   zz104: bool; 
140
   zz105: bool; 
141
   zz106: int ; 
142
   zz107: bool; 
143
   zz108: int ; 
144
   zz109: int ; 
145
   zz110: int ; 
146
   zz111: int ; 
147
   zz112: bool; 
148
   zz113: int ; 
149
   zz114: int ; 
150
   zz115: int ; 
151
   zz116: bool; 
152
   zz117: bool; 
153
   zz118: int ; 
154
   zz119: int ; 
155
   zz120: int ; 
156
   zz121: int ; 
157
   zz122: int ; 
158
   zz123: int ; 
159
   zz124: int ; 
160
   zz125: int ; 
161
   zz126: int ; 
162
   zz127: int ; 
163
   zz128: bool; 
164
   zz129: int ; 
165
   zz130: int ; 
166
   zz131: int ; 
167
   zz132: int ; 
168
   zz133: bool; 
169
   zz134: int ; 
170
   zz135: int ; 
171
   zz136: int ; 
172
   zz137: int ; 
173
   zz138: bool; 
174
   zz139: bool; 
175
   zz140: int ; 
176
   zz141: bool; 
177
   zz142: int ; 
178
   zz143: int ; 
179
   zz144: bool; 
180
   zz145: bool; 
181
   zz146: int ; 
182
   zz147: int ; 
183
   zz148: int ; 
184
   zz149: int ; 
185
   zz150: int ; 
186
   zz151: bool; 
187
   zz152: bool; 
188
   zz153: int ; 
189
   zz154: int ; 
190
   zz155: bool; 
191
   zz156: int ; 
192
   zz157: int ; 
193
   zz158: bool; 
194
   zz159: int ; 
195
   zz160: int ; 
196
   zz161: int ; 
197
   zz162: bool; 
198
   zz163: bool; 
199
   zz164: bool; 
200
   zz165: bool; 
201
   zz166: int ; 
202
   zz167: int ; 
203
   zz168: int ; 
204
   zz169: int ; 
205
   zz170: int ; 
206
   zz171: bool; 
207
   zz172: int ; 
208
   zz173: int ; 
209
   zz174: int ; 
210
   zz175: int ; 
211
   zz176: int ; 
212
   zz177: bool; 
213
   zz178: bool; 
214
   zz179: bool; 
215
   zz180: bool; 
216
   zz181: bool; 
217
   zz182: bool; 
218
   zz183: bool; 
219
   zz184: bool; 
220
   zz185: bool; 
221
   zz186: bool; 
222
   zz187: bool; 
223
   zz188: bool; 
224
   zz189: bool; 
225
   zz190: real; 
226
   zz191: bool; 
227
   zz192: bool; 
228
   zz193: bool; 
229
   zz194: bool; 
230
   zz195: bool; 
231
   zz196: bool; 
232
   zz197: bool; 
233
   zz198: bool; 
234
   zz199: bool; 
235
   zz200: bool; 
236
   zz201: bool; 
237
   zz202: bool; 
238
   zz203: bool; 
239
   zz204: real; 
240
   zz205: real; 
241
   zz206: bool; 
242
   zz207: bool; 
243
   zz208: bool; 
244
   zz209: bool; 
245
   zz210: bool; 
246
   zz211: real; 
247
   zz212: bool; 
248
   zz213: bool; 
249
   zz214: bool; 
250
   zz215: bool; 
251
   zz216: bool; 
252
   zz217: bool; 
253
   zz218: real; 
254
   zz219: real; 
255
   zz220: real; 
256
   zz221: real; 
257
   zz222: real; 
258
   zz223: real; 
259
   zz224: real; 
260
   zz225: real; 
261
   zz226: real; 
262
   zz227: real; 
263
   zz228: real; 
264
   zz229: real; 
265
   zz230: real; 
266
   zz231: bool; 
267
   zz232: bool; 
268
   zz233: bool; 
269
   zz234: bool; 
270
   zz235: bool; 
271
   zz236: bool; 
272
   zz237: bool; 
273
   zz238: bool; 
274
   zz239: bool;
275

    
276
let 
277
   zz166 = 
278
      (if (0 >= zz168)
279
         then 0
280
         else zz168);
281

    
282
   zz168 = 
283
      (if accelResume
284
         then zz167
285
         else 0);
286

    
287
   zz169 = (0 -> (pre zz170));
288

    
289
   zz172 = 
290
      (if (0 >= zz174)
291
         then 0
292
         else zz174);
293

    
294
   zz174 = 
295
      (if decelSet
296
         then zz173
297
         else 0);
298

    
299
   zz175 = (0 -> (pre zz176));
300

    
301
   zz156 = (0 -> (pre zz161));
302

    
303
   zz157 = (0 -> (pre mode));
304

    
305
   zz159 = 
306
      (if SP3c
307
         then 1
308
         else 0);
309

    
310
   (* Beginning transition segment: trans20
311
      <fired> is true if the following are true: 
312
         1. the previous transition guard was true, 
313
         2. the source node for the transition is active, 
314
         3. the condition for the transition to fire is true, and 
315
         4. no higher-priority transition has completed (not <complete>) *)
316
   zz93 = ((zz91 = 8) and 
317
      (((
318
      (if ((zz185 = true) = false)
319
         then 0
320
         else 1) <> 0) and 
321
      (
322
      (if ((zz186 = true) = false)
323
         then 0
324
         else 1) <> 0)) and 
325
      (not zz88)));
326

    
327
   (* Beginning transition segment: trans19
328
      <fired> is true if the following are true: 
329
         1. the previous transition guard was true, 
330
         2. the source node for the transition is active, 
331
         3. the condition for the transition to fire is true, and 
332
         4. no higher-priority transition has completed (not <complete>) *)
333
   zz99 = ((zz97 = 8) and 
334
      (((
335
      (if ((zz180 = true) = false)
336
         then 0
337
         else 1) <> 0) and 
338
      (
339
      (if ((zz186 = true) = false)
340
         then 0
341
         else 1) <> 0)) and 
342
      (not zz94)));
343

    
344
   (* Beginning transition segment: trans22
345
      <fired> is true if the following are true: 
346
         1. the previous transition guard was true, 
347
         2. the source node for the transition is active, 
348
         3. the condition for the transition to fire is true, and 
349
         4. no higher-priority transition has completed (not <complete>) *)
350
   zz104 = ((zz102 = 7) and 
351
      (((
352
      (if ((zz185 = true) = false)
353
         then 0
354
         else 1) <> 0) and 
355
      (
356
      (if ((zz186 = true) = false)
357
         then 0
358
         else 1) <> 0)) and 
359
      (not zz100)));
360

    
361
   (* Beginning transition segment: trans24
362
      <fired> is true if the following are true: 
363
         1. the previous transition guard was true, 
364
         2. the source node for the transition is active, 
365
         3. the condition for the transition to fire is true, and 
366
         4. no higher-priority transition has completed (not <complete>) *)
367
   zz24 = ((zz108 = 4) and 
368
      (
369
      (if ((zz185 = true) = false)
370
         then 0
371
         else 1) <> 0));
372

    
373
   (* Beginning transition segment: trans14
374
      <fired> is true if the following are true: 
375
         1. the previous transition guard was true, 
376
         2. the source node for the transition is active, 
377
         3. the condition for the transition to fire is true, and 
378
         4. no higher-priority transition has completed (not <complete>) *)
379
   zz30 = ((zz28 = 4) and 
380
      ((
381
      (if ((zz171 = true) = false)
382
         then 0
383
         else 1) <> 0) and 
384
      (not zz24)));
385

    
386
   (* Beginning transition segment: trans15
387
      <fired> is true if the following are true: 
388
         1. the previous transition guard was true, 
389
         2. the source node for the transition is active, 
390
         3. the condition for the transition to fire is true, and 
391
         4. no higher-priority transition has completed (not <complete>) *)
392
   zz36 = ((zz34 = 4) and 
393
      ((
394
      (if ((zz177 = true) = false)
395
         then 0
396
         else 1) <> 0) and 
397
      (not zz31)));
398

    
399
   (* Beginning transition segment: trans17
400
      <fired> is true if the following are true: 
401
         1. the previous transition guard was true, 
402
         2. the source node for the transition is active, 
403
         3. the condition for the transition to fire is true, and 
404
         4. no higher-priority transition has completed (not <complete>) *)
405
   zz42 = ((zz40 = 6) and 
406
      ((
407
      (if ((zz177 = false) = false)
408
         then 0
409
         else 1) <> 0) and 
410
      (not zz37)));
411

    
412
   (* Beginning transition segment: trans16
413
      <fired> is true if the following are true: 
414
         1. the previous transition guard was true, 
415
         2. the source node for the transition is active, 
416
         3. the condition for the transition to fire is true, and 
417
         4. no higher-priority transition has completed (not <complete>) *)
418
   zz47 = ((zz45 = 5) and 
419
      ((
420
      (if ((zz171 = false) = false)
421
         then 0
422
         else 1) <> 0) and 
423
      (not zz43)));
424

    
425
   zz57 = ((zz58 = 4) or 
426
      ((zz58 = 5) or 
427
      (zz58 = 6)));
428

    
429
   zz63 = 
430
      (if (not 
431
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
432
         ((zz101 >= 3) and 
433
         (zz101 <= 6)))
434
         then 
435
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
436
               3
437
         else zz101);
438

    
439
   (* Beginning transition segment: trans18
440
      <fired> is true if the following are true: 
441
         1. the previous transition guard was true, 
442
         2. the source node for the transition is active, 
443
         3. the condition for the transition to fire is true, and 
444
         4. no higher-priority transition has completed (not <complete>) *)
445
   zz64 = ((not 
446
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
447
      ((zz101 >= 3) and 
448
      (zz101 <= 6))) and 
449

    
450
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
451
      ((zz63 >= 3) and 
452
      (zz63 <= 6)));
453

    
454
   (* Beginning transition segment: trans12
455
      <fired> is true if the following are true: 
456
         1. the previous transition guard was true, 
457
         2. the source node for the transition is active, 
458
         3. the condition for the transition to fire is true, and 
459
         4. no higher-priority transition has completed (not <complete>) *)
460
   zz116 = ((not 
461
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
462
      ((zz146 >= 2) and 
463
      (zz146 <= 8))) and 
464

    
465
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
466
      ((zz115 >= 2) and 
467
      (zz115 <= 8)));
468

    
469
   zz120 = 
470
      (if (zz142 = 1)
471
         then 
472
               (* <Exit state> path: Off maps to field: __root and value: 0 *)
473
               0
474
         else zz142);
475

    
476
   zz137 = 
477
      (if 
478
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
479
         ((zz156 >= 2) and 
480
         (zz156 <= 8))
481
         then 
482
               (* <Exit state> path: On maps to field: __root and value: 0 *)
483
               0
484
         else zz136);
485

    
486
   SP3c = true;
487

    
488
   zz171 = (zz170 = 20);
489

    
490
   (* Condition actions for transition segment: trans22: NONE
491
      Transition action(s) for transition: trans22
492
      <complete> is true if either: 
493
         1. this transition has completed, or 
494
         2. a higher-priority transition has already completed 
495
       *)
496
   zz105 = (zz104 or 
497
      zz100);
498

    
499
   zz127 = 
500
      (if (zz156 = 4)
501
         then 
502
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
503
               3
504
         else zz156);
505

    
506
   zz204 = cruiseThrottle;
507

    
508
   zz165 = (mode = 6);
509

    
510
   SP7 = ((not zz165) or 
511
      zz208);
512

    
513
   zz136 = 
514
      (if 
515
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
516
         ((zz156 >= 2) and 
517
         (zz156 <= 8))
518
         then zz123
519
         else zz135);
520

    
521
   (* Exit action(s) for transition: On_Init -> On_Active *)
522
   zz106 = 
523
      (if zz104
524
         then zz60
525
         else zz102);
526

    
527
   zz173 = (zz175 + 1);
528

    
529
   zz81 = 
530
      (if (zz147 = 4)
531
         then 
532
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
533
               3
534
         else zz147);
535

    
536
   zz181 = (carGear = 3);
537

    
538
   zz79 = 
539
      (if (zz84 = 6)
540
         then 
541
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
542
               3
543
         else zz84);
544

    
545
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
546
   zz38 = 
547
      (if zz36
548
         then zz14
549
         else zz34);
550

    
551
   (* Exit action(s) for transition: On -> On_Init: NONE
552
      Transition action(s) for transition: On -> On_Init: NONE
553
      Entry action(s) for transition: On -> On_Init *)
554
   zz119 = 
555
      (if zz116
556
         then zz114
557
         else zz143);
558
   (* Transition segment: trans12 complete. *)
559

    
560
   zz78 = 
561
      (if (not (zz89 = 8))
562
         then 3
563
         else zz148);
564

    
565
   zz15 = 
566
      (if (zz34 = 4)
567
         then false
568
         else zz33);
569

    
570
   zz83 = 
571
      (if 
572
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
573
         ((zz147 >= 3) and 
574
         (zz147 <= 6))
575
         then zz81
576
         else zz147);
577

    
578
   zz54 = 
579
      (if (not (zz55 = 4))
580
         then 4
581
         else zz103);
582

    
583
   zz192 = (zz211 > desiredSpeed);
584

    
585
   zz16 = 
586
      (if (not (zz32 = 5))
587
         then 
588
               (* <Enter state> path: On.Active.Increase maps to field: __root and value: 5 *)
589
               5
590
         else zz32);
591

    
592
   zz158 = (false -> (pre zz162));
593

    
594
   SP3a = ((not (not zz163)) or 
595
      (not zz199));
596

    
597
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
598
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
599
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
600
   zz67 = 
601
      (if zz64
602
         then zz62
603
         else zz98);
604
   (* Transition segment: trans18 complete. *)
605

    
606
   (* Condition actions for transition segment: trans17: NONE
607
      Transition action(s) for transition: trans17
608
      <complete> is true if either: 
609
         1. this transition has completed, or 
610
         2. a higher-priority transition has already completed 
611
       *)
612
   zz43 = (zz42 or 
613
      zz37);
614

    
615
   zz76 = 
616
      (if (zz91 = 8)
617
         then 
618
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
619
               2
620
         else zz91);
621

    
622
   zz80 = 
623
      (if (zz83 = 5)
624
         then 
625
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
626
               3
627
         else zz83);
628

    
629
   zz198 = (zz197 or 
630
      zz196);
631

    
632
   zz193 = (desiredSpeed <> 0.0);
633

    
634
   SP1 = ((not (not zz186)) or 
635
      zz187);
636

    
637
   zz231 = (cruiseThrottle <= 100.0);
638

    
639
   zz123 = 
640
      (if (zz135 = 8)
641
         then 
642
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
643
               2
644
         else zz135);
645

    
646
   zz19 = 
647
      (if (zz28 = 4)
648
         then false
649
         else zz27);
650

    
651
   (* Condition actions for transition segment: trans20: NONE
652
      Transition action(s) for transition: trans20
653
      <complete> is true if either: 
654
         1. this transition has completed, or 
655
         2. a higher-priority transition has already completed 
656
       *)
657
   zz94 = (zz93 or 
658
      zz88);
659

    
660
   cruiseThrottle = 
661
      (if zz201
662
         then zz226
663
         else 0.0);
664

    
665
   zz86 = 
666
      (if 
667
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
668
         ((zz147 >= 3) and 
669
         (zz147 <= 6))
670
         then 
671
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
672
               2
673
         else zz85);
674

    
675
   VRP1 = (zz232 and 
676
      zz231);
677

    
678
   zz131 = 
679
      (if 
680
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
681
         ((zz156 >= 3) and 
682
         (zz156 <= 6))
683
         then zz125
684
         else zz130);
685

    
686
   zz235 = (desiredSpeed < 0.0);
687

    
688
   SP9 = ((not zz214) or 
689
      zz215);
690

    
691
   zz138 = 
692
      (if 
693
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
694
         ((zz156 >= 2) and 
695
         (zz156 <= 8))
696
         then zz133
697
         else zz158);
698

    
699
   zz65 = ((zz66 = 4) or 
700
      ((zz66 = 5) or 
701
      (zz66 = 6)));
702

    
703
   zz194 = (desiredSpeed >= 15.0);
704

    
705
   zz197 = (mode = 1);
706

    
707
   OK = (not zz237);
708

    
709
   zz6 = 
710
      (if (not (zz49 = 4))
711
         then 
712
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
713
               4
714
         else zz49);
715

    
716
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
717
   zz33 = 
718
      (if zz30
719
         then zz19
720
         else zz27);
721

    
722
   zz134 = 
723
      (if 
724
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
725
         ((zz156 >= 2) and 
726
         (zz156 <= 8))
727
         then zz132
728
         else zz156);
729

    
730
   zz61 = 
731
      (if (not (zz63 = 4))
732
         then 
733
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
734
               4
735
         else zz63);
736

    
737
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
738
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
739
   zz34 = 
740
      (if zz30
741
         then zz16
742
         else zz32);
743
   (* Transition segment: trans14 complete. *)
744

    
745
   (* Exit action(s) for transition: On -> Off *)
746
   zz141 = 
747
      (if zz139
748
         then zz138
749
         else zz158);
750

    
751
   (* Beginning transition segment: trans13
752
      <fired> is true if the following are true: 
753
         1. the previous transition guard was true, 
754
         2. the source node for the transition is active, 
755
         3. the condition for the transition to fire is true, and 
756
         4. no higher-priority transition has completed (not <complete>) *)
757
   zz139 = (
758
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
759
      ((zz156 >= 2) and 
760
      (zz156 <= 8)) and 
761
      (not onOff));
762

    
763
   zz178 = accelResume;
764

    
765
   zz234 = (desiredSpeed >= 0.0);
766

    
767
   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE
768
      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
769
   zz45 = 
770
      (if zz42
771
         then zz9
772
         else zz44);
773
   (* Transition segment: trans17 complete. *)
774

    
775
   zz121 = 
776
      (if (not (zz140 = 1))
777
         then 
778
               (* <Enter state> path: Off maps to field: __root and value: 1 *)
779
               1
780
         else zz140);
781

    
782
   zz184 = (true -> (pre zz183));
783

    
784
   (* Exit action(s) for transition: On -> On_Init: NONE
785
      Transition action(s) for transition: On -> On_Init: NONE
786
      Entry action(s) for transition: On -> On_Init *)
787
   zz118 = 
788
      (if zz116
789
         then zz113
790
         else zz115);
791
   (* Transition segment: trans12 complete. *)
792

    
793
   zz191 = (zz189 and 
794
      zz188);
795

    
796
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
797
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
798
   zz41 = 
799
      (if zz36
800
         then zz13
801
         else zz35);
802
   (* Transition segment: trans15 complete. *)
803

    
804
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
805
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
806
   zz35 = 
807
      (if zz30
808
         then zz17
809
         else zz29);
810
   (* Transition segment: trans14 complete. *)
811

    
812
   zz208 = (zz211 >= desiredSpeed);
813

    
814
   zz200 = (zz223 = 0.0);
815

    
816
   zz154 = 
817
      (if (not (zz156 = 1))
818
         then 1
819
         else zz157);
820

    
821
   zz73 = ((zz74 = 4) or 
822
      ((zz74 = 5) or 
823
      (zz74 = 6)));
824

    
825
   (* Transition action(s) for transition: On -> Off: NONE
826
      Entry action(s) for transition: On -> Off *)
827
   zz142 = 
828
      (if zz139
829
         then zz121
830
         else zz140);
831
   (* Transition segment: trans13 complete. *)
832

    
833
   zz124 = 
834
      (if (zz134 = 7)
835
         then 
836
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
837
               2
838
         else zz134);
839

    
840
   VRP4 = ((zz238 or 
841
      zz195) or 
842
      zz239);
843

    
844
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
845
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
846
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
847
   zz75 = 
848
      (if zz72
849
         then zz70
850
         else zz92);
851
   (* Transition segment: trans18 complete. *)
852

    
853
   zz233 = (desiredSpeed <= 100.0);
854

    
855
   zz223 = 
856
      (if zz217
857
         then zz2
858
         else zz218);
859

    
860
   zz185 = ((not zz184) and 
861
      zz183);
862

    
863
   zz180 = ((not zz179) and 
864
      zz178);
865

    
866
   zz239 = (desiredSpeed = carSpeed);
867

    
868
   (* Transition action(s) for transition: Off -> On: NONE
869
      Entry action(s) for transition: Off -> On *)
870
   zz148 = 
871
      (if zz144
872
         then zz119
873
         else zz143);
874
   (* Transition segment: trans23 complete. *)
875

    
876
   zz115 = 
877
      (if (not 
878
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
879
         ((zz146 >= 2) and 
880
         (zz146 <= 8)))
881
         then 
882
               (* <Enter state> path: On maps to field: __root and value: 2 *)
883
               2
884
         else zz146);
885

    
886
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
887
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
888
   zz40 = 
889
      (if zz36
890
         then zz12
891
         else zz38);
892
   (* Transition segment: trans15 complete. *)
893

    
894
   (* Exit action(s) for transition: On -> Off *)
895
   zz140 = 
896
      (if zz139
897
         then zz137
898
         else zz156);
899

    
900
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
901
   zz39 = 
902
      (if zz36
903
         then zz15
904
         else zz33);
905

    
906
   zz8 = 
907
      (if (zz45 = 5)
908
         then 
909
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
910
               3
911
         else zz45);
912

    
913
   zz122 = 
914
      (if (not (zz140 = 1))
915
         then 1
916
         else zz157);
917

    
918
   zz179 = (true -> (pre zz178));
919

    
920
   zz82 = 
921
      (if (zz147 = 4)
922
         then false
923
         else zz141);
924

    
925
   zz203 = (zz201 or 
926
      zz202);
927

    
928
   zz186 = (((((not cancel) and 
929
      (not brakePedal)) and 
930
      zz181) and 
931
      zz182) and 
932
      validInputs);
933

    
934
   zz183 = decelSet;
935

    
936
   zz155 = (true -> 
937
      (if (pre SP3c)
938
         then false
939
         else (pre zz155)));
940

    
941
   zz196 = (mode = 2);
942

    
943
   zz161 = zz160;
944

    
945
   zz9 = 
946
      (if (not (zz44 = 4))
947
         then 
948
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
949
               4
950
         else zz44);
951

    
952
   (* Transition action(s) for transition: On_Inactive -> On_Active *)
953
   zz96 = 
954
      (if zz93
955
         then true
956
         else zz90);
957

    
958
   zz52 = 
959
      (if ((not zz48) and 
960
         (zz50 = 4))
961
         then false
962
         else zz39);
963

    
964
   zz0 = zz217;
965

    
966
   zz2 = (
967
      (if (zz1 and 
968
         (not zz0))
969
         then 0.0
970
         else (zz222 + 0.05)) -> 
971
      (if (zz1 and 
972
         (not zz0))
973
         then 0.0
974
         else 
975
      (if zz0
976
         then (zz222 + 0.05)
977
         else (pre zz2))));
978

    
979
   zz1 = (true -> 
980
      (if (pre zz0)
981
         then false
982
         else (pre zz1)));
983

    
984
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
985
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
986
   zz51 = 
987
      (if zz47
988
         then zz7
989
         else zz46);
990
   (* Transition segment: trans16 complete. *)
991

    
992
   zz162 = 
993
      (if SP3c
994
         then 
995
               (if zz155
996
                  then zz158
997
                  else zz151)
998
         else zz158);
999

    
1000
   (* Condition actions for transition segment: trans19: NONE
1001
      Transition action(s) for transition: trans19
1002
      <complete> is true if either: 
1003
         1. this transition has completed, or 
1004
         2. a higher-priority transition has already completed 
1005
       *)
1006
   zz100 = (zz99 or 
1007
      zz94);
1008

    
1009
   zz53 = 
1010
      (if (not (zz55 = 4))
1011
         then 
1012
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1013
               4
1014
         else zz55);
1015

    
1016
   zz188 = (desiredSpeed <> 100.0);
1017

    
1018
   SP10 = ((not zz191) or 
1019
      zz192);
1020

    
1021
   zz13 = 
1022
      (if (not (zz38 = 6))
1023
         then 5
1024
         else zz35);
1025

    
1026
   zz201 = ((zz163 or 
1027
      zz164) or 
1028
      zz165);
1029

    
1030
   zz14 = 
1031
      (if (zz34 = 4)
1032
         then 
1033
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1034
               3
1035
         else zz34);
1036

    
1037
   zz126 = 
1038
      (if (zz129 = 5)
1039
         then 
1040
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
1041
               3
1042
         else zz129);
1043

    
1044
   (* Exit action(s) for outer loop transition: On_Active_Maintain *)
1045
   zz26 = 
1046
      (if zz24
1047
         then zz23
1048
         else zz107);
1049

    
1050
   (* Exit action(s) for transition: Off -> On *)
1051
   zz146 = 
1052
      (if zz144
1053
         then zz120
1054
         else zz142);
1055

    
1056
   zz199 = (
1057
      (if (zz162 = false)
1058
         then 0.0
1059
         else 1.0) = 1.0);
1060

    
1061
   zz227 = (desiredSpeed - carSpeed);
1062

    
1063
   zz150 = 
1064
      (if ((not zz145) and 
1065

    
1066
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1067
         ((zz147 >= 2) and 
1068
         (zz147 <= 8)))
1069
         then zz111
1070
         else zz148);
1071

    
1072
   zz177 = (zz176 = 20);
1073

    
1074
   (* Transition action(s) for outer loop transition: On_Active_Maintain *)
1075
   zz27 = 
1076
      (if zz24
1077
         then true
1078
         else zz26);
1079

    
1080
   (* Entry action(s) for transition: On_Inactive -> On_Active *)
1081
   zz97 = 
1082
      (if zz93
1083
         then zz74
1084
         else zz95);
1085
   (* Transition segment: trans20 complete. *)
1086

    
1087
   zz195 = (desiredSpeed = 0.0);
1088

    
1089
   zz71 = 
1090
      (if (not 
1091
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1092
         ((zz95 >= 3) and 
1093
         (zz95 <= 6)))
1094
         then 
1095
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1096
               3
1097
         else zz95);
1098

    
1099
   zz62 = 
1100
      (if (not (zz63 = 4))
1101
         then 4
1102
         else zz98);
1103

    
1104
   zz229 = 
1105
      (if (zz228 < ( -10.0))
1106
         then ( -10.0)
1107
         else 
1108
      (if (zz228 > 10.0)
1109
         then 10.0
1110
         else zz228));
1111

    
1112
   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE
1113
      Entry action(s) for transition: On_Inactive -> On_Active *)
1114
   zz103 = 
1115
      (if zz99
1116
         then zz67
1117
         else zz98);
1118
   (* Transition segment: trans19 complete. *)
1119

    
1120
   zz55 = 
1121
      (if (not 
1122
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1123
         ((zz106 >= 3) and 
1124
         (zz106 <= 6)))
1125
         then 
1126
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1127
               3
1128
         else zz106);
1129

    
1130
   (* Beginning transition segment: trans18
1131
      <fired> is true if the following are true: 
1132
         1. the previous transition guard was true, 
1133
         2. the source node for the transition is active, 
1134
         3. the condition for the transition to fire is true, and 
1135
         4. no higher-priority transition has completed (not <complete>) *)
1136
   zz56 = ((not 
1137
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1138
      ((zz106 >= 3) and 
1139
      (zz106 <= 6))) and 
1140

    
1141
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1142
      ((zz55 >= 3) and 
1143
      (zz55 <= 6)));
1144

    
1145
   (* Beginning transition segment: trans18
1146
      <fired> is true if the following are true: 
1147
         1. the previous transition guard was true, 
1148
         2. the source node for the transition is active, 
1149
         3. the condition for the transition to fire is true, and 
1150
         4. no higher-priority transition has completed (not <complete>) *)
1151
   zz72 = ((not 
1152
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1153
      ((zz95 >= 3) and 
1154
      (zz95 <= 6))) and 
1155

    
1156
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1157
      ((zz71 >= 3) and 
1158
      (zz71 <= 6)));
1159

    
1160
   (* Transition action(s) for transition: On_Active -> On_Inactive: NONE
1161
      Entry action(s) for transition: On_Active -> On_Inactive *)
1162
   zz91 = 
1163
      (if zz88
1164
         then zz77
1165
         else zz89);
1166
   (* Transition segment: trans21 complete. *)
1167

    
1168
   zz202 = (mode = 3);
1169

    
1170
   zz221 = 
1171
      (if zz162
1172
         then carSpeed
1173
         else zz223);
1174

    
1175
   SP2 = ((not (not zz201)) or 
1176
      zz187);
1177

    
1178
   (* Entry action(s) for transition: On_Init -> On_Active *)
1179
   zz108 = 
1180
      (if zz104
1181
         then zz58
1182
         else zz106);
1183
   (* Transition segment: trans22 complete. *)
1184

    
1185
   zz238 = (desiredSpeed = zz211);
1186

    
1187
   zz212 = (zz211 = desiredSpeed);
1188

    
1189
   (* Beginning transition segment: trans21
1190
      <fired> is true if the following are true: 
1191
         1. the previous transition guard was true, 
1192
         2. the source node for the transition is active, 
1193
         3. the condition for the transition to fire is true, and 
1194
         4. no higher-priority transition has completed (not <complete>) *)
1195
   zz88 = (
1196
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1197
      ((zz147 >= 3) and 
1198
      (zz147 <= 6)) and 
1199
      (not zz186));
1200

    
1201
   (* Condition actions for transition segment: trans16: NONE
1202
      Transition action(s) for transition: trans16
1203
      <complete> is true if either: 
1204
         1. this transition has completed, or 
1205
         2. a higher-priority transition has already completed 
1206
       *)
1207
   zz48 = (zz47 or 
1208
      zz43);
1209

    
1210
   SP4 = ((not zz203) or 
1211
      zz194);
1212

    
1213
   zz149 = 
1214
      (if ((not zz145) and 
1215

    
1216
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1217
         ((zz147 >= 2) and 
1218
         (zz147 <= 8)))
1219
         then zz110
1220
         else zz147);
1221

    
1222
   zz132 = 
1223
      (if 
1224
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1225
         ((zz156 >= 3) and 
1226
         (zz156 <= 6))
1227
         then 
1228
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
1229
               2
1230
         else zz131);
1231

    
1232
   zz112 = 
1233
      (if ((not zz105) and 
1234

    
1235
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1236
         ((zz108 >= 3) and 
1237
         (zz108 <= 6)))
1238
         then zz52
1239
         else zz107);
1240

    
1241
   (* Exit action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
1242
   zz44 = 
1243
      (if zz42
1244
         then zz11
1245
         else zz40);
1246

    
1247
   zz215 = (zz211 < desiredSpeed);
1248

    
1249
   zz236 = (desiredSpeed > 0.0);
1250

    
1251
   zz113 = 
1252
      (if (not (zz115 = 7))
1253
         then 
1254
               (* <Enter state> path: On.Init maps to field: __root and value: 7 *)
1255
               7
1256
         else zz115);
1257

    
1258
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
1259
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
1260
   zz50 = 
1261
      (if zz47
1262
         then zz6
1263
         else zz49);
1264
   (* Transition segment: trans16 complete. *)
1265

    
1266
   (* Exit action(s) for transition: On_Inactive -> On_Active *)
1267
   zz95 = 
1268
      (if zz93
1269
         then zz76
1270
         else zz91);
1271

    
1272
   zz3 = zz216;
1273

    
1274
   zz5 = (
1275
      (if (zz4 and 
1276
         (not zz3))
1277
         then 0.0
1278
         else (zz222 - 0.05)) -> 
1279
      (if (zz4 and 
1280
         (not zz3))
1281
         then 0.0
1282
         else 
1283
      (if zz3
1284
         then (zz222 - 0.05)
1285
         else (pre zz5))));
1286

    
1287
   zz4 = (true -> 
1288
      (if (pre zz3)
1289
         then false
1290
         else (pre zz4)));
1291

    
1292
   zz60 = 
1293
      (if (zz102 = 7)
1294
         then 
1295
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
1296
               2
1297
         else zz102);
1298

    
1299
   (* Entry action(s) for transition: On_Init -> On_Active *)
1300
   zz109 = 
1301
      (if zz104
1302
         then zz59
1303
         else zz103);
1304
   (* Transition segment: trans22 complete. *)
1305

    
1306
   zz205 = (0.0 -> (pre zz204));
1307

    
1308
   zz209 = zz163;
1309

    
1310
   zz216 = zz164;
1311

    
1312
   zz217 = zz165;
1313

    
1314
   zz117 = (
1315
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1316
      ((zz118 >= 3) and 
1317
      (zz118 <= 6)) or 
1318
      ((zz118 = 7) or 
1319
      (zz118 = 8)));
1320

    
1321
   zz70 = 
1322
      (if (not (zz71 = 4))
1323
         then 4
1324
         else zz92);
1325

    
1326
   zz22 = 
1327
      (if (zz108 = 4)
1328
         then 
1329
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1330
               3
1331
         else zz108);
1332

    
1333
   zz160 = 
1334
      (if SP3c
1335
         then 
1336
               (if zz155
1337
                  then zz153
1338
                  else zz149)
1339
         else zz156);
1340

    
1341
   VRP2 = (zz234 and 
1342
      zz233);
1343

    
1344
   zz153 = 
1345
      (if (not (zz156 = 1))
1346
         then 
1347
               (* <Enter state> path: Off maps to field: __root and value: 1 *)
1348
               1
1349
         else zz156);
1350

    
1351
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1352
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1353
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1354
   zz58 = 
1355
      (if zz56
1356
         then zz53
1357
         else zz55);
1358
   (* Transition segment: trans18 complete. *)
1359

    
1360
   (* Beginning transition segment: trans23
1361
      <fired> is true if the following are true: 
1362
         1. the previous transition guard was true, 
1363
         2. the source node for the transition is active, 
1364
         3. the condition for the transition to fire is true, and 
1365
         4. no higher-priority transition has completed (not <complete>) *)
1366
   zz144 = ((zz142 = 1) and 
1367
      (onOff and 
1368
      (not zz139)));
1369

    
1370
   (* Condition actions for transition segment: trans15: NONE
1371
      Transition action(s) for transition: trans15
1372
      <complete> is true if either: 
1373
         1. this transition has completed, or 
1374
         2. a higher-priority transition has already completed 
1375
       *)
1376
   zz37 = (zz36 or 
1377
      zz31);
1378

    
1379
   zz222 = (0.0 -> (pre desiredSpeed));
1380

    
1381
   zz228 = (zz227 * 1.0);
1382

    
1383
   zz68 = 
1384
      (if (zz97 = 8)
1385
         then 
1386
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
1387
               2
1388
         else zz97);
1389

    
1390
   zz125 = 
1391
      (if (zz130 = 6)
1392
         then 
1393
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
1394
               3
1395
         else zz130);
1396

    
1397
   zz170 = 
1398
      (if (zz166 <= 20)
1399
         then zz166
1400
         else 20);
1401

    
1402
   zz167 = (zz169 + 1);
1403

    
1404
   zz11 = 
1405
      (if (zz40 = 6)
1406
         then 
1407
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
1408
               3
1409
         else zz40);
1410

    
1411
   zz163 = (mode = 4);
1412

    
1413
   zz187 = (cruiseThrottle = 0.0);
1414

    
1415
   zz129 = 
1416
      (if 
1417
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1418
         ((zz156 >= 3) and 
1419
         (zz156 <= 6))
1420
         then zz127
1421
         else zz156);
1422

    
1423
   (* Exit action(s) for transition: On_Active -> On_Inactive *)
1424
   zz90 = 
1425
      (if zz88
1426
         then zz87
1427
         else zz141);
1428

    
1429
   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE
1430
      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
1431
   zz46 = 
1432
      (if zz42
1433
         then zz10
1434
         else zz41);
1435
   (* Transition segment: trans17 complete. *)
1436

    
1437
   (* Entry action(s) for transition: On_Inactive -> On_Active *)
1438
   zz98 = 
1439
      (if zz93
1440
         then zz75
1441
         else zz92);
1442
   (* Transition segment: trans20 complete. *)
1443

    
1444
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
1445
   zz32 = 
1446
      (if zz30
1447
         then zz18
1448
         else zz28);
1449

    
1450
   zz225 = (zz230 + zz224);
1451

    
1452
   zz190 = desiredSpeed;
1453

    
1454
   zz207 = (zz211 <= desiredSpeed);
1455

    
1456
   (* Exit action(s) for outer loop transition: On_Active_Maintain *)
1457
   zz25 = 
1458
      (if zz24
1459
         then zz22
1460
         else zz108);
1461

    
1462
   mode = 
1463
      (if SP3c
1464
         then 
1465
               (if zz155
1466
                  then zz154
1467
                  else zz150)
1468
         else zz157);
1469

    
1470
   SP5 = ((not zz163) or 
1471
      zz206);
1472

    
1473
   zz135 = 
1474
      (if 
1475
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1476
         ((zz156 >= 2) and 
1477
         (zz156 <= 8))
1478
         then zz124
1479
         else zz134);
1480

    
1481
   zz111 = 
1482
      (if ((not zz105) and 
1483

    
1484
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1485
         ((zz108 >= 3) and 
1486
         (zz108 <= 6)))
1487
         then zz51
1488
         else zz109);
1489

    
1490
   SP3b = ((not zz198) or 
1491
      zz200);
1492

    
1493
   (* Transition action(s) for transition: On -> Off: NONE
1494
      Entry action(s) for transition: On -> Off *)
1495
   zz143 = 
1496
      (if zz139
1497
         then zz122
1498
         else zz157);
1499
   (* Transition segment: trans13 complete. *)
1500

    
1501
   zz219 = 
1502
      (if zz202
1503
         then zz222
1504
         else 0.0);
1505

    
1506
   zz23 = 
1507
      (if (zz108 = 4)
1508
         then false
1509
         else zz107);
1510

    
1511
   (* Condition actions for transition segment: trans23: NONE
1512
      Transition action(s) for transition: trans23
1513
      <complete> is true if either: 
1514
         1. this transition has completed, or 
1515
         2. a higher-priority transition has already completed 
1516
       *)
1517
   zz145 = (zz144 or 
1518
      zz139);
1519

    
1520
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1521
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1522
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1523
   zz66 = 
1524
      (if zz64
1525
         then zz61
1526
         else zz63);
1527
   (* Transition segment: trans18 complete. *)
1528

    
1529
   SP3 = ((not zz198) or 
1530
      zz195);
1531

    
1532
   zz232 = (cruiseThrottle >= 0.0);
1533

    
1534
   zz110 = 
1535
      (if ((not zz105) and 
1536

    
1537
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1538
         ((zz108 >= 3) and 
1539
         (zz108 <= 6)))
1540
         then zz50
1541
         else zz108);
1542

    
1543
   zz152 = ((zz153 = 1) or 
1544

    
1545
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1546
      ((zz153 >= 2) and 
1547
      (zz153 <= 8)));
1548

    
1549
   (* Transition action(s) for transition: On_Init -> On_Active *)
1550
   zz107 = 
1551
      (if zz104
1552
         then true
1553
         else zz96);
1554

    
1555
   (* Exit action(s) for transition: On_Active -> On_Inactive *)
1556
   zz89 = 
1557
      (if zz88
1558
         then zz86
1559
         else zz147);
1560

    
1561
   SP11 = ((not zz193) or 
1562
      zz194);
1563

    
1564
   zz220 = 
1565
      (if zz163
1566
         then zz222
1567
         else zz219);
1568

    
1569
   zz21 = 
1570
      (if (not (zz25 = 4))
1571
         then 4
1572
         else zz109);
1573

    
1574
   zz213 = (false -> (pre zz216));
1575

    
1576
   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE
1577
      Entry action(s) for transition: On_Inactive -> On_Active *)
1578
   zz102 = 
1579
      (if zz99
1580
         then zz66
1581
         else zz101);
1582
   (* Transition segment: trans19 complete. *)
1583

    
1584
   zz176 = 
1585
      (if (zz172 <= 20)
1586
         then zz172
1587
         else 20);
1588

    
1589
   zz130 = 
1590
      (if 
1591
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1592
         ((zz156 >= 3) and 
1593
         (zz156 <= 6))
1594
         then zz126
1595
         else zz129);
1596

    
1597
   zz237 = (zz236 and 
1598
      zz235);
1599

    
1600
   (* Exit action(s) for transition: On_Inactive -> On_Active *)
1601
   zz101 = 
1602
      (if zz99
1603
         then zz68
1604
         else zz97);
1605

    
1606
   zz164 = (mode = 5);
1607

    
1608
   zz17 = 
1609
      (if (not (zz32 = 5))
1610
         then 6
1611
         else zz29);
1612

    
1613
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1614
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1615
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1616
   zz74 = 
1617
      (if zz72
1618
         then zz69
1619
         else zz71);
1620
   (* Transition segment: trans18 complete. *)
1621

    
1622
   zz230 = (zz229 / 20.0);
1623

    
1624
   CP8a = ((not zz162) or 
1625
      zz201);
1626

    
1627
   zz133 = 
1628
      (if 
1629
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1630
         ((zz156 >= 3) and 
1631
         (zz156 <= 6))
1632
         then zz128
1633
         else zz158);
1634

    
1635
   SP6 = ((not zz164) or 
1636
      zz207);
1637

    
1638
   zz151 = 
1639
      (if ((not zz145) and 
1640

    
1641
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1642
         ((zz147 >= 2) and 
1643
         (zz147 <= 8)))
1644
         then zz112
1645
         else zz141);
1646

    
1647
   zz189 = (false -> (pre zz217));
1648

    
1649
   zz214 = (zz213 and 
1650
      zz193);
1651

    
1652
   (* Entry action(s) for outer loop transition: On_Active_Maintain *)
1653
   zz28 = 
1654
      (if zz24
1655
         then zz20
1656
         else zz25);
1657
   (* Transition segment: trans24 complete. *)
1658

    
1659
   zz206 = (zz205 = cruiseThrottle);
1660

    
1661
   zz12 = 
1662
      (if (not (zz38 = 6))
1663
         then 
1664
               (* <Enter state> path: On.Active.Decrease maps to field: __root and value: 6 *)
1665
               6
1666
         else zz38);
1667

    
1668
   zz224 = (0.0 -> (pre cruiseThrottle));
1669

    
1670
   zz87 = 
1671
      (if 
1672
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1673
         ((zz147 >= 3) and 
1674
         (zz147 <= 6))
1675
         then zz82
1676
         else zz141);
1677

    
1678
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1679
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1680
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1681
   zz59 = 
1682
      (if zz56
1683
         then zz54
1684
         else zz103);
1685
   (* Transition segment: trans18 complete. *)
1686

    
1687
   zz128 = 
1688
      (if (zz156 = 4)
1689
         then false
1690
         else zz158);
1691

    
1692
   (* Transition action(s) for transition: Off -> On: NONE
1693
      Entry action(s) for transition: Off -> On *)
1694
   zz147 = 
1695
      (if zz144
1696
         then zz118
1697
         else zz146);
1698
   (* Transition segment: trans23 complete. *)
1699

    
1700
   SP8 = ((not zz210) or 
1701
      zz212);
1702

    
1703
   zz7 = 
1704
      (if (not (zz49 = 4))
1705
         then 4
1706
         else zz46);
1707

    
1708
   desiredSpeed = 
1709
      (if (zz221 < 0.0)
1710
         then 0.0
1711
         else 
1712
      (if (zz221 > 100.0)
1713
         then 100.0
1714
         else zz221));
1715

    
1716
   (* Entry action(s) for outer loop transition: On_Active_Maintain *)
1717
   zz29 = 
1718
      (if zz24
1719
         then zz21
1720
         else zz109);
1721
   (* Transition segment: trans24 complete. *)
1722

    
1723
   zz18 = 
1724
      (if (zz28 = 4)
1725
         then 
1726
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1727
               3
1728
         else zz28);
1729

    
1730
   zz114 = 
1731
      (if (not (zz115 = 7))
1732
         then 2
1733
         else zz143);
1734

    
1735
   zz211 = (0.0 -> (pre zz190));
1736

    
1737
   zz226 = 
1738
      (if (zz225 < 0.0)
1739
         then 0.0
1740
         else 
1741
      (if (zz225 > 100.0)
1742
         then 100.0
1743
         else zz225));
1744

    
1745
   zz69 = 
1746
      (if (not (zz71 = 4))
1747
         then 
1748
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1749
               4
1750
         else zz71);
1751

    
1752
   zz20 = 
1753
      (if (not (zz25 = 4))
1754
         then 
1755
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1756
               4
1757
         else zz25);
1758

    
1759
   (* Condition actions for transition segment: trans14: NONE
1760
      Transition action(s) for transition: trans14
1761
      <complete> is true if either: 
1762
         1. this transition has completed, or 
1763
         2. a higher-priority transition has already completed 
1764
       *)
1765
   zz31 = (zz30 or 
1766
      zz24);
1767

    
1768
   zz218 = 
1769
      (if zz216
1770
         then zz5
1771
         else zz220);
1772

    
1773
   zz10 = 
1774
      (if (not (zz44 = 4))
1775
         then 4
1776
         else zz41);
1777

    
1778
   zz77 = 
1779
      (if (not (zz89 = 8))
1780
         then 
1781
               (* <Enter state> path: On.Inactive maps to field: __root and value: 8 *)
1782
               8
1783
         else zz89);
1784

    
1785
   (* Transition action(s) for transition: On_Active -> On_Inactive: NONE
1786
      Entry action(s) for transition: On_Active -> On_Inactive *)
1787
   zz92 = 
1788
      (if zz88
1789
         then zz78
1790
         else zz148);
1791
   (* Transition segment: trans21 complete. *)
1792

    
1793
   zz182 = (carSpeed >= 15.0);
1794

    
1795
   zz210 = (false -> (pre zz209));
1796

    
1797
   zz85 = 
1798
      (if 
1799
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1800
         ((zz147 >= 3) and 
1801
         (zz147 <= 6))
1802
         then zz79
1803
         else zz84);
1804

    
1805
   zz84 = 
1806
      (if 
1807
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1808
         ((zz147 >= 3) and 
1809
         (zz147 <= 6))
1810
         then zz80
1811
         else zz83);
1812

    
1813
   (* Exit action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
1814
   zz49 = 
1815
      (if zz47
1816
         then zz8
1817
         else zz45);
1818

    
1819
--  --%PROPERTY zz57;
1820
--   --%PROPERTY zz65;
1821
--   --%PROPERTY zz73;
1822
--   --%PROPERTY zz117;
1823
--   --%PROPERTY zz152;
1824
--   --%PROPERTY       VRP1;
1825
--   --%PROPERTY       VRP2;
1826
--   --%PROPERTY       CP8a;
1827
   --%PROPERTY       OK;
1828
--   --%PROPERTY       VRP4;
1829
--   --%PROPERTY       SP4;
1830
--   --%PROPERTY       SP5;
1831
--   --%PROPERTY       SP6;
1832
--   --%PROPERTY       SP7;
1833
--   --%PROPERTY       SP3b;
1834
--   --%PROPERTY       SP3c;
1835
--   --%PROPERTY       SP3;
1836
--   --%PROPERTY       SP3a;
1837
--   --%PROPERTY       SP2;
1838
--   --%PROPERTY       SP1;
1839
--   --%PROPERTY       SP8;
1840
--   --%PROPERTY       SP9;
1841
--   --%PROPERTY       SP10;
1842
--   --%PROPERTY       SP11;
1843

    
1844
--   check zz57; 
1845

    
1846
--   check zz65; 
1847

    
1848
--   check zz73; 
1849

    
1850
--   check zz117; 
1851

    
1852
--   check zz152;
1853

    
1854
tel;
1855

    
1856