Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / large / ccp01.lus @ 65f71d05

History | View | Annotate | Download (44.2 KB)

1 22fe1c93 ploc
2
3 65f71d05 ploc
--@ ensures OK;
4 22fe1c93 ploc
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)
12
      returns (OK:bool);
13
14
var
15
   mode: int ; 
16
      cruiseThrottle: real; 
17
      desiredSpeed: real; 
18
      VRP1: bool; 
19
      VRP2: bool; 
20
      CP8a: bool; 
21
      VRP3: bool; 
22
      VRP4: bool; 
23
      SP4: bool; 
24
      SP5: bool; 
25
      SP6: bool; 
26
      SP7: bool; 
27
      SP3b: bool; 
28
      SP3c: bool; 
29
      SP3: bool; 
30
      SP3a: bool; 
31
      SP2: bool; 
32
      SP1: bool; 
33
      SP8: bool; 
34
      SP9: bool; 
35
      SP10: bool; 
36
      SP11: bool;
37
   zz0: bool; 
38
   zz1: bool; 
39
   zz2: real; 
40
   zz3: bool; 
41
   zz4: bool; 
42
   zz5: real; 
43
   zz6: int ; 
44
   zz7: int ; 
45
   zz8: int ; 
46
   zz9: int ; 
47
   zz10: int ; 
48
   zz11: int ; 
49
   zz12: int ; 
50
   zz13: int ; 
51
   zz14: int ; 
52
   zz15: bool; 
53
   zz16: int ; 
54
   zz17: int ; 
55
   zz18: int ; 
56
   zz19: bool; 
57
   zz20: int ; 
58
   zz21: int ; 
59
   zz22: int ; 
60
   zz23: bool; 
61
   zz24: bool; 
62
   zz25: int ; 
63
   zz26: bool; 
64
   zz27: bool; 
65
   zz28: int ; 
66
   zz29: int ; 
67
   zz30: bool; 
68
   zz31: bool; 
69
   zz32: int ; 
70
   zz33: bool; 
71
   zz34: int ; 
72
   zz35: int ; 
73
   zz36: bool; 
74
   zz37: bool; 
75
   zz38: int ; 
76
   zz39: bool; 
77
   zz40: int ; 
78
   zz41: int ; 
79
   zz42: bool; 
80
   zz43: bool; 
81
   zz44: int ; 
82
   zz45: int ; 
83
   zz46: int ; 
84
   zz47: bool; 
85
   zz48: bool; 
86
   zz49: int ; 
87
   zz50: int ; 
88
   zz51: int ; 
89
   zz52: bool; 
90
   zz53: int ; 
91
   zz54: int ; 
92
   zz55: int ; 
93
   zz56: bool; 
94
   zz58: int ; 
95
   zz59: int ; 
96
   zz60: int ; 
97
   zz61: int ; 
98
   zz62: int ; 
99
   zz63: int ; 
100
   zz64: bool; 
101
   zz65: bool; 
102
   zz66: int ; 
103
   zz67: int ; 
104
   zz68: int ; 
105
   zz69: int ; 
106
   zz70: int ; 
107
   zz71: int ; 
108
   zz72: bool; 
109
   zz73: bool; 
110
   zz74: int ; 
111
   zz75: int ; 
112
   zz76: int ; 
113
   zz77: int ; 
114
   zz78: int ; 
115
   zz79: int ; 
116
   zz80: int ; 
117
   zz81: int ; 
118
   zz82: bool; 
119
   zz83: int ; 
120
   zz84: int ; 
121
   zz85: int ; 
122
   zz86: int ; 
123
   zz87: bool; 
124
   zz88: bool; 
125
   zz89: int ; 
126
   zz90: bool; 
127
   zz91: int ; 
128
   zz92: int ; 
129
   zz93: bool; 
130
   zz94: bool; 
131
   zz95: int ; 
132
   zz96: bool; 
133
   zz97: int ; 
134
   zz98: int ; 
135
   zz99: bool; 
136
   zz100: bool; 
137
   zz101: int ; 
138
   zz102: int ; 
139
   zz103: int ; 
140
   zz104: bool; 
141
   zz105: bool; 
142
   zz106: int ; 
143
   zz107: bool; 
144
   zz108: int ; 
145
   zz109: int ; 
146
   zz110: int ; 
147
   zz111: int ; 
148
   zz112: bool; 
149
   zz113: int ; 
150
   zz114: int ; 
151
   zz115: int ; 
152
   zz116: bool; 
153
   zz117: bool; 
154
   zz118: int ; 
155
   zz119: int ; 
156
   zz120: int ; 
157
   zz121: int ; 
158
   zz122: int ; 
159
   zz123: int ; 
160
   zz124: int ; 
161
   zz125: int ; 
162
   zz126: int ; 
163
   zz127: int ; 
164
   zz128: bool; 
165
   zz129: int ; 
166
   zz130: int ; 
167
   zz131: int ; 
168
   zz132: int ; 
169
   zz133: bool; 
170
   zz134: int ; 
171
   zz135: int ; 
172
   zz136: int ; 
173
   zz137: int ; 
174
   zz138: bool; 
175
   zz139: bool; 
176
   zz140: int ; 
177
   zz141: bool; 
178
   zz142: int ; 
179
   zz143: int ; 
180
   zz144: bool; 
181
   zz145: bool; 
182
   zz146: int ; 
183
   zz147: int ; 
184
   zz148: int ; 
185
   zz149: int ; 
186
   zz150: int ; 
187
   zz151: bool; 
188
   zz152: bool; 
189
   zz153: int ; 
190
   zz154: int ; 
191
   zz155: bool; 
192
   zz156: int ; 
193
   zz157: int ; 
194
   zz158: bool; 
195
   zz159: int ; 
196
   zz160: int ; 
197
   zz161: int ; 
198
   zz162: bool; 
199
   zz163: bool; 
200
   zz164: bool; 
201
   zz165: bool; 
202
   zz166: int ; 
203
   zz167: int ; 
204
   zz168: int ; 
205
   zz169: int ; 
206
   zz170: int ; 
207
   zz171: bool; 
208
   zz172: int ; 
209
   zz173: int ; 
210
   zz174: int ; 
211
   zz175: int ; 
212
   zz176: int ; 
213
   zz177: bool; 
214
   zz178: bool; 
215
   zz179: bool; 
216
   zz180: bool; 
217
   zz181: bool; 
218
   zz182: bool; 
219
   zz183: bool; 
