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