Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (44.2 KB)

1

    
2

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

    
13
var
14
mode: int ; 
15
      cruiseThrottle: real; 
16
      desiredSpeed: real; 
17
      VRP1: bool; 
18
      CP8a: bool; 
19
      VRP3: bool; 
20
      VRP4: bool; 
21
      SP4: bool; 
22
      SP5: bool; 
23
      SP6: bool; 
24
      SP7: bool; 
25
      SP3b: bool; 
26
      SP3c: bool; 
27
      SP3: bool; 
28
      SP3a: bool; 
29
      SP2: bool; 
30
      SP1: bool; 
31
      SP8: bool; 
32
      SP9: bool; 
33
      SP10: bool; 
34
      SP11: bool;
35

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
487
   SP3c = true;
488

    
489
   zz171 = (zz170 = 20);
490

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

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

    
507
   zz204 = cruiseThrottle;
508

    
509
   zz165 = (mode = 6);
510

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

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

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

    
528
   zz173 = (zz175 + 1);
529

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

    
537
   zz181 = (carGear = 3);
538

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

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

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

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

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

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

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

    
584
   zz192 = (zz211 > desiredSpeed);
585

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

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

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

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

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

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

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

    
630
   zz198 = (zz197 or 
631
      zz196);
632

    
633
   zz193 = (desiredSpeed <> 0.0);
634

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

    
638
   zz231 = (cruiseThrottle <= 100.0);
639

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

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

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

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

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

    
676
   VRP1 = (zz232 and 
677
      zz231);
678

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

    
687
   zz235 = (desiredSpeed < 0.0);
688

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

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

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

    
704
   zz194 = (desiredSpeed >= 15.0);
705

    
706
   zz197 = (mode = 1);
707

    
708
   VRP3 = (not zz237);
709

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

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

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

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

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

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

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

    
764
   zz178 = accelResume;
765

    
766
   zz234 = (desiredSpeed >= 0.0);
767

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

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

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

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

    
794
   zz191 = (zz189 and 
795
      zz188);
796

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

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

    
813
   zz208 = (zz211 >= desiredSpeed);
814

    
815
   zz200 = (zz223 = 0.0);
816

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

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

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

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

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

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

    
854
   zz233 = (desiredSpeed <= 100.0);
855

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

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

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

    
867
   zz239 = (desiredSpeed = carSpeed);
868

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

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

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

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

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

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

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

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

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

    
926
   zz203 = (zz201 or 
927
      zz202);
928

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

    
935
   zz183 = decelSet;
936

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

    
942
   zz196 = (mode = 2);
943

    
944
   zz161 = zz160;
945

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

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

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

    
965
   zz0 = zz217;
966

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

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

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

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

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

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

    
1017
   zz188 = (desiredSpeed <> 100.0);
1018

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

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

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

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

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

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

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

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

    
1062
   zz227 = (desiredSpeed - carSpeed);
1063

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

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

    
1073
   zz177 = (zz176 = 20);
1074

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

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

    
1088
   zz195 = (desiredSpeed = 0.0);
1089

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

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

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

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

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

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

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

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

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

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

    
1169
   zz202 = (mode = 3);
1170

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

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

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

    
1186
   zz238 = (desiredSpeed = zz211);
1187

    
1188
   zz212 = (zz211 = desiredSpeed);
1189

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

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

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

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

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

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

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

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

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

    
1248
   zz215 = (zz211 < desiredSpeed);
1249

    
1250
   zz236 = (desiredSpeed > 0.0);
1251

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

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

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

    
1273
   zz3 = zz216;
1274

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

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

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

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

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

    
1309
   zz209 = zz163;
1310

    
1311
   zz216 = zz164;
1312

    
1313
   zz217 = zz165;
1314

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

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

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

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

    
1342
   OK = (zz234 and 
1343
      zz233);
1344

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

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

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

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

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

    
1382
   zz228 = (zz227 * 1.0);
1383

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

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

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

    
1403
   zz167 = (zz169 + 1);
1404

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

    
1412
   zz163 = (mode = 4);
1413

    
1414
   zz187 = (cruiseThrottle = 0.0);
1415

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

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

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

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

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

    
1451
   zz225 = (zz230 + zz224);
1452

    
1453
   zz190 = desiredSpeed;
1454

    
1455
   zz207 = (zz211 <= desiredSpeed);
1456

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1533
   zz232 = (cruiseThrottle >= 0.0);
1534

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

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

    
1544
   zz152 = ((zz153 = 1) or 
1545

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

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

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

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

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

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

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

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

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

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

    
1598
   zz237 = (zz236 and 
1599
      zz235);
1600

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

    
1607
   zz164 = (mode = 5);
1608

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

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

    
1623
   zz230 = (zz229 / 20.0);
1624

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

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

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

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

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

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

    
1650
   zz214 = (zz213 and 
1651
      zz193);
1652

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

    
1660
   zz206 = (zz205 = cruiseThrottle);
1661

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1794
   zz182 = (carSpeed >= 15.0);
1795

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

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

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

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

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

    
1845
--   check zz57; 
1846

    
1847
--   check zz65; 
1848

    
1849
--   check zz73; 
1850

    
1851
--   check zz117; 
1852

    
1853
--   check zz152;
1854

    
1855
tel;
1856

    
1857