220
   zz184: bool; 
221
   zz185: bool; 
222
   zz186: bool; 
223
   zz187: bool; 
224
   zz188: bool; 
225
   zz189: bool; 
226
   zz190: real; 
227
   zz191: bool; 
228
   zz192: bool; 
229
   zz193: bool; 
230
   zz194: bool; 
231
   zz195: bool; 
232
   zz196: bool; 
233
   zz197: bool; 
234
   zz198: bool; 
235
   zz199: bool; 
236
   zz200: bool; 
237
   zz201: bool; 
238
   zz202: bool; 
239
   zz203: bool; 
240
   zz204: real; 
241
   zz205: real; 
242
   zz206: bool; 
243
   zz207: bool; 
244
   zz208: bool; 
245
   zz209: bool; 
246
   zz210: bool; 
247
   zz211: real; 
248
   zz212: bool; 
249
   zz213: bool; 
250
   zz214: bool; 
251
   zz215: bool; 
252
   zz216: bool; 
253
   zz217: bool; 
254
   zz218: real; 
255
   zz219: real; 
256
   zz220: real; 
257
   zz221: real; 
258
   zz222: real; 
259
   zz223: real; 
260
   zz224: real; 
261
   zz225: real; 
262
   zz226: real; 
263
   zz227: real; 
264
   zz228: real; 
265
   zz229: real; 
266
   zz230: real; 
267
   zz231: bool; 
268
   zz232: bool; 
269
   zz233: bool; 
270
   zz234: bool; 
271
   zz235: bool; 
272
   zz236: bool; 
273
   zz237: bool; 
274
   zz238: bool; 
275
   zz239: bool;
276
277
let 
278
   zz166 = 
279
      (if (0 >= zz168)
280
         then 0
281
         else zz168);
282
283
   zz168 = 
284
      (if accelResume
285
         then zz167
286
         else 0);
287
288
   zz169 = (0 -> (pre zz170));
289
290
   zz172 = 
291
      (if (0 >= zz174)
292
         then 0
293
         else zz174);
294
295
   zz174 = 
296
      (if decelSet
297
         then zz173
298
         else 0);
299
300
   zz175 = (0 -> (pre zz176));
301
302
   zz156 = (0 -> (pre zz161));
303
304
   zz157 = (0 -> (pre mode));
305
306
   zz159 = 
307
      (if SP3c
308
         then 1
309
         else 0);
310
311
   (* Beginning transition segment: trans20
312
      <fired> is true if the following are true: 
313
         1. the previous transition guard was true, 
314
         2. the source node for the transition is active, 
315
         3. the condition for the transition to fire is true, and 
316
         4. no higher-priority transition has completed (not <complete>) *)
317
   zz93 = ((zz91 = 8) and 
318
      (((
319
      (if ((zz185 = true) = false)
320
         then 0
321
         else 1) <> 0) and 
322
      (
323
      (if ((zz186 = true) = false)
324
         then 0
325
         else 1) <> 0)) and 
326
      (not zz88)));
327
328
   (* Beginning transition segment: trans19
329
      <fired> is true if the following are true: 
330
         1. the previous transition guard was true, 
331
         2. the source node for the transition is active, 
332
         3. the condition for the transition to fire is true, and 
333
         4. no higher-priority transition has completed (not <complete>) *)
334
   zz99 = ((zz97 = 8) and 
335
      (((
336
      (if ((zz180 = true) = false)
337
         then 0
338
         else 1) <> 0) and 
339
      (
340
      (if ((zz186 = true) = false)
341
         then 0
342
         else 1) <> 0)) and 
343
      (not zz94)));
344
345
   (* Beginning transition segment: trans22
346
      <fired> is true if the following are true: 
347
         1. the previous transition guard was true, 
348
         2. the source node for the transition is active, 
349
         3. the condition for the transition to fire is true, and 
350
         4. no higher-priority transition has completed (not <complete>) *)
351
   zz104 = ((zz102 = 7) and 
352
      (((
353
      (if ((zz185 = true) = false)
354
         then 0
355
         else 1) <> 0) and 
356
      (
357
      (if ((zz186 = true) = false)
358
         then 0
359
         else 1) <> 0)) and 
360
      (not zz100)));
361
362
   (* Beginning transition segment: trans24
363
      <fired> is true if the following are true: 
364
         1. the previous transition guard was true, 
365
         2. the source node for the transition is active, 
366
         3. the condition for the transition to fire is true, and 
367
         4. no higher-priority transition has completed (not <complete>) *)
368
   zz24 = ((zz108 = 4) and 
369
      (
370
      (if ((zz185 = true) = false)
371
         then 0
372
         else 1) <> 0));
373
374
   (* Beginning transition segment: trans14
375
      <fired> is true if the following are true: 
376
         1. the previous transition guard was true, 
377
         2. the source node for the transition is active, 
378
         3. the condition for the transition to fire is true, and 
379
         4. no higher-priority transition has completed (not <complete>) *)
380
   zz30 = ((zz28 = 4) and 
381
      ((
382
      (if ((zz171 = true) = false)
383
         then 0
384
         else 1) <> 0) and 
385
      (not zz24)));
386
387
   (* Beginning transition segment: trans15
388
      <fired> is true if the following are true: 
389
         1. the previous transition guard was true, 
390
         2. the source node for the transition is active, 
391
         3. the condition for the transition to fire is true, and 
392
         4. no higher-priority transition has completed (not <complete>) *)
393
   zz36 = ((zz34 = 4) and 
394
      ((
395
      (if ((zz177 = true) = false)
396
         then 0
397
         else 1) <> 0) and 
398
      (not zz31)));
399
400
   (* Beginning transition segment: trans17
401
      <fired> is true if the following are true: 
402
         1. the previous transition guard was true, 
403
         2. the source node for the transition is active, 
404
         3. the condition for the transition to fire is true, and 
405
         4. no higher-priority transition has completed (not <complete>) *)
406
   zz42 = ((zz40 = 6) and 
407
      ((
408
      (if ((zz177 = false) = false)
409
         then 0
410
         else 1) <> 0) and 
411
      (not zz37)));
412
413
   (* Beginning transition segment: trans16
414
      <fired> is true if the following are true: 
415
         1. the previous transition guard was true, 
416
         2. the source node for the transition is active, 
417
         3. the condition for the transition to fire is true, and 
418
         4. no higher-priority transition has completed (not <complete>) *)
