Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / large / ccp11.lus @ 22fe1c93

History | View | Annotate | Download (44.2 KB)

1 22fe1c93 ploc
2
3
node top(onOff: bool; 
4
      decelSet: bool; 
5
      accelResume: bool; 
6
      cancel: bool; 
7
      brakePedal: bool; 
8
      carGear: int ; 
9
      carSpeed: real; 
10
      validInputs: bool) returns (OK: bool);
11
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
      SP5: bool; 
22
      SP6: bool; 
23
      SP7: bool; 
24
      SP3b: bool; 
25
      SP3c: bool; 
26
      SP3: bool; 
27
      SP3a: bool; 
28
      SP2: bool; 
29
      SP1: bool; 
30
      SP8: bool; 
31
      SP9: bool; 
32
      SP10: bool; 
33
      SP11: 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
   OK = ((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
   SP11 = ((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       OK;
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       SP11;
1842
1843
--   check zz57; 
1844
1845
--   check zz65; 
1846
1847
--   check zz73; 
1848
1849
--   check zz117; 
1850
1851
--   check zz152;
1852
1853
tel;
1854