Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (44.2 KB)

1

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

    
11
var
12
   mode: int ; 
13
      cruiseThrottle: real; 
14
      desiredSpeed: real; 
15
      VRP1: bool; 
16
      VRP2: bool; 
17
      CP8a: bool; 
18
      VRP3: bool; 
19
      VRP4: bool; 
20
      SP4: 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
   zz118: int ; 
152
   zz119: int ; 
153
   zz120: int ; 
154
   zz121: int ; 
155
   zz122: int ; 
156
   zz123: int ; 
157
   zz124: int ; 
158
   zz125: int ; 
159
   zz126: int ; 
160
   zz127: int ; 
161
   zz128: bool; 
162
   zz129: int ; 
163
   zz130: int ; 
164
   zz131: int ; 
165
   zz132: int ; 
166
   zz133: bool; 
167
   zz134: int ; 
168
   zz135: int ; 
169
   zz136: int ; 
170
   zz137: int ; 
171
   zz138: bool; 
172
   zz139: bool; 
173
   zz140: int ; 
174
   zz141: bool; 
175
   zz142: int ; 
176
   zz143: int ; 
177
   zz144: bool; 
178
   zz145: bool; 
179
   zz146: int ; 
180
   zz147: int ; 
181
   zz148: int ; 
182
   zz149: int ; 
183
   zz150: int ; 
184
   zz151: bool; 
185
   zz152: bool; 
186
   zz153: int ; 
187
   zz154: int ; 
188
   zz155: bool; 
189
   zz156: int ; 
190
   zz157: int ; 
191
   zz158: bool; 
192
   zz159: int ; 
193
   zz160: int ; 
194
   zz161: int ; 
195
   zz162: bool; 
196
   zz163: bool; 
197
   zz164: bool; 
198
   zz165: bool; 
199
   zz166: int ; 
200
   zz167: int ; 
201
   zz168: int ; 
202
   zz169: int ; 
203
   zz170: int ; 
204
   zz171: bool; 
205
   zz172: int ; 
206
   zz173: int ; 
207
   zz174: int ; 
208
   zz175: int ; 
209
   zz176: int ; 
210
   zz177: bool; 
211
   zz178: bool; 
212
   zz179: bool; 
213
   zz180: bool; 
214
   zz181: bool; 
215
   zz182: bool; 
216
   zz183: bool; 
217
   zz184: bool; 
218
   zz185: bool; 
219
   zz186: bool; 
220
   zz187: bool; 
221
   zz188: bool; 
222
   zz189: bool; 
223
   zz190: real; 
224
   zz191: bool; 
225
   zz192: bool; 
226
   zz193: bool; 
227
   zz194: bool; 
228
   zz195: bool; 
229
   zz196: bool; 
230
   zz197: bool; 
231
   zz198: bool; 
232
   zz199: bool; 
233
   zz200: bool; 
234
   zz201: bool; 
235
   zz202: bool; 
236
   zz203: bool; 
237
   zz204: real; 
238
   zz205: real; 
239
   zz206: bool; 
240
   zz207: bool; 
241
   zz208: bool; 
242
   zz209: bool; 
243
   zz210: bool; 
244
   zz211: real; 
245
   zz212: bool; 
246
   zz213: bool; 
247
   zz214: bool; 
248
   zz215: bool; 
249
   zz216: bool; 
250
   zz217: bool; 
251
   zz218: real; 
252
   zz219: real; 
253
   zz220: real; 
254
   zz221: real; 
255
   zz222: real; 
256
   zz223: real; 
257
   zz224: real; 
258
   zz225: real; 
259
   zz226: real; 
260
   zz227: real; 
261
   zz228: real; 
262
   zz229: real; 
263
   zz230: real; 
264
   zz231: bool; 
265
   zz232: bool; 
266
   zz233: bool; 
267
   zz234: bool; 
268
   zz235: bool; 
269
   zz236: bool; 
270
   zz237: bool; 
271
   zz238: bool; 
272
   zz239: bool;
273

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
484
   SP3c = true;
485

    
486
   zz171 = (zz170 = 20);
487

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

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

    
504
   zz204 = cruiseThrottle;
505

    
506
   zz165 = (mode = 6);
507

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

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

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

    
525
   zz173 = (zz175 + 1);
526

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

    
534
   zz181 = (carGear = 3);