419
   zz47 = ((zz45 = 5) and 
420
      ((
421
      (if ((zz171 = false) = false)
422
         then 0
423
         else 1) <> 0) and 
424
      (not zz43)));
425
426
   OK = ((zz58 = 4) or 
427
      ((zz58 = 5) or 
428
      (zz58 = 6)));
429
430
   zz63 = 
431
      (if (not 
432
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
433
         ((zz101 >= 3) and 
434
         (zz101 <= 6)))
435
         then 
436
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
437
               3
438
         else zz101);
439
440
   (* Beginning transition segment: trans18
441
      <fired> is true if the following are true: 
442
         1. the previous transition guard was true, 
443
         2. the source node for the transition is active, 
444
         3. the condition for the transition to fire is true, and 
445
         4. no higher-priority transition has completed (not <complete>) *)
446
   zz64 = ((not 
447
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
448
      ((zz101 >= 3) and 
449
      (zz101 <= 6))) and 
450
451
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
452
      ((zz63 >= 3) and 
453
      (zz63 <= 6)));
454
455
   (* Beginning transition segment: trans12
456
      <fired> is true if the following are true: 
457
         1. the previous transition guard was true, 
458
         2. the source node for the transition is active, 
459
         3. the condition for the transition to fire is true, and 
460
         4. no higher-priority transition has completed (not <complete>) *)
461
   zz116 = ((not 
462
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
463
      ((zz146 >= 2) and 
464
      (zz146 <= 8))) and 
465
466
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
467
      ((zz115 >= 2) and 
468
      (zz115 <= 8)));
469
470
   zz120 = 
471
      (if (zz142 = 1)
472
         then 
473
               (* <Exit state> path: Off maps to field: __root and value: 0 *)
474
               0
475
         else zz142);
476
477
   zz137 = 
478
      (if 
479
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
480
         ((zz156 >= 2) and 
481
         (zz156 <= 8))
482
         then 
483
               (* <Exit state> path: On maps to field: __root and value: 0 *)
484
               0
485
         else zz136);
486
487
   SP3c = true;
488
489
   zz171 = (zz170 = 20);
490
491
   (* Condition actions for transition segment: trans22: NONE
492
      Transition action(s) for transition: trans22
493
      <complete> is true if either: 
494
         1. this transition has completed, or 
495
         2. a higher-priority transition has already completed 
496
       *)
497
   zz105 = (zz104 or 
498
      zz100);
499
500
   zz127 = 
501
      (if (zz156 = 4)
502
         then 
503
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
504
               3
505
         else zz156);
506
507
   zz204 = cruiseThrottle;
508
509
   zz165 = (mode = 6);
510
511
   SP7 = ((not zz165) or 
512
      zz208);
513
514
   zz136 = 
515
      (if 
516
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
517
         ((zz156 >= 2) and 
518
         (zz156 <= 8))
519
         then zz123
520
         else zz135);
521
522
   (* Exit action(s) for transition: On_Init -> On_Active *)
523
   zz106 = 
524
      (if zz104
525
         then zz60
526
         else zz102);
527
528
   zz173 = (zz175 + 1);
529
530
   zz81 = 
531
      (if (zz147 = 4)
532
         then 
533
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
534
               3
535
         else zz147);
536
537
   zz181 = (carGear = 3);
538
539
   zz79 = 
540
      (if (zz84 = 6)
541
         then 
542
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
543
               3
544
         else zz84);
545
546
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
547
   zz38 = 
548
      (if zz36
549
         then zz14
550
         else zz34);
551
552
   (* Exit action(s) for transition: On -> On_Init: NONE
553
      Transition action(s) for transition: On -> On_Init: NONE
554
      Entry action(s) for transition: On -> On_Init *)
555
   zz119 = 
556
      (if zz116
557
         then zz114
558
         else zz143);
559
   (* Transition segment: trans12 complete. *)
560
561
   zz78 = 
562
      (if (not (zz89 = 8))
563
         then 3
564
         else zz148);
565
566
   zz15 = 
567
      (if (zz34 = 4)
568
         then false
569
         else zz33);
570
571
   zz83 = 
572
      (if 
573
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
574
         ((zz147 >= 3) and 
575
         (zz147 <= 6))
576
         then zz81
577
         else zz147);
578
579
   zz54 = 
580
      (if (not (zz55 = 4))
581
         then 4
582
         else zz103);
583
584
   zz192 = (zz211 > desiredSpeed);
585
586
   zz16 = 
587
      (if (not (zz32 = 5))
588
         then 
589
               (* <Enter state> path: On.Active.Increase maps to field: __root and value: 5 *)
590
               5
591
         else zz32);
592
593
   zz158 = (false -> (pre zz162));
594
595
   SP3a = ((not (not zz163)) or 
596
      (not zz199));
597
598
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
599
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
600
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
601
   zz67 = 
602
      (if zz64
603
         then zz62
604
         else zz98);
605
   (* Transition segment: trans18 complete. *)
606
607
   (* Condition actions for transition segment: trans17: NONE
608
      Transition action(s) for transition: trans17
609
      <complete> is true if either: 
610
         1. this transition has completed, or 
611
         2. a higher-priority transition has already completed 
612
       *)
613
   zz43 = (zz42 or 
614
      zz37);
615
616
   zz76 = 
617
      (if (zz91 = 8)
618
         then 
619
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
620
               2
621
         else zz91);
622
623
   zz80 = 
624
      (if (zz83 = 5)
625
         then 
626
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
627
               3
628
         else zz83);
629
630
   zz198 = (zz197 or 
631
      zz196);
632
633
   zz193 = (desiredSpeed <> 0.0);
634
635
   SP1 = ((not (not zz186)) or 
636
      zz187);
637
638
   zz231 = (cruiseThrottle <= 100.0);
639
640
   zz123 = 
641
      (if (zz135 = 8)
642
         then 
643
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
644
               2
645
         else zz135);
646
647
   zz19 = 
648
      (if (zz28 = 4)
649
         then false
650
         else zz27);
651
652
   (* Condition actions for transition segment: trans20: NONE
653
      Transition action(s) for transition: trans20
654
      <complete> is true if either: 
655
         1. this transition has completed, or 
656
         2. a higher-priority transition has already completed 
657
       *)
658
   zz94 = (zz93 or 
659
      zz88);
660
661
   cruiseThrottle = 
662
      (if zz201
663
         then zz226
664
         else 0.0);
665
666
   zz86 = 
