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