535

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

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

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

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

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

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

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

    
581
   zz192 = (zz211 > desiredSpeed);
582

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

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

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

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

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

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

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

    
627
   zz198 = (zz197 or 
628
      zz196);
629

    
630
   zz193 = (desiredSpeed <> 0.0);
631

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

    
635
   zz231 = (cruiseThrottle <= 100.0);
636

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

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

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

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

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

    
673
   VRP1 = (zz232 and 
674
      zz231);
675

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

    
684
   zz235 = (desiredSpeed < 0.0);
685

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

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

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

    
701
   zz194 = (desiredSpeed >= 15.0);
702

    
703
   zz197 = (mode = 1);
704

    
705
   VRP3 = (not zz237);
706

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

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

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

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

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

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

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

    
761
   zz178 = accelResume;
762

    
763
   zz234 = (desiredSpeed >= 0.0);
764

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

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

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

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

    
791
   zz191 = (zz189 and 
792
      zz188);
793

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

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

    
810
   zz208 = (zz211 >= desiredSpeed);
811

    
812
   zz200 = (zz223 = 0.0);
813

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

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

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

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

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

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

    
851
   zz233 = (desiredSpeed <= 100.0);
852

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

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

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

    
864
   zz239 = (desiredSpeed = carSpeed);
865

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

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

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

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

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

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

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

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

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

    
923
   zz203 = (zz201 or 
924
      zz202);
925

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

    
932
   zz183 = decelSet;
933

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

    
939
   zz196 = (mode = 2);
940

    
941
   zz161 = zz160;
942

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

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

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

    
962
   zz0 = zz217;
963

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

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

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

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

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

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

    
1014
   zz188 = (desiredSpeed <> 100.0);
1015

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

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

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

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

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

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

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

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

    
1059
   zz227 = (desiredSpeed - carSpeed);
1060

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

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

    
1070
   zz177 = (zz176 = 20);
1071

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

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

    
1085
   zz195 = (desiredSpeed = 0.0);
1086

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

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

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

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

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

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

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

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

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

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

    
1166
   zz202 = (mode = 3);
1167

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

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

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

    
1183
   zz238 = (desiredSpeed = zz211);
1184

    
1185
   zz212 = (zz211 = desiredSpeed);
1186

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

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

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

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

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

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

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

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

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

    
1245
   zz215 = (zz211 < desiredSpeed);
1246

    
1247
   zz236 = (desiredSpeed > 0.0);
1248

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

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

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

    
1270
   zz3 = zz216;
1271

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

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

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

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

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

    
1306
   zz209 = zz163;
1307

    
1308
   zz216 = zz164;
1309

    
1310
   zz217 = zz165;
1311

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

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

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

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

    
1339
   VRP2 = (zz234 and 
1340
      zz233);
1341

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

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

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

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

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

    
1379
   zz228 = (zz227 * 1.0);
1380

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

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

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

    
1400
   zz167 = (zz169 + 1);
1401

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

    
1409
   zz163 = (mode = 4);
1410

    
1411
   zz187 = (cruiseThrottle = 0.0);
1412

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

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

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

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

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

    
1448
   zz225 = (zz230 + zz224);
1449

    
1450
   zz190 = desiredSpeed;
1451

    
1452
   zz207 = (zz211 <= desiredSpeed);
1453

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1530
   zz232 = (cruiseThrottle >= 0.0);
1531

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

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

    
1541
   zz152 = ((zz153 = 1) or 
1542

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

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

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

    
1559
   SP11 = ((not zz193) or 
1560
      zz194);
1561

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

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

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

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

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

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

    
1595
   zz237 = (zz236 and 
1596
      zz235);
1597

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

    
1604
   zz164 = (mode = 5);
1605

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

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

    
1620
   zz230 = (zz229 / 20.0);
1621

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

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

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

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

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

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

    
1647
   zz214 = (zz213 and 
1648
      zz193);
1649

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

    
1657
   zz206 = (zz205 = cruiseThrottle);
1658

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1791
   zz182 = (carSpeed >= 15.0);
1792

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

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

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

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

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

    
1842
--   check zz57; 
1843

    
1844
--   check zz65; 
1845

    
1846
--   check zz73; 
1847

    
1848
--   check OK; 
1849

    
1850
--   check zz152;
1851

    
1852
tel;
1853

    
1854