667
      (if 
668
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
669
         ((zz147 >= 3) and 
670
         (zz147 <= 6))
671
         then 
672
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
673
               2
674
         else zz85);
675
676
   VRP1 = (zz232 and 
677
      zz231);
678
679
   zz131 = 
680
      (if 
681
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
682
         ((zz156 >= 3) and 
683
         (zz156 <= 6))
684
         then zz125
685
         else zz130);
686
687
   zz235 = (desiredSpeed < 0.0);
688
689
   SP9 = ((not zz214) or 
690
      zz215);
691
692
   zz138 = 
693
      (if 
694
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
695
         ((zz156 >= 2) and 
696
         (zz156 <= 8))
697
         then zz133
698
         else zz158);
699
700
   zz65 = ((zz66 = 4) or 
701
      ((zz66 = 5) or 
702
      (zz66 = 6)));
703
704
   zz194 = (desiredSpeed >= 15.0);
705
706
   zz197 = (mode = 1);
707
708
   VRP3 = (not zz237);
709
710
   zz6 = 
711
      (if (not (zz49 = 4))
712
         then 
713
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
714
               4
715
         else zz49);
716
717
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
718
   zz33 = 
719
      (if zz30
720
         then zz19
721
         else zz27);
722
723
   zz134 = 
724
      (if 
725
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
726
         ((zz156 >= 2) and 
727
         (zz156 <= 8))
728
         then zz132
729
         else zz156);
730
731
   zz61 = 
732
      (if (not (zz63 = 4))
733
         then 
734
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
735
               4
736
         else zz63);
737
738
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
739
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
740
   zz34 = 
741
      (if zz30
742
         then zz16
743
         else zz32);
744
   (* Transition segment: trans14 complete. *)
745
746
   (* Exit action(s) for transition: On -> Off *)
747
   zz141 = 
748
      (if zz139
749
         then zz138
750
         else zz158);
751
752
   (* Beginning transition segment: trans13
753
      <fired> is true if the following are true: 
754
         1. the previous transition guard was true, 
755
         2. the source node for the transition is active, 
756
         3. the condition for the transition to fire is true, and 
757
         4. no higher-priority transition has completed (not <complete>) *)
758
   zz139 = (
759
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
760
      ((zz156 >= 2) and 
761
      (zz156 <= 8)) and 
762
      (not onOff));
763
764
   zz178 = accelResume;
765
766
   zz234 = (desiredSpeed >= 0.0);
767
768
   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE
769
      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
770
   zz45 = 
771
      (if zz42
772
         then zz9
773
         else zz44);
774
   (* Transition segment: trans17 complete. *)
775
776
   zz121 = 
777
      (if (not (zz140 = 1))
778
         then 
779
               (* <Enter state> path: Off maps to field: __root and value: 1 *)
780
               1
781
         else zz140);
782
783
   zz184 = (true -> (pre zz183));
784
785
   (* Exit action(s) for transition: On -> On_Init: NONE
786
      Transition action(s) for transition: On -> On_Init: NONE
787
      Entry action(s) for transition: On -> On_Init *)
788
   zz118 = 
789
      (if zz116
790
         then zz113
791
         else zz115);
792
   (* Transition segment: trans12 complete. *)
793
794
   zz191 = (zz189 and 
795
      zz188);
796
797
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
798
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
799
   zz41 = 
800
      (if zz36
801
         then zz13
802
         else zz35);
803
   (* Transition segment: trans15 complete. *)
804
805
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
806
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
807
   zz35 = 
808
      (if zz30
809
         then zz17
810
         else zz29);
811
   (* Transition segment: trans14 complete. *)
812
813
   zz208 = (zz211 >= desiredSpeed);
814
815
   zz200 = (zz223 = 0.0);
816
817
   zz154 = 
818
      (if (not (zz156 = 1))
819
         then 1
820
         else zz157);
821
822
   zz73 = ((zz74 = 4) or 
823
      ((zz74 = 5) or 
824
      (zz74 = 6)));
825
826
   (* Transition action(s) for transition: On -> Off: NONE
827
      Entry action(s) for transition: On -> Off *)
828
   zz142 = 
829
      (if zz139
830
         then zz121
831
         else zz140);
832
   (* Transition segment: trans13 complete. *)
833
834
   zz124 = 
835
      (if (zz134 = 7)
836
         then 
837
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
838
               2
839
         else zz134);
840
841
   VRP4 = ((zz238 or 
842
      zz195) or 
843
      zz239);
844
845
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
846
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
847
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
848
   zz75 = 
849
      (if zz72
850
         then zz70
851
         else zz92);
852
   (* Transition segment: trans18 complete. *)
853
854
   zz233 = (desiredSpeed <= 100.0);
855
856
   zz223 = 
857
      (if zz217
858
         then zz2
859
         else zz218);
860
861
   zz185 = ((not zz184) and 
862
      zz183);
863
864
   zz180 = ((not zz179) and 
865
      zz178);
866
867
   zz239 = (desiredSpeed = carSpeed);
868
869
   (* Transition action(s) for transition: Off -> On: NONE
870
      Entry action(s) for transition: Off -> On *)
871
   zz148 = 
872
      (if zz144
873
         then zz119
874
         else zz143);
875
   (* Transition segment: trans23 complete. *)
876
877
   zz115 = 
878
      (if (not 
879
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
880
         ((zz146 >= 2) and 
881
         (zz146 <= 8)))
882
         then 
883
               (* <Enter state> path: On maps to field: __root and value: 2 *)
884
               2
885
         else zz146);
886
887
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
888
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
889
   zz40 = 
890
      (if zz36
891
         then zz12
892
         else zz38);
893
   (* Transition segment: trans15 complete. *)
894
895
   (* Exit action(s) for transition: On -> Off *)
896
   zz140 = 
897
      (if zz139
898
         then zz137
899
         else zz156);
900
901
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
902
   zz39 = 
903
      (if zz36
904
         then zz15
905
         else zz33);
906
907
   zz8 = 
908
      (if (zz45 = 5)
909
         then 
910
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
911
               3
912
         else zz45);
913
914
   zz122 = 
915
      (if (not (zz140 = 1))
916
         then 1
917
         else zz157);
918
919
   zz179 = (true -> (pre zz178));
920
921
   zz82 = 
922
      (if (zz147 = 4)
923
         then false
924
         else zz141);
925
926
   zz203 = (zz201 or 
927
      zz202);
928
929
   zz186 = (((((not cancel) and 
930
      (not brakePedal)) and 
931
      zz181) and 
932
      zz182) and 
933
      validInputs);
