Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
485
   SP3c = true;
486

    
487
   zz171 = (zz170 = 20);
488

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

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

    
505
   zz204 = cruiseThrottle;
506

    
507
   zz165 = (mode = 6);
508

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

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

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

    
526
   zz173 = (zz175 + 1);
527

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

    
535
   zz181 = (carGear = 3);
536

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

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

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

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

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

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

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

    
582
   zz192 = (zz211 > desiredSpeed);
583

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

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

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

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

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

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

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

    
628
   zz198 = (zz197 or 
629
      zz196);
630

    
631
   zz193 = (desiredSpeed <> 0.0);
632

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

    
636
   zz231 = (cruiseThrottle <= 100.0);
637

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

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

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

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

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

    
674
   VRP1 = (zz232 and 
675
      zz231);
676

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

    
685
   zz235 = (desiredSpeed < 0.0);
686

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

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

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

    
702
   zz194 = (desiredSpeed >= 15.0);
703

    
704
   zz197 = (mode = 1);
705

    
706
   VRP3 = (not zz237);
707

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

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

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

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

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

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

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

    
762
   zz178 = accelResume;
763

    
764
   zz234 = (desiredSpeed >= 0.0);
765

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

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

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

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

    
792
   zz191 = (zz189 and 
793
      zz188);
794

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

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

    
811
   zz208 = (zz211 >= desiredSpeed);
812

    
813
   zz200 = (zz223 = 0.0);
814

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

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

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

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

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

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

    
852
   zz233 = (desiredSpeed <= 100.0);
853

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

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

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

    
865
   zz239 = (desiredSpeed = carSpeed);
866

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

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

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

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

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

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

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

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

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

    
924
   zz203 = (zz201 or 
925
      zz202);
926

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

    
933
   zz183 = decelSet;
934

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

    
940
   zz196 = (mode = 2);
941

    
942
   zz161 = zz160;
943

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

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

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

    
963
   zz0 = zz217;
964

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

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

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

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

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

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

    
1015
   zz188 = (desiredSpeed <> 100.0);
1016

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

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

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

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

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

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

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

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

    
1060
   zz227 = (desiredSpeed - carSpeed);
1061

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

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

    
1071
   zz177 = (zz176 = 20);
1072

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

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

    
1086
   zz195 = (desiredSpeed = 0.0);
1087

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

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

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

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

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

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

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

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

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

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

    
1167
   zz202 = (mode = 3);
1168

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

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

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

    
1184
   zz238 = (desiredSpeed = zz211);
1185

    
1186
   zz212 = (zz211 = desiredSpeed);
1187

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

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

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

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

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

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

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

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

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

    
1246
   zz215 = (zz211 < desiredSpeed);
1247

    
1248
   zz236 = (desiredSpeed > 0.0);
1249

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

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

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

    
1271
   zz3 = zz216;
1272

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

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

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

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

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

    
1307
   zz209 = zz163;
1308

    
1309
   zz216 = zz164;
1310

    
1311
   zz217 = zz165;
1312

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

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

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

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

    
1340
   VRP2 = (zz234 and 
1341
      zz233);
1342

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

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

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

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

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

    
1380
   zz228 = (zz227 * 1.0);
1381

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

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

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

    
1401
   zz167 = (zz169 + 1);
1402

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

    
1410
   zz163 = (mode = 4);
1411

    
1412
   zz187 = (cruiseThrottle = 0.0);
1413

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

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

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

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

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

    
1449
   zz225 = (zz230 + zz224);
1450

    
1451
   zz190 = desiredSpeed;
1452

    
1453
   zz207 = (zz211 <= desiredSpeed);
1454

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1531
   zz232 = (cruiseThrottle >= 0.0);
1532

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

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

    
1542
   zz152 = ((zz153 = 1) or 
1543

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

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

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

    
1560
   OK = ((not zz193) or 
1561
      zz194);
1562

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

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

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

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

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

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

    
1596
   zz237 = (zz236 and 
1597
      zz235);
1598

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

    
1605
   zz164 = (mode = 5);
1606

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

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

    
1621
   zz230 = (zz229 / 20.0);
1622

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

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

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

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

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

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

    
1648
   zz214 = (zz213 and 
1649
      zz193);
1650

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

    
1658
   zz206 = (zz205 = cruiseThrottle);
1659

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1792
   zz182 = (carSpeed >= 15.0);
1793

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

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

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

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

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

    
1843
--   check zz57; 
1844

    
1845
--   check zz65; 
1846

    
1847
--   check zz73; 
1848

    
1849
--   check zz117; 
1850

    
1851
--   check zz152;
1852

    
1853
tel;
1854

    
1855