934
935
   zz183 = decelSet;
936
937
   zz155 = (true -> 
938
      (if (pre SP3c)
939
         then false
940
         else (pre zz155)));
941
942
   zz196 = (mode = 2);
943
944
   zz161 = zz160;
945
946
   zz9 = 
947
      (if (not (zz44 = 4))
948
         then 
949
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
950
               4
951
         else zz44);
952
953
   (* Transition action(s) for transition: On_Inactive -> On_Active *)
954
   zz96 = 
955
      (if zz93
956
         then true
957
         else zz90);
958
959
   zz52 = 
960
      (if ((not zz48) and 
961
         (zz50 = 4))
962
         then false
963
         else zz39);
964
965
   zz0 = zz217;
966
967
   zz2 = (
968
      (if (zz1 and 
969
         (not zz0))
970
         then 0.0
971
         else (zz222 + 0.05)) -> 
972
      (if (zz1 and 
973
         (not zz0))
974
         then 0.0
975
         else 
976
      (if zz0
977
         then (zz222 + 0.05)
978
         else (pre zz2))));
979
980
   zz1 = (true -> 
981
      (if (pre zz0)
982
         then false
983
         else (pre zz1)));
984
985
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
986
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
987
   zz51 = 
988
      (if zz47
989
         then zz7
990
         else zz46);
991
   (* Transition segment: trans16 complete. *)
992
993
   zz162 = 
994
      (if SP3c
995
         then 
996
               (if zz155
997
                  then zz158
998
                  else zz151)
999
         else zz158);
1000
1001
   (* Condition actions for transition segment: trans19: NONE
1002
      Transition action(s) for transition: trans19
1003
      <complete> is true if either: 
1004
         1. this transition has completed, or 
1005
         2. a higher-priority transition has already completed 
1006
       *)
1007
   zz100 = (zz99 or 
1008
      zz94);
1009
1010
   zz53 = 
1011
      (if (not (zz55 = 4))
1012
         then 
1013
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1014
               4
1015
         else zz55);
1016
1017
   zz188 = (desiredSpeed <> 100.0);
1018
1019
   SP10 = ((not zz191) or 
1020
      zz192);
1021
1022
   zz13 = 
1023
      (if (not (zz38 = 6))
1024
         then 5
1025
         else zz35);
1026
1027
   zz201 = ((zz163 or 
1028
      zz164) or 
1029
      zz165);
1030
1031
   zz14 = 
1032
      (if (zz34 = 4)
1033
         then 
1034
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1035
               3
1036
         else zz34);
1037
1038
   zz126 = 
1039
      (if (zz129 = 5)
1040
         then 
1041
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
1042
               3
1043
         else zz129);
1044
1045
   (* Exit action(s) for outer loop transition: On_Active_Maintain *)
1046
   zz26 = 
1047
      (if zz24
1048
         then zz23
1049
         else zz107);
1050
1051
   (* Exit action(s) for transition: Off -> On *)
1052
   zz146 = 
1053
      (if zz144
1054
         then zz120
1055
         else zz142);
1056
1057
   zz199 = (
1058
      (if (zz162 = false)
1059
         then 0.0
1060
         else 1.0) = 1.0);
1061
1062
   zz227 = (desiredSpeed - carSpeed);
1063
1064
   zz150 = 
1065
      (if ((not zz145) and 
1066
1067
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1068
         ((zz147 >= 2) and 
1069
         (zz147 <= 8)))
1070
         then zz111
1071
         else zz148);
1072
1073
   zz177 = (zz176 = 20);
1074
1075
   (* Transition action(s) for outer loop transition: On_Active_Maintain *)
1076
   zz27 = 
1077
      (if zz24
1078
         then true
1079
         else zz26);
1080
1081
   (* Entry action(s) for transition: On_Inactive -> On_Active *)
1082
   zz97 = 
1083
      (if zz93
1084
         then zz74
1085
         else zz95);
1086
   (* Transition segment: trans20 complete. *)
1087
1088
   zz195 = (desiredSpeed = 0.0);
1089
1090
   zz71 = 
1091
      (if (not 
1092
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1093
         ((zz95 >= 3) and 
1094
         (zz95 <= 6)))
1095
         then 
1096
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1097
               3
1098
         else zz95);
1099
1100
   zz62 = 
1101
      (if (not (zz63 = 4))
1102
         then 4
1103
         else zz98);
1104
1105
   zz229 = 
1106
      (if (zz228 < ( -10.0))
1107
         then ( -10.0)
1108
         else 
1109
      (if (zz228 > 10.0)
1110
         then 10.0
1111
         else zz228));
1112
1113
   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE
1114
      Entry action(s) for transition: On_Inactive -> On_Active *)
1115
   zz103 = 
1116
      (if zz99
1117
         then zz67
1118
         else zz98);
1119
   (* Transition segment: trans19 complete. *)
1120
1121
   zz55 = 
1122
      (if (not 
1123
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1124
         ((zz106 >= 3) and 
1125
         (zz106 <= 6)))
1126
         then 
1127
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1128
               3
1129
         else zz106);
1130
1131
   (* Beginning transition segment: trans18
1132
      <fired> is true if the following are true: 
1133
         1. the previous transition guard was true, 
1134
         2. the source node for the transition is active, 
1135
         3. the condition for the transition to fire is true, and 
1136
         4. no higher-priority transition has completed (not <complete>) *)
1137
   zz56 = ((not 
1138
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1139
      ((zz106 >= 3) and 
1140
      (zz106 <= 6))) and 
1141
1142
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1143
      ((zz55 >= 3) and 
1144
      (zz55 <= 6)));
1145
1146
   (* Beginning transition segment: trans18
1147
      <fired> is true if the following are true: 
1148
         1. the previous transition guard was true, 
1149
         2. the source node for the transition is active, 
1150
         3. the condition for the transition to fire is true, and 
1151
         4. no higher-priority transition has completed (not <complete>) *)
1152
   zz72 = ((not 
1153
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1154
      ((zz95 >= 3) and 
1155
      (zz95 <= 6))) and 
1156
1157
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1158
      ((zz71 >= 3) and 
1159
      (zz71 <= 6)));
1160
1161
   (* Transition action(s) for transition: On_Active -> On_Inactive: NONE
1162
      Entry action(s) for transition: On_Active -> On_Inactive *)
1163
   zz91 = 
1164
      (if zz88
1165
         then zz77
1166
         else zz89);
1167
   (* Transition segment: trans21 complete. *)
1168
1169
   zz202 = (mode = 3);
1170
1171
   zz221 = 
1172
      (if zz162
1173
         then carSpeed
1174
         else zz223);
1175
1176
   SP2 = ((not (not zz201)) or 
1177
      zz187);
1178
1179
   (* Entry action(s) for transition: On_Init -> On_Active *)
1180
   zz108 = 
1181
      (if zz104
1182
         then zz58
1183
         else zz106);
1184
   (* Transition segment: trans22 complete. *)
1185
1186
   zz238 = (desiredSpeed = zz211);
1187
1188
   zz212 = (zz211 = desiredSpeed);
1189
1190
   (* Beginning transition segment: trans21
1191
      <fired> is true if the following are true: 
1192
         1. the previous transition guard was true, 
1193
         2. the source node for the transition is active, 
1194
         3. the condition for the transition to fire is true, and 
1195
         4. no higher-priority transition has completed (not <complete>) *)
1196
   zz88 = (
1197
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1198
      ((zz147 >= 3) and 
1199
      (zz147 <= 6)) and 
1200
      (not zz186));
1201
1202
   (* Condition actions for transition segment: trans16: NONE
1203
      Transition action(s) for transition: trans16
1204
      <complete> is true if either: 
1205
         1. this transition has completed, or 
1206
         2. a higher-priority transition has already completed 
1207
       *)
1208
   zz48 = (zz47 or 
1209
      zz43);
1210
1211
   SP4 = ((not zz203) or 
1212
      zz194);
1213
1214
   zz149 = 
1215
      (if ((not zz145) and 
1216
1217
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1218
         ((zz147 >= 2) and 
1219
         (zz147 <= 8)))
1220
         then zz110
1221
         else zz147);
1222
1223
   zz132 = 
1224
      (if 
1225
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1226
         ((zz156 >= 3) and 
1227
         (zz156 <= 6))
1228
         then 
1229
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
1230
               2
1231
         else zz131);
1232
1233
   zz112 = 
1234
      (if ((not zz105) and 
1235
1236
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1237
         ((zz108 >= 3) and 
1238
         (zz108 <= 6)))
1239
         then zz52
1240
         else zz107);
1241
1242
   (* Exit action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
1243
   zz44 = 
1244
      (if zz42
1245
         then zz11
1246
         else zz40);
1247
1248
   zz215 = (zz211 < desiredSpeed);
1249
1250
   zz236 = (desiredSpeed > 0.0);
1251
1252
   zz113 = 
1253
      (if (not (zz115 = 7))
1254
         then 
1255
               (* <Enter state> path: On.Init maps to field: __root and value: 7 *)
1256
               7
1257
         else zz115);
1258
1259
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
1260
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
1261
   zz50 = 
1262
      (if zz47
1263
         then zz6
1264
         else zz49);
1265
   (* Transition segment: trans16 complete. *)
1266
1267
   (* Exit action(s) for transition: On_Inactive -> On_Active *)
1268
   zz95 = 
1269
      (if zz93
1270
         then zz76
1271
         else zz91);
1272
1273
   zz3 = zz216;
1274
1275
   zz5 = (
1276
      (if (zz4 and 
1277
         (not zz3))
1278
         then 0.0
1279
         else (zz222 - 0.05)) -> 
1280
      (if (zz4 and 
1281
         (not zz3))
1282
         then 0.0
1283
         else 
1284
      (if zz3
1285
         then (zz222 - 0.05)
1286
         else (pre zz5))));
1287
1288
   zz4 = (true -> 
1289
      (if (pre zz3)
1290
         then false
1291
         else (pre zz4)));
1292
1293
   zz60 = 
1294
      (if (zz102 = 7)
1295
         then 
1296
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
1297
               2
1298
         else zz102);
1299
1300
   (* Entry action(s) for transition: On_Init -> On_Active *)
1301
   zz109 = 
1302
      (if zz104
1303
         then zz59
1304
         else zz103);
1305
   (* Transition segment: trans22 complete. *)
1306
1307
   zz205 = (0.0 -> (pre zz204));
1308
1309
   zz209 = zz163;
1310
1311
   zz216 = zz164;
1312
1313
   zz217 = zz165;
1314
1315
   zz117 = (
1316
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1317
      ((zz118 >= 3) and 
1318
      (zz118 <= 6)) or 
1319
      ((zz118 = 7) or 
1320
      (zz118 = 8)));
1321
1322
   zz70 = 
1323
      (if (not (zz71 = 4))
1324
         then 4
1325
         else zz92);
1326
1327
   zz22 = 
1328
      (if (zz108 = 4)
1329
         then 
1330
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1331
               3
1332
         else zz108);
1333
1334
   zz160 = 
1335
      (if SP3c
1336
         then 
1337
               (if zz155
1338
                  then zz153
1339
                  else zz149)
1340
         else zz156);
1341
1342
   VRP2 = (zz234 and 
1343
      zz233);
1344
1345
   zz153 = 
1346
      (if (not (zz156 = 1))
1347
         then 
1348
               (* <Enter state> path: Off maps to field: __root and value: 1 *)
1349
               1
1350
         else zz156);
1351
1352
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1353
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1354
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1355
   zz58 = 
1356
      (if zz56
1357
         then zz53
1358
         else zz55);
1359
   (* Transition segment: trans18 complete. *)
1360
1361
   (* Beginning transition segment: trans23
1362
      <fired> is true if the following are true: 
1363
         1. the previous transition guard was true, 
1364
         2. the source node for the transition is active, 
1365
         3. the condition for the transition to fire is true, and 
1366
         4. no higher-priority transition has completed (not <complete>) *)
1367
   zz144 = ((zz142 = 1) and 
1368
      (onOff and 
1369
      (not zz139)));
1370
1371
   (* Condition actions for transition segment: trans15: NONE
1372
      Transition action(s) for transition: trans15
1373
      <complete> is true if either: 
1374
         1. this transition has completed, or 
1375
         2. a higher-priority transition has already completed 
1376
       *)
1377
   zz37 = (zz36 or 
1378
      zz31);
1379
1380
   zz222 = (0.0 -> (pre desiredSpeed));
1381
1382
   zz228 = (zz227 * 1.0);
1383
1384
   zz68 = 
1385
      (if (zz97 = 8)
1386
         then 
1387
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
1388
               2
1389
         else zz97);
1390
1391
   zz125 = 
1392
      (if (zz130 = 6)
1393
         then 
1394
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
1395
               3
1396
         else zz130);
1397
1398
   zz170 = 
1399
      (if (zz166 <= 20)
1400
         then zz166
1401
         else 20);
1402
1403
   zz167 = (zz169 + 1);
1404
1405
   zz11 = 
1406
      (if (zz40 = 6)
1407
         then 
1408
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
1409
               3
1410
         else zz40);
1411
1412
   zz163 = (mode = 4);
1413
1414
   zz187 = (cruiseThrottle = 0.0);
1415
1416
   zz129 = 
1417
      (if 
1418
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1419
         ((zz156 >= 3) and 
1420
         (zz156 <= 6))
1421
         then zz127
1422
         else zz156);
1423
1424
   (* Exit action(s) for transition: On_Active -> On_Inactive *)
1425
   zz90 = 
1426
      (if zz88
1427
         then zz87
1428
         else zz141);
1429
1430
   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE
1431
      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
1432
   zz46 = 
1433
      (if zz42
1434
         then zz10
1435
         else zz41);
1436
   (* Transition segment: trans17 complete. *)
1437
1438
   (* Entry action(s) for transition: On_Inactive -> On_Active *)
1439
   zz98 = 
1440
      (if zz93
1441
         then zz75
1442
         else zz92);
1443
   (* Transition segment: trans20 complete. *)
1444
1445
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
1446
   zz32 = 
1447
      (if zz30
1448
         then zz18
1449
         else zz28);
1450
1451
   zz225 = (zz230 + zz224);
1452
1453
   zz190 = desiredSpeed;
1454
1455
   zz207 = (zz211 <= desiredSpeed);
1456
1457
   (* Exit action(s) for outer loop transition: On_Active_Maintain *)
1458
   zz25 = 
1459
      (if zz24
1460
         then zz22
1461
         else zz108);
1462
1463
   mode = 
1464
      (if SP3c
1465
         then 
1466
               (if zz155
1467
                  then zz154
1468
                  else zz150)
1469
         else zz157);
1470
1471
   SP5 = ((not zz163) or 
1472
      zz206);
1473
1474
   zz135 = 
1475
      (if 
1476
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1477
         ((zz156 >= 2) and 
1478
         (zz156 <= 8))
1479
         then zz124
1480
         else zz134);
1481
1482
   zz111 = 
1483
      (if ((not zz105) and 
1484
1485
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1486
         ((zz108 >= 3) and 
1487
         (zz108 <= 6)))
1488
         then zz51
1489
         else zz109);
1490
1491
   SP3b = ((not zz198) or 
1492
      zz200);
1493
1494
   (* Transition action(s) for transition: On -> Off: NONE
1495
      Entry action(s) for transition: On -> Off *)
1496
   zz143 = 
1497
      (if zz139
1498
         then zz122
1499
         else zz157);
1500
   (* Transition segment: trans13 complete. *)
1501
1502
   zz219 = 
1503
      (if zz202
1504
         then zz222
1505
         else 0.0);
1506
1507
   zz23 = 
1508
      (if (zz108 = 4)
1509
         then false
1510
         else zz107);
1511
1512
   (* Condition actions for transition segment: trans23: NONE
1513
      Transition action(s) for transition: trans23
1514
      <complete> is true if either: 
1515
         1. this transition has completed, or 
1516
         2. a higher-priority transition has already completed 
1517
       *)
1518
   zz145 = (zz144 or 
1519
      zz139);
1520
1521
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1522
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1523
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1524
   zz66 = 
1525
      (if zz64
1526
         then zz61
1527
         else zz63);
1528
   (* Transition segment: trans18 complete. *)
1529
1530
   SP3 = ((not zz198) or 
1531
      zz195);
1532
1533
   zz232 = (cruiseThrottle >= 0.0);
1534
1535
   zz110 = 
1536
      (if ((not zz105) and 
1537
1538
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1539
         ((zz108 >= 3) and 
1540
         (zz108 <= 6)))
1541
         then zz50
1542
         else zz108);
1543
1544
   zz152 = ((zz153 = 1) or 
1545
1546
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1547
      ((zz153 >= 2) and 
1548
      (zz153 <= 8)));
1549
1550
   (* Transition action(s) for transition: On_Init -> On_Active *)
1551
   zz107 = 
1552
      (if zz104
1553
         then true
1554
         else zz96);
1555
1556
   (* Exit action(s) for transition: On_Active -> On_Inactive *)
1557
   zz89 = 
1558
      (if zz88
1559
         then zz86
1560
         else zz147);
1561
1562
   SP11 = ((not zz193) or 
1563
      zz194);
1564
1565
   zz220 = 
1566
      (if zz163
1567
         then zz222
1568
         else zz219);
1569
1570
   zz21 = 
1571
      (if (not (zz25 = 4))
1572
         then 4
1573
         else zz109);
1574
1575
   zz213 = (false -> (pre zz216));
1576
1577
   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE
1578
      Entry action(s) for transition: On_Inactive -> On_Active *)
1579
   zz102 = 
1580
      (if zz99
1581
         then zz66
1582
         else zz101);
1583
   (* Transition segment: trans19 complete. *)
1584
1585
   zz176 = 
1586
      (if (zz172 <= 20)
1587
         then zz172
1588
         else 20);
1589
1590
   zz130 = 
1591
      (if 
1592
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1593
         ((zz156 >= 3) and 
1594
         (zz156 <= 6))
1595
         then zz126
1596
         else zz129);
1597
1598
   zz237 = (zz236 and 
1599
      zz235);
1600
1601
   (* Exit action(s) for transition: On_Inactive -> On_Active *)
1602
   zz101 = 
1603
      (if zz99
1604
         then zz68
1605
         else zz97);
1606
1607
   zz164 = (mode = 5);
1608
1609
   zz17 = 
1610
      (if (not (zz32 = 5))
1611
         then 6
1612
         else zz29);
1613
1614
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1615
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1616
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1617
   zz74 = 
1618
      (if zz72
1619
         then zz69
1620
         else zz71);
1621
   (* Transition segment: trans18 complete. *)
1622
1623
   zz230 = (zz229 / 20.0);
1624
1625
   CP8a = ((not zz162) or 
1626
      zz201);
1627
1628
   zz133 = 
1629
      (if 
1630
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1631
         ((zz156 >= 3) and 
1632
         (zz156 <= 6))
1633
         then zz128
1634
         else zz158);
1635
1636
   SP6 = ((not zz164) or 
1637
      zz207);
1638
1639
   zz151 = 
1640
      (if ((not zz145) and 
1641
1642
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1643
         ((zz147 >= 2) and 
1644
         (zz147 <= 8)))
1645
         then zz112
1646
         else zz141);
1647
1648
   zz189 = (false -> (pre zz217));
1649
1650
   zz214 = (zz213 and 
1651
      zz193);
1652
1653
   (* Entry action(s) for outer loop transition: On_Active_Maintain *)
1654
   zz28 = 
1655
      (if zz24
1656
         then zz20
1657
         else zz25);
1658
   (* Transition segment: trans24 complete. *)
1659
1660
   zz206 = (zz205 = cruiseThrottle);
1661
1662
   zz12 = 
1663
      (if (not (zz38 = 6))
1664
         then 
1665
               (* <Enter state> path: On.Active.Decrease maps to field: __root and value: 6 *)
1666
               6
1667
         else zz38);
1668
1669
   zz224 = (0.0 -> (pre cruiseThrottle));
1670
1671
   zz87 = 
1672
      (if 
1673
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1674
         ((zz147 >= 3) and 
1675
         (zz147 <= 6))
1676
         then zz82
1677
         else zz141);
1678
1679
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
1680
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
1681
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
1682
   zz59 = 
1683
      (if zz56
1684
         then zz54
1685
         else zz103);
1686
   (* Transition segment: trans18 complete. *)
1687
1688
   zz128 = 
1689
      (if (zz156 = 4)
1690
         then false
1691
         else zz158);
1692
1693
   (* Transition action(s) for transition: Off -> On: NONE
1694
      Entry action(s) for transition: Off -> On *)
1695
   zz147 = 
1696
      (if zz144
1697
         then zz118
1698
         else zz146);
1699
   (* Transition segment: trans23 complete. *)
1700
1701
   SP8 = ((not zz210) or 
1702
      zz212);
1703
1704
   zz7 = 
1705
      (if (not (zz49 = 4))
1706
         then 4
1707
         else zz46);
1708
1709
   desiredSpeed = 
1710
      (if (zz221 < 0.0)
1711
         then 0.0
1712
         else 
1713
      (if (zz221 > 100.0)
1714
         then 100.0
1715
         else zz221));
1716
1717
   (* Entry action(s) for outer loop transition: On_Active_Maintain *)
1718
   zz29 = 
1719
      (if zz24
1720
         then zz21
1721
         else zz109);
1722
   (* Transition segment: trans24 complete. *)
1723
1724
   zz18 = 
1725
      (if (zz28 = 4)
1726
         then 
1727
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1728
               3
1729
         else zz28);
1730
1731
   zz114 = 
1732
      (if (not (zz115 = 7))
1733
         then 2
1734
         else zz143);
1735
1736
   zz211 = (0.0 -> (pre zz190));
1737
1738
   zz226 = 
1739
      (if (zz225 < 0.0)
1740
         then 0.0
1741
         else 
1742
      (if (zz225 > 100.0)
1743
         then 100.0
1744
         else zz225));
1745
1746
   zz69 = 
1747
      (if (not (zz71 = 4))
1748
         then 
1749
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1750
               4
1751
         else zz71);
1752
1753
   zz20 = 
1754
      (if (not (zz25 = 4))
1755
         then 
1756
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1757
               4
1758
         else zz25);
1759
1760
   (* Condition actions for transition segment: trans14: NONE
1761
      Transition action(s) for transition: trans14
1762
      <complete> is true if either: 
1763
         1. this transition has completed, or 
1764
         2. a higher-priority transition has already completed 
1765
       *)
1766
   zz31 = (zz30 or 
1767
      zz24);
1768
1769
   zz218 = 
1770
      (if zz216
1771
         then zz5
1772
         else zz220);
1773
1774
   zz10 = 
1775
      (if (not (zz44 = 4))
1776
         then 4
1777
         else zz41);
1778
1779
   zz77 = 
1780
      (if (not (zz89 = 8))
1781
         then 
1782
               (* <Enter state> path: On.Inactive maps to field: __root and value: 8 *)
1783
               8
1784
         else zz89);
1785
1786
   (* Transition action(s) for transition: On_Active -> On_Inactive: NONE
1787
      Entry action(s) for transition: On_Active -> On_Inactive *)
1788
   zz92 = 
1789
      (if zz88
1790
         then zz78
1791
         else zz148);
1792
   (* Transition segment: trans21 complete. *)
1793
1794
   zz182 = (carSpeed >= 15.0);
1795
1796
   zz210 = (false -> (pre zz209));
1797
1798
   zz85 = 
1799
      (if 
1800
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1801
         ((zz147 >= 3) and 
1802
         (zz147 <= 6))
1803
         then zz79
1804
         else zz84);
1805
1806
   zz84 = 
1807
      (if 
1808
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1809
         ((zz147 >= 3) and 
1810
         (zz147 <= 6))
1811
         then zz80
1812
         else zz83);
1813
1814
   (* Exit action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
1815
   zz49 = 
1816
      (if zz47
1817
         then zz8
1818
         else zz45);
1819
1820
  --%PROPERTY OK;
1821
--   --%PROPERTY zz65;
1822
--   --%PROPERTY zz73;
1823
--   --%PROPERTY zz117;
1824
--   --%PROPERTY zz152;
1825
--   --%PROPERTY       VRP1;
1826
--   --%PROPERTY       VRP2;
1827
--   --%PROPERTY       CP8a;
1828
--   --%PROPERTY       VRP3;
1829
--   --%PROPERTY       VRP4;
1830
--   --%PROPERTY       SP4;
1831
--   --%PROPERTY       SP5;
1832
--   --%PROPERTY       SP6;
1833
--   --%PROPERTY       SP7;
1834
--   --%PROPERTY       SP3b;
1835
--   --%PROPERTY       SP3c;
1836
--   --%PROPERTY       SP3;
1837
--   --%PROPERTY       SP3a;
1838
--   --%PROPERTY       SP2;
1839
--   --%PROPERTY       SP1;
1840
--   --%PROPERTY       SP8;
1841
--   --%PROPERTY       SP9;
1842
--   --%PROPERTY       SP10;
1843
--   --%PROPERTY       SP11;
1844
1845
--   check OK; 
1846
1847
--   check zz65; 
1848
1849
--   check zz73; 
1850
1851
--   check zz117; 
1852
1853
--   check zz152;
1854
1855
tel;
1856