1extern int __VERIFIER_nondet_int(void);
2
3
4
5#line 2 "libacc.c"
6struct JoinPoint {
7 void **(*fp)(struct JoinPoint * ) ;
8 void **args ;
9 int argsCount ;
10 char const **argsType ;
11 void *(*arg)(int , struct JoinPoint * ) ;
12 char const *(*argType)(int , struct JoinPoint * ) ;
13 void **retValue ;
14 char const *retType ;
15 char const *funcName ;
16 char const *targetName ;
17 char const *fileName ;
18 char const *kind ;
19 void *excep_return ;
20};
21#line 18 "libacc.c"
22struct __UTAC__CFLOW_FUNC {
23 int (*func)(int , int ) ;
24 int val ;
25 struct __UTAC__CFLOW_FUNC *next ;
26};
27#line 18 "libacc.c"
28struct __UTAC__EXCEPTION {
29 void *jumpbuf ;
30 unsigned long long prtValue ;
31 int pops ;
32 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
33};
34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
35typedef unsigned long size_t;
36#line 76 "libacc.c"
37struct __ACC__ERR {
38 void *v ;
39 struct __ACC__ERR *next ;
40};
41#line 1 "Elevator.o"
42#pragma merger(0,"Elevator.i","")
43#line 359 "/usr/include/stdio.h"
44extern int printf(char const * __restrict __format , ...) ;
45#line 10 "Person.h"
46int getWeight(int person ) ;
47#line 14
48int getDestination(int person ) ;
49#line 16
50void enterElevator(int p ) ;
51#line 12 "Floor.h"
52int isFloorCalling(int floorID ) ;
53#line 14
54void resetCallOnFloor(int floorID ) ;
55#line 18
56int isPersonOnFloor(int person , int floor ) ;
57#line 22
58void removePersonFromFloor(int person , int floor ) ;
59#line 24
60int isTopFloor(int floorID ) ;
61#line 28
62void initFloors(void) ;
63#line 20 "Elevator.h"
64void timeShift(void) ;
65#line 22
66int isBlocked(void) ;
67#line 24
68void printState(void) ;
69#line 26
70int isEmpty(void) ;
71#line 28
72int isAnyLiftButtonPressed(void) ;
73#line 30
74int buttonForFloorIsPressed(int floorID ) ;
75#line 33
76void initTopDown(void) ;
77#line 35
78void initBottomUp(void) ;
79#line 38
80int areDoorsOpen(void) ;
81#line 40
82int getCurrentFloorID(void) ;
83#line 42
84int isIdle(void) ;
85#line 45 "Elevator.h"
86int weight = 0;
87#line 47 "Elevator.h"
88int maximumWeight = 100;
89#line 55 "Elevator.h"
90int executiveFloor = 4;
91#line 58
92int isExecutiveFloorCalling(void) ;
93#line 60
94int isExecutiveFloor(int floorID ) ;
95#line 63 "Elevator.h"
96int blocked = 0;
97#line 16 "Elevator.c"
98int currentHeading = 1;
99#line 18 "Elevator.c"
100int currentFloorID = 0;
101#line 20 "Elevator.c"
102int persons_0 ;
103#line 22 "Elevator.c"
104int persons_1 ;
105#line 24 "Elevator.c"
106int persons_2 ;
107#line 26 "Elevator.c"
108int persons_3 ;
109#line 28 "Elevator.c"
110int persons_4 ;
111#line 30 "Elevator.c"
112int persons_5 ;
113#line 33 "Elevator.c"
114int doorState = 1;
115#line 35 "Elevator.c"
116int floorButtons_0 ;
117#line 37 "Elevator.c"
118int floorButtons_1 ;
119#line 39 "Elevator.c"
120int floorButtons_2 ;
121#line 41 "Elevator.c"
122int floorButtons_3 ;
123#line 43 "Elevator.c"
124int floorButtons_4 ;
125#line 51 "Elevator.c"
126void initTopDown(void)
127{
128
129 {
130 {
131#line 52
132 currentFloorID = 4;
133#line 53
134 currentHeading = 0;
135#line 54
136 floorButtons_0 = 0;
137#line 55
138 floorButtons_1 = 0;
139#line 56
140 floorButtons_2 = 0;
141#line 57
142 floorButtons_3 = 0;
143#line 58
144 floorButtons_4 = 0;
145#line 59
146 persons_0 = 0;
147#line 60
148 persons_1 = 0;
149#line 61
150 persons_2 = 0;
151#line 62
152 persons_3 = 0;
153#line 63
154 persons_4 = 0;
155#line 64
156 persons_5 = 0;
157#line 65
158 initFloors();
159 }
160#line 1083 "Elevator.c"
161 return;
162}
163}
164#line 68 "Elevator.c"
165void initBottomUp(void)
166{
167
168 {
169 {
170#line 69
171 currentFloorID = 0;
172#line 70
173 currentHeading = 1;
174#line 71
175 floorButtons_0 = 0;
176#line 72
177 floorButtons_1 = 0;
178#line 73
179 floorButtons_2 = 0;
180#line 74
181 floorButtons_3 = 0;
182#line 75
183 floorButtons_4 = 0;
184#line 76
185 persons_0 = 0;
186#line 77
187 persons_1 = 0;
188#line 78
189 persons_2 = 0;
190#line 79
191 persons_3 = 0;
192#line 80
193 persons_4 = 0;
194#line 81
195 persons_5 = 0;
196#line 82
197 initFloors();
198 }
199#line 1129 "Elevator.c"
200 return;
201}
202}
203#line 84 "Elevator.c"
204int isBlocked(void)
205{ int retValue_acc ;
206
207 {
208#line 1147 "Elevator.c"
209 retValue_acc = blocked;
210#line 1149
211 return (retValue_acc);
212#line 1156
213 return (retValue_acc);
214}
215}
216#line 89 "Elevator.c"
217void enterElevator__wrappee__base(int p )
218{
219
220 {
221#line 98
222 if (p == 0) {
223#line 99
224 persons_0 = 1;
225 } else {
226#line 100
227 if (p == 1) {
228#line 101
229 persons_1 = 1;
230 } else {
231#line 102
232 if (p == 2) {
233#line 103
234 persons_2 = 1;
235 } else {
236#line 104
237 if (p == 3) {
238#line 105
239 persons_3 = 1;
240 } else {
241#line 106
242 if (p == 4) {
243#line 107
244 persons_4 = 1;
245 } else {
246#line 108
247 if (p == 5) {
248#line 109
249 persons_5 = 1;
250 } else {
251
252 }
253 }
254 }
255 }
256 }
257 }
258#line 1191 "Elevator.c"
259 return;
260}
261}
262#line 100 "Elevator.c"
263void enterElevator(int p )
264{ int tmp ;
265
266 {
267 {
268#line 101
269 enterElevator__wrappee__base(p);
270#line 102
271 tmp = getWeight(p);
272#line 102
273 weight = weight + tmp;
274 }
275#line 1213 "Elevator.c"
276 return;
277}
278}
279#line 105 "Elevator.c"
280void leaveElevator__wrappee__base(int p )
281{
282
283 {
284#line 113
285 if (p == 0) {
286#line 114
287 persons_0 = 0;
288 } else {
289#line 115
290 if (p == 1) {
291#line 116
292 persons_1 = 0;
293 } else {
294#line 117
295 if (p == 2) {
296#line 118
297 persons_2 = 0;
298 } else {
299#line 119
300 if (p == 3) {
301#line 120
302 persons_3 = 0;
303 } else {
304#line 121
305 if (p == 4) {
306#line 122
307 persons_4 = 0;
308 } else {
309#line 123
310 if (p == 5) {
311#line 124
312 persons_5 = 0;
313 } else {
314
315 }
316 }
317 }
318 }
319 }
320 }
321#line 1244 "Elevator.c"
322 return;
323}
324}
325#line 115 "Elevator.c"
326void leaveElevator__wrappee__weight(int p )
327{ int tmp ;
328
329 {
330 {
331#line 116
332 leaveElevator__wrappee__base(p);
333#line 117
334 tmp = getWeight(p);
335#line 117
336 weight = weight - tmp;
337 }
338#line 1266 "Elevator.c"
339 return;
340}
341}
342#line 121 "Elevator.c"
343void leaveElevator(int p )
344{ int tmp ;
345
346 {
347 {
348#line 122
349 leaveElevator__wrappee__weight(p);
350#line 124
351 tmp = isEmpty();
352 }
353#line 124
354 if (tmp) {
355#line 125
356 floorButtons_0 = 0;
357#line 126
358 floorButtons_1 = 0;
359#line 127
360 floorButtons_2 = 0;
361#line 128
362 floorButtons_3 = 0;
363#line 129
364 floorButtons_4 = 0;
365 } else {
366
367 }
368#line 1299 "Elevator.c"
369 return;
370}
371}
372#line 1301
373void __utac_acc__Specification2_spec__2(int floor ) ;
374#line 133 "Elevator.c"
375void pressInLiftFloorButton(int floorID )
376{ int __utac__ad__arg1 ;
377
378 {
379 {
380#line 1312 "Elevator.c"
381 __utac__ad__arg1 = floorID;
382#line 1313
383 __utac_acc__Specification2_spec__2(__utac__ad__arg1);
384 }
385#line 139
386 if (floorID == 0) {
387#line 140
388 floorButtons_0 = 1;
389 } else {
390#line 141
391 if (floorID == 1) {
392#line 142
393 floorButtons_1 = 1;
394 } else {
395#line 143
396 if (floorID == 2) {
397#line 144
398 floorButtons_2 = 1;
399 } else {
400#line 145
401 if (floorID == 3) {
402#line 146
403 floorButtons_3 = 1;
404 } else {
405#line 147
406 if (floorID == 4) {
407#line 148 "Elevator.c"
408 floorButtons_4 = 1;
409 } else {
410
411 }
412 }
413 }
414 }
415 }
416#line 1337 "Elevator.c"
417 return;
418}
419}
420#line 141 "Elevator.c"
421void resetFloorButton(int floorID )
422{
423
424 {
425#line 147
426 if (floorID == 0) {
427#line 148
428 floorButtons_0 = 0;
429 } else {
430#line 149
431 if (floorID == 1) {
432#line 150
433 floorButtons_1 = 0;
434 } else {
435#line 151
436 if (floorID == 2) {
437#line 152
438 floorButtons_2 = 0;
439 } else {
440#line 153
441 if (floorID == 3) {
442#line 154
443 floorButtons_3 = 0;
444 } else {
445#line 155
446 if (floorID == 4) {
447#line 156
448 floorButtons_4 = 0;
449 } else {
450
451 }
452 }
453 }
454 }
455 }
456#line 1366 "Elevator.c"
457 return;
458}
459}
460#line 149 "Elevator.c"
461int getCurrentFloorID(void)
462{ int retValue_acc ;
463
464 {
465#line 1384 "Elevator.c"
466 retValue_acc = currentFloorID;
467#line 1386
468 return (retValue_acc);
469#line 1393
470 return (retValue_acc);
471}
472}
473#line 153 "Elevator.c"
474int areDoorsOpen(void)
475{ int retValue_acc ;
476
477 {
478#line 1415 "Elevator.c"
479 retValue_acc = doorState;
480#line 1417
481 return (retValue_acc);
482#line 1424
483 return (retValue_acc);
484}
485}
486#line 157 "Elevator.c"
487int buttonForFloorIsPressed(int floorID )
488{ int retValue_acc ;
489
490 {
491#line 163 "Elevator.c"
492 if (floorID == 0) {
493#line 1447
494 retValue_acc = floorButtons_0;
495#line 1449
496 return (retValue_acc);
497 } else {
498#line 1451
499 if (floorID == 1) {
500#line 1454
501 retValue_acc = floorButtons_1;
502#line 1456
503 return (retValue_acc);
504 } else {
505#line 1458
506 if (floorID == 2) {
507#line 1461
508 retValue_acc = floorButtons_2;
509#line 1463
510 return (retValue_acc);
511 } else {
512#line 1465
513 if (floorID == 3) {
514#line 1468
515 retValue_acc = floorButtons_3;
516#line 1470
517 return (retValue_acc);
518 } else {
519#line 1472
520 if (floorID == 4) {
521#line 1475
522 retValue_acc = floorButtons_4;
523#line 1477
524 return (retValue_acc);
525 } else {
526#line 1481 "Elevator.c"
527 retValue_acc = 0;
528#line 1483
529 return (retValue_acc);
530 }
531 }
532 }
533 }
534 }
535#line 1490 "Elevator.c"
536 return (retValue_acc);
537}
538}
539#line 166 "Elevator.c"
540int getCurrentHeading(void)
541{ int retValue_acc ;
542
543 {
544#line 1512 "Elevator.c"
545 retValue_acc = currentHeading;
546#line 1514
547 return (retValue_acc);
548#line 1521
549 return (retValue_acc);
550}
551}
552#line 170 "Elevator.c"
553int isEmpty(void)
554{ int retValue_acc ;
555
556 {
557#line 177 "Elevator.c"
558 if (persons_0 == 1) {
559#line 1544
560 retValue_acc = 0;
561#line 1546
562 return (retValue_acc);
563 } else {
564#line 1548
565 if (persons_1 == 1) {
566#line 1551
567 retValue_acc = 0;
568#line 1553
569 return (retValue_acc);
570 } else {
571#line 1555
572 if (persons_2 == 1) {
573#line 1558
574 retValue_acc = 0;
575#line 1560
576 return (retValue_acc);
577 } else {
578#line 1562
579 if (persons_3 == 1) {
580#line 1565
581 retValue_acc = 0;
582#line 1567
583 return (retValue_acc);
584 } else {
585#line 1569
586 if (persons_4 == 1) {
587#line 1572
588 retValue_acc = 0;
589#line 1574
590 return (retValue_acc);
591 } else {
592#line 1576
593 if (persons_5 == 1) {
594#line 1579 "Elevator.c"
595 retValue_acc = 0;
596#line 1581
597 return (retValue_acc);
598 } else {
599
600 }
601 }
602 }
603 }
604 }
605 }
606#line 1586 "Elevator.c"
607 retValue_acc = 1;
608#line 1588
609 return (retValue_acc);
610#line 1595
611 return (retValue_acc);
612}
613}
614#line 181 "Elevator.c"
615int anyStopRequested(void)
616{ int retValue_acc ;
617 int tmp ;
618 int tmp___0 ;
619 int tmp___1 ;
620 int tmp___2 ;
621 int tmp___3 ;
622
623 {
624 {
625#line 192
626 tmp___3 = isFloorCalling(0);
627 }
628#line 192 "Elevator.c"
629 if (tmp___3) {
630#line 1618
631 retValue_acc = 1;
632#line 1620
633 return (retValue_acc);
634 } else {
635#line 1622
636 if (floorButtons_0) {
637#line 1625
638 retValue_acc = 1;
639#line 1627
640 return (retValue_acc);
641 } else {
642 {
643#line 1629 "Elevator.c"
644 tmp___2 = isFloorCalling(1);
645 }
646#line 1629
647 if (tmp___2) {
648#line 1632
649 retValue_acc = 1;
650#line 1634
651 return (retValue_acc);
652 } else {
653#line 1636
654 if (floorButtons_1) {
655#line 1639
656 retValue_acc = 1;
657#line 1641
658 return (retValue_acc);
659 } else {
660 {
661#line 1643
662 tmp___1 = isFloorCalling(2);
663 }
664#line 1643
665 if (tmp___1) {
666#line 1646
667 retValue_acc = 1;
668#line 1648
669 return (retValue_acc);
670 } else {
671#line 1650
672 if (floorButtons_2) {
673#line 1653
674 retValue_acc = 1;
675#line 1655
676 return (retValue_acc);
677 } else {
678 {
679#line 1657
680 tmp___0 = isFloorCalling(3);
681 }
682#line 1657
683 if (tmp___0) {
684#line 1660
685 retValue_acc = 1;
686#line 1662
687 return (retValue_acc);
688 } else {
689#line 1664
690 if (floorButtons_3) {
691#line 1667
692 retValue_acc = 1;
693#line 1669
694 return (retValue_acc);
695 } else {
696 {
697#line 1671
698 tmp = isFloorCalling(4);
699 }
700#line 1671
701 if (tmp) {
702#line 1674
703 retValue_acc = 1;
704#line 1676
705 return (retValue_acc);
706 } else {
707#line 1678
708 if (floorButtons_4) {
709#line 1681
710 retValue_acc = 1;
711#line 1683
712 return (retValue_acc);
713 } else {
714
715 }
716 }
717 }
718 }
719 }
720 }
721 }
722 }
723 }
724 }
725#line 1688 "Elevator.c"
726 retValue_acc = 0;
727#line 1690
728 return (retValue_acc);
729#line 1697
730 return (retValue_acc);
731}
732}
733#line 195 "Elevator.c"
734int isIdle(void)
735{ int retValue_acc ;
736 int tmp ;
737
738 {
739 {
740#line 1719 "Elevator.c"
741 tmp = anyStopRequested();
742#line 1719
743 retValue_acc = tmp == 0;
744 }
745#line 1721
746 return (retValue_acc);
747#line 1728
748 return (retValue_acc);
749}
750}
751#line 199 "Elevator.c"
752int stopRequestedInDirection__wrappee__empty(int dir , int respectFloorCalls , int respectInLiftCalls )
753{ int retValue_acc ;
754 int tmp ;
755 int tmp___0 ;
756 int tmp___1 ;
757 int tmp___2 ;
758 int tmp___3 ;
759 int tmp___4 ;
760 int tmp___5 ;
761 int tmp___6 ;
762 int tmp___7 ;
763 int tmp___8 ;
764 int tmp___9 ;
765
766 {
767#line 250
768 if (dir == 1) {
769 {
770#line 210
771 tmp = isTopFloor(currentFloorID);
772 }
773#line 210 "Elevator.c"
774 if (tmp) {
775#line 1754 "Elevator.c"
776 retValue_acc = 0;
777#line 1756
778 return (retValue_acc);
779 } else {
780
781 }
782#line 210
783 if (currentFloorID < 0) {
784#line 210
785 if (respectFloorCalls) {
786 {
787#line 210 "Elevator.c"
788 tmp___4 = isFloorCalling(0);
789 }
790#line 210 "Elevator.c"
791 if (tmp___4) {
792#line 1762 "Elevator.c"
793 retValue_acc = 1;
794#line 1764
795 return (retValue_acc);
796 } else {
797 goto _L___16;
798 }
799 } else {
800 goto _L___16;
801 }
802 } else {
803 _L___16:
804#line 1766
805 if (currentFloorID < 0) {
806#line 1766
807 if (respectInLiftCalls) {
808#line 1766
809 if (floorButtons_0) {
810#line 1769
811 retValue_acc = 1;
812#line 1771
813 return (retValue_acc);
814 } else {
815 goto _L___14;
816 }
817 } else {
818 goto _L___14;
819 }
820 } else {
821 _L___14:
822#line 1773
823 if (currentFloorID < 1) {
824#line 1773
825 if (respectFloorCalls) {
826 {
827#line 1773
828 tmp___3 = isFloorCalling(1);
829 }
830#line 1773
831 if (tmp___3) {
832#line 1776
833 retValue_acc = 1;
834#line 1778
835 return (retValue_acc);
836 } else {
837 goto _L___12;
838 }
839 } else {
840 goto _L___12;
841 }
842 } else {
843 _L___12:
844#line 1780
845 if (currentFloorID < 1) {
846#line 1780
847 if (respectInLiftCalls) {
848#line 1780
849 if (floorButtons_1) {
850#line 1783
851 retValue_acc = 1;
852#line 1785
853 return (retValue_acc);
854 } else {
855 goto _L___10;
856 }
857 } else {
858 goto _L___10;
859 }
860 } else {
861 _L___10:
862#line 1787
863 if (currentFloorID < 2) {
864#line 1787
865 if (respectFloorCalls) {
866 {
867#line 1787
868 tmp___2 = isFloorCalling(2);
869 }
870#line 1787
871 if (tmp___2) {
872#line 1790
873 retValue_acc = 1;
874#line 1792
875 return (retValue_acc);
876 } else {
877 goto _L___8;
878 }
879 } else {
880 goto _L___8;
881 }
882 } else {
883 _L___8:
884#line 1794
885 if (currentFloorID < 2) {
886#line 1794
887 if (respectInLiftCalls) {
888#line 1794
889 if (floorButtons_2) {
890#line 1797
891 retValue_acc = 1;
892#line 1799
893 return (retValue_acc);
894 } else {
895 goto _L___6;
896 }
897 } else {
898 goto _L___6;
899 }
900 } else {
901 _L___6:
902#line 1801
903 if (currentFloorID < 3) {
904#line 1801
905 if (respectFloorCalls) {
906 {
907#line 1801
908 tmp___1 = isFloorCalling(3);
909 }
910#line 1801
911 if (tmp___1) {
912#line 1804
913 retValue_acc = 1;
914#line 1806
915 return (retValue_acc);
916 } else {
917 goto _L___4;
918 }
919 } else {
920 goto _L___4;
921 }
922 } else {
923 _L___4:
924#line 1808
925 if (currentFloorID < 3) {
926#line 1808
927 if (respectInLiftCalls) {
928#line 1808
929 if (floorButtons_3) {
930#line 1811
931 retValue_acc = 1;
932#line 1813
933 return (retValue_acc);
934 } else {
935 goto _L___2;
936 }
937 } else {
938 goto _L___2;
939 }
940 } else {
941 _L___2:
942#line 1815
943 if (currentFloorID < 4) {
944#line 1815
945 if (respectFloorCalls) {
946 {
947#line 1815
948 tmp___0 = isFloorCalling(4);
949 }
950#line 1815
951 if (tmp___0) {
952#line 1818
953 retValue_acc = 1;
954#line 1820
955 return (retValue_acc);
956 } else {
957 goto _L___0;
958 }
959 } else {
960 goto _L___0;
961 }
962 } else {
963 _L___0:
964#line 1822
965 if (currentFloorID < 4) {
966#line 1822
967 if (respectInLiftCalls) {
968#line 1822
969 if (floorButtons_4) {
970#line 1825
971 retValue_acc = 1;
972#line 1827
973 return (retValue_acc);
974 } else {
975#line 1831
976 retValue_acc = 0;
977#line 1833
978 return (retValue_acc);
979 }
980 } else {
981#line 1831
982 retValue_acc = 0;
983#line 1833
984 return (retValue_acc);
985 }
986 } else {
987#line 1831 "Elevator.c"
988 retValue_acc = 0;
989#line 1833
990 return (retValue_acc);
991 }
992 }
993 }
994 }
995 }
996 }
997 }
998 }
999 }
1000 }
1001 } else {
1002#line 235 "Elevator.c"
1003 if (currentFloorID == 0) {
1004#line 1841 "Elevator.c"
1005 retValue_acc = 0;
1006#line 1843
1007 return (retValue_acc);
1008 } else {
1009
1010 }
1011#line 235
1012 if (currentFloorID > 0) {
1013#line 235
1014 if (respectFloorCalls) {
1015 {
1016#line 235 "Elevator.c"
1017 tmp___9 = isFloorCalling(0);
1018 }
1019#line 235 "Elevator.c"
1020 if (tmp___9) {
1021#line 1849 "Elevator.c"
1022 retValue_acc = 1;
1023#line 1851
1024 return (retValue_acc);
1025 } else {
1026 goto _L___34;
1027 }
1028 } else {
1029 goto _L___34;
1030 }
1031 } else {
1032 _L___34:
1033#line 1853
1034 if (currentFloorID > 0) {
1035#line 1853
1036 if (respectInLiftCalls) {
1037#line 1853
1038 if (floorButtons_0) {
1039#line 1856
1040 retValue_acc = 1;
1041#line 1858
1042 return (retValue_acc);
1043 } else {
1044 goto _L___32;
1045 }
1046 } else {
1047 goto _L___32;
1048 }
1049 } else {
1050 _L___32:
1051#line 1860
1052 if (currentFloorID > 1) {
1053#line 1860
1054 if (respectFloorCalls) {
1055 {
1056#line 1860
1057 tmp___8 = isFloorCalling(1);
1058 }
1059#line 1860
1060 if (tmp___8) {
1061#line 1863
1062 retValue_acc = 1;
1063#line 1865
1064 return (retValue_acc);
1065 } else {
1066 goto _L___30;
1067 }
1068 } else {
1069 goto _L___30;
1070 }
1071 } else {
1072 _L___30:
1073#line 1867
1074 if (currentFloorID > 1) {
1075#line 1867
1076 if (respectInLiftCalls) {
1077#line 1867
1078 if (floorButtons_1) {
1079#line 1870
1080 retValue_acc = 1;
1081#line 1872
1082 return (retValue_acc);
1083 } else {
1084 goto _L___28;
1085 }
1086 } else {
1087 goto _L___28;
1088 }
1089 } else {
1090 _L___28:
1091#line 1874
1092 if (currentFloorID > 2) {
1093#line 1874
1094 if (respectFloorCalls) {
1095 {
1096#line 1874
1097 tmp___7 = isFloorCalling(2);
1098 }
1099#line 1874
1100 if (tmp___7) {
1101#line 1877
1102 retValue_acc = 1;
1103#line 1879
1104 return (retValue_acc);
1105 } else {
1106 goto _L___26;
1107 }
1108 } else {
1109 goto _L___26;
1110 }
1111 } else {
1112 _L___26:
1113#line 1881
1114 if (currentFloorID > 2) {
1115#line 1881
1116 if (respectInLiftCalls) {
1117#line 1881
1118 if (floorButtons_2) {
1119#line 1884
1120 retValue_acc = 1;
1121#line 1886
1122 return (retValue_acc);
1123 } else {
1124 goto _L___24;
1125 }
1126 } else {
1127 goto _L___24;
1128 }
1129 } else {
1130 _L___24:
1131#line 1888
1132 if (currentFloorID > 3) {
1133#line 1888
1134 if (respectFloorCalls) {
1135 {
1136#line 1888
1137 tmp___6 = isFloorCalling(3);
1138 }
1139#line 1888
1140 if (tmp___6) {
1141#line 1891
1142 retValue_acc = 1;
1143#line 1893
1144 return (retValue_acc);
1145 } else {
1146 goto _L___22;
1147 }
1148 } else {
1149 goto _L___22;
1150 }
1151 } else {
1152 _L___22:
1153#line 1895
1154 if (currentFloorID > 3) {
1155#line 1895
1156 if (respectInLiftCalls) {
1157#line 1895
1158 if (floorButtons_3) {
1159#line 1898
1160 retValue_acc = 1;
1161#line 1900
1162 return (retValue_acc);
1163 } else {
1164 goto _L___20;
1165 }
1166 } else {
1167 goto _L___20;
1168 }
1169 } else {
1170 _L___20:
1171#line 1902
1172 if (currentFloorID > 4) {
1173#line 1902
1174 if (respectFloorCalls) {
1175 {
1176#line 1902
1177 tmp___5 = isFloorCalling(4);
1178 }
1179#line 1902
1180 if (tmp___5) {
1181#line 1905
1182 retValue_acc = 1;
1183#line 1907
1184 return (retValue_acc);
1185 } else {
1186 goto _L___18;
1187 }
1188 } else {
1189 goto _L___18;
1190 }
1191 } else {
1192 _L___18:
1193#line 1909
1194 if (currentFloorID > 4) {
1195#line 1909
1196 if (respectInLiftCalls) {
1197#line 1909
1198 if (floorButtons_4) {
1199#line 1912
1200 retValue_acc = 1;
1201#line 1914
1202 return (retValue_acc);
1203 } else {
1204#line 1918
1205 retValue_acc = 0;
1206#line 1920
1207 return (retValue_acc);
1208 }
1209 } else {
1210#line 1918
1211 retValue_acc = 0;
1212#line 1920
1213 return (retValue_acc);
1214 }
1215 } else {
1216#line 1918 "Elevator.c"
1217 retValue_acc = 0;
1218#line 1920
1219 return (retValue_acc);
1220 }
1221 }
1222 }
1223 }
1224 }
1225 }
1226 }
1227 }
1228 }
1229 }
1230 }
1231#line 1927 "Elevator.c"
1232 return (retValue_acc);
1233}
1234}
1235#line 254 "Elevator.c"
1236int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls )
1237{ int retValue_acc ;
1238 int tmp ;
1239 int tmp___0 ;
1240 int __cil_tmp7 ;
1241 int __cil_tmp8 ;
1242
1243 {
1244 {
1245#line 259
1246 tmp___0 = isExecutiveFloorCalling();
1247 }
1248#line 259 "Elevator.c"
1249 if (tmp___0) {
1250 {
1251#line 1952
1252 tmp = getCurrentFloorID();
1253#line 1952
1254 __cil_tmp7 = dir == 1;
1255#line 1952
1256 __cil_tmp8 = tmp < executiveFloor;
1257#line 1952
1258 retValue_acc = __cil_tmp8 == __cil_tmp7;
1259 }
1260#line 1954
1261 return (retValue_acc);
1262 } else {
1263 {
1264#line 1960 "Elevator.c"
1265 retValue_acc = stopRequestedInDirection__wrappee__empty(dir, respectFloorCalls,
1266 respectInLiftCalls);
1267 }
1268#line 1962
1269 return (retValue_acc);
1270 }
1271#line 1969 "Elevator.c"
1272 return (retValue_acc);
1273}
1274}
1275#line 262 "Elevator.c"
1276int isAnyLiftButtonPressed(void)
1277{ int retValue_acc ;
1278
1279 {
1280#line 268 "Elevator.c"
1281 if (floorButtons_0) {
1282#line 1992
1283 retValue_acc = 1;
1284#line 1994
1285 return (retValue_acc);
1286 } else {
1287#line 1996
1288 if (floorButtons_1) {
1289#line 1999
1290 retValue_acc = 1;
1291#line 2001
1292 return (retValue_acc);
1293 } else {
1294#line 2003
1295 if (floorButtons_2) {
1296#line 2006
1297 retValue_acc = 1;
1298#line 2008
1299 return (retValue_acc);
1300 } else {
1301#line 2010
1302 if (floorButtons_3) {
1303#line 2013
1304 retValue_acc = 1;
1305#line 2015
1306 return (retValue_acc);
1307 } else {
1308#line 2017
1309 if (floorButtons_4) {
1310#line 2020
1311 retValue_acc = 1;
1312#line 2022
1313 return (retValue_acc);
1314 } else {
1315#line 2026 "Elevator.c"
1316 retValue_acc = 0;
1317#line 2028
1318 return (retValue_acc);
1319 }
1320 }
1321 }
1322 }
1323 }
1324#line 2035 "Elevator.c"
1325 return (retValue_acc);
1326}
1327}
1328#line 271 "Elevator.c"
1329void continueInDirection(int dir )
1330{ int tmp ;
1331
1332 {
1333#line 272
1334 currentHeading = dir;
1335#line 273
1336 if (currentHeading == 1) {
1337 {
1338#line 278
1339 tmp = isTopFloor(currentFloorID);
1340 }
1341#line 278
1342 if (tmp) {
1343#line 276
1344 currentHeading = 0;
1345 } else {
1346
1347 }
1348 } else {
1349#line 283
1350 if (currentFloorID == 0) {
1351#line 281
1352 currentHeading = 1;
1353 } else {
1354
1355 }
1356 }
1357#line 284
1358 if (currentHeading == 1) {
1359#line 285
1360 currentFloorID = currentFloorID + 1;
1361 } else {
1362#line 287
1363 currentFloorID = currentFloorID - 1;
1364 }
1365#line 2081 "Elevator.c"
1366 return;
1367}
1368}
1369#line 291 "Elevator.c"
1370int stopRequestedAtCurrentFloor__wrappee__empty(void)
1371{ int retValue_acc ;
1372 int tmp ;
1373 int tmp___0 ;
1374
1375 {
1376 {
1377#line 298
1378 tmp___0 = isFloorCalling(currentFloorID);
1379 }
1380#line 298 "Elevator.c"
1381 if (tmp___0) {
1382#line 2102
1383 retValue_acc = 1;
1384#line 2104
1385 return (retValue_acc);
1386 } else {
1387 {
1388#line 2106 "Elevator.c"
1389 tmp = buttonForFloorIsPressed(currentFloorID);
1390 }
1391#line 2106
1392 if (tmp) {
1393#line 2111
1394 retValue_acc = 1;
1395#line 2113
1396 return (retValue_acc);
1397 } else {
1398#line 2119
1399 retValue_acc = 0;
1400#line 2121
1401 return (retValue_acc);
1402 }
1403 }
1404#line 2128 "Elevator.c"
1405 return (retValue_acc);
1406}
1407}
1408#line 302 "Elevator.c"
1409int stopRequestedAtCurrentFloor(void)
1410{ int retValue_acc ;
1411 int tmp ;
1412 int tmp___0 ;
1413
1414 {
1415 {
1416#line 305
1417 tmp = isExecutiveFloorCalling();
1418 }
1419#line 305
1420 if (tmp) {
1421 {
1422#line 305 "Elevator.c"
1423 tmp___0 = getCurrentFloorID();
1424 }
1425#line 305 "Elevator.c"
1426 if (executiveFloor == tmp___0) {
1427 {
1428#line 2159
1429 retValue_acc = stopRequestedAtCurrentFloor__wrappee__empty();
1430 }
1431#line 2161
1432 return (retValue_acc);
1433 } else {
1434#line 2153 "Elevator.c"
1435 retValue_acc = 0;
1436#line 2155
1437 return (retValue_acc);
1438 }
1439 } else {
1440 {
1441#line 2159 "Elevator.c"
1442 retValue_acc = stopRequestedAtCurrentFloor__wrappee__empty();
1443 }
1444#line 2161
1445 return (retValue_acc);
1446 }
1447#line 2168 "Elevator.c"
1448 return (retValue_acc);
1449}
1450}
1451#line 308 "Elevator.c"
1452int getReverseHeading(int ofHeading )
1453{ int retValue_acc ;
1454
1455 {
1456#line 311 "Elevator.c"
1457 if (ofHeading == 0) {
1458#line 2193
1459 retValue_acc = 1;
1460#line 2195
1461 return (retValue_acc);
1462 } else {
1463#line 2199 "Elevator.c"
1464 retValue_acc = 0;
1465#line 2201
1466 return (retValue_acc);
1467 }
1468#line 2208 "Elevator.c"
1469 return (retValue_acc);
1470}
1471}
1472#line 315 "Elevator.c"
1473void processWaitingOnFloor(int floorID )
1474{ int tmp ;
1475 int tmp___0 ;
1476 int tmp___1 ;
1477 int tmp___2 ;
1478 int tmp___3 ;
1479 int tmp___4 ;
1480 int tmp___5 ;
1481 int tmp___6 ;
1482 int tmp___7 ;
1483 int tmp___8 ;
1484 int tmp___9 ;
1485 int tmp___10 ;
1486
1487 {
1488 {
1489#line 321
1490 tmp___0 = isPersonOnFloor(0, floorID);
1491 }
1492#line 321
1493 if (tmp___0) {
1494 {
1495#line 317
1496 removePersonFromFloor(0, floorID);
1497#line 318
1498 tmp = getDestination(0);
1499#line 318
1500 pressInLiftFloorButton(tmp);
1501#line 319
1502 enterElevator(0);
1503 }
1504 } else {
1505
1506 }
1507 {
1508#line 321
1509 tmp___2 = isPersonOnFloor(1, floorID);
1510 }
1511#line 321
1512 if (tmp___2) {
1513 {
1514#line 322
1515 removePersonFromFloor(1, floorID);
1516#line 323
1517 tmp___1 = getDestination(1);
1518#line 323
1519 pressInLiftFloorButton(tmp___1);
1520#line 324
1521 enterElevator(1);
1522 }
1523 } else {
1524
1525 }
1526 {
1527#line 326
1528 tmp___4 = isPersonOnFloor(2, floorID);
1529 }
1530#line 326
1531 if (tmp___4) {
1532 {
1533#line 327
1534 removePersonFromFloor(2, floorID);
1535#line 328
1536 tmp___3 = getDestination(2);
1537#line 328
1538 pressInLiftFloorButton(tmp___3);
1539#line 329
1540 enterElevator(2);
1541 }
1542 } else {
1543
1544 }
1545 {
1546#line 331
1547 tmp___6 = isPersonOnFloor(3, floorID);
1548 }
1549#line 331
1550 if (tmp___6) {
1551 {
1552#line 332
1553 removePersonFromFloor(3, floorID);
1554#line 333
1555 tmp___5 = getDestination(3);
1556#line 333
1557 pressInLiftFloorButton(tmp___5);
1558#line 334
1559 enterElevator(3);
1560 }
1561 } else {
1562
1563 }
1564 {
1565#line 336
1566 tmp___8 = isPersonOnFloor(4, floorID);
1567 }
1568#line 336
1569 if (tmp___8) {
1570 {
1571#line 337
1572 removePersonFromFloor(4, floorID);
1573#line 338
1574 tmp___7 = getDestination(4);
1575#line 338
1576 pressInLiftFloorButton(tmp___7);
1577#line 339
1578 enterElevator(4);
1579 }
1580 } else {
1581
1582 }
1583 {
1584#line 341
1585 tmp___10 = isPersonOnFloor(5, floorID);
1586 }
1587#line 341
1588 if (tmp___10) {
1589 {
1590#line 342
1591 removePersonFromFloor(5, floorID);
1592#line 343
1593 tmp___9 = getDestination(5);
1594#line 343
1595 pressInLiftFloorButton(tmp___9);
1596#line 344
1597 enterElevator(5);
1598 }
1599 } else {
1600
1601 }
1602 {
1603#line 346
1604 resetCallOnFloor(floorID);
1605 }
1606#line 2286 "Elevator.c"
1607 return;
1608}
1609}
1610#line 350 "Elevator.c"
1611void timeShift__wrappee__executivefloor(void)
1612{ int tmp ;
1613 int tmp___0 ;
1614 int tmp___1 ;
1615 int tmp___2 ;
1616 int tmp___3 ;
1617 int tmp___4 ;
1618 int tmp___5 ;
1619 int tmp___6 ;
1620 int tmp___7 ;
1621 int tmp___8 ;
1622 int tmp___9 ;
1623
1624 {
1625 {
1626#line 383
1627 tmp___9 = stopRequestedAtCurrentFloor();
1628 }
1629#line 383
1630 if (tmp___9) {
1631#line 355
1632 doorState = 1;
1633#line 357
1634 if (persons_0) {
1635 {
1636#line 357
1637 tmp = getDestination(0);
1638 }
1639#line 357
1640 if (tmp == currentFloorID) {
1641 {
1642#line 358
1643 leaveElevator(0);
1644 }
1645 } else {
1646
1647 }
1648 } else {
1649
1650 }
1651#line 358
1652 if (persons_1) {
1653 {
1654#line 358
1655 tmp___0 = getDestination(1);
1656 }
1657#line 358
1658 if (tmp___0 == currentFloorID) {
1659 {
1660#line 359
1661 leaveElevator(1);
1662 }
1663 } else {
1664
1665 }
1666 } else {
1667
1668 }
1669#line 359
1670 if (persons_2) {
1671 {
1672#line 359
1673 tmp___1 = getDestination(2);
1674 }
1675#line 359
1676 if (tmp___1 == currentFloorID) {
1677 {
1678#line 360
1679 leaveElevator(2);
1680 }
1681 } else {
1682
1683 }
1684 } else {
1685
1686 }
1687#line 360
1688 if (persons_3) {
1689 {
1690#line 360
1691 tmp___2 = getDestination(3);
1692 }
1693#line 360
1694 if (tmp___2 == currentFloorID) {
1695 {
1696#line 361
1697 leaveElevator(3);
1698 }
1699 } else {
1700
1701 }
1702 } else {
1703
1704 }
1705#line 361
1706 if (persons_4) {
1707 {
1708#line 361
1709 tmp___3 = getDestination(4);
1710 }
1711#line 361
1712 if (tmp___3 == currentFloorID) {
1713 {
1714#line 362
1715 leaveElevator(4);
1716 }
1717 } else {
1718
1719 }
1720 } else {
1721
1722 }
1723#line 362
1724 if (persons_5) {
1725 {
1726#line 362
1727 tmp___4 = getDestination(5);
1728 }
1729#line 362
1730 if (tmp___4 == currentFloorID) {
1731 {
1732#line 363
1733 leaveElevator(5);
1734 }
1735 } else {
1736
1737 }
1738 } else {
1739
1740 }
1741 {
1742#line 363
1743 processWaitingOnFloor(currentFloorID);
1744#line 364
1745 resetFloorButton(currentFloorID);
1746 }
1747 } else {
1748#line 370
1749 if (doorState == 1) {
1750#line 367
1751 doorState = 0;
1752 } else {
1753
1754 }
1755 {
1756#line 370
1757 tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
1758 }
1759#line 370
1760 if (tmp___8) {
1761 {
1762#line 373
1763 continueInDirection(currentHeading);
1764 }
1765 } else {
1766 {
1767#line 374
1768 tmp___6 = getReverseHeading(currentHeading);
1769#line 374
1770 tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
1771 }
1772#line 374
1773 if (tmp___7) {
1774 {
1775#line 377
1776 tmp___5 = getReverseHeading(currentHeading);
1777#line 377
1778 continueInDirection(tmp___5);
1779 }
1780 } else {
1781 {
1782#line 381
1783 continueInDirection(currentHeading);
1784 }
1785 }
1786 }
1787 }
1788#line 2349 "Elevator.c"
1789 return;
1790}
1791}
1792#line 2351
1793void __utac_acc__Specification2_spec__3(void) ;
1794#line 388 "Elevator.c"
1795void timeShift(void)
1796{ int tmp ;
1797
1798 {
1799 {
1800#line 394
1801 tmp = areDoorsOpen();
1802 }
1803#line 394
1804 if (tmp) {
1805#line 394
1806 if (weight > maximumWeight) {
1807#line 390
1808 blocked = 1;
1809 } else {
1810 {
1811#line 392
1812 blocked = 0;
1813#line 393
1814 timeShift__wrappee__executivefloor();
1815 }
1816 }
1817 } else {
1818 {
1819#line 392
1820 blocked = 0;
1821#line 393
1822 timeShift__wrappee__executivefloor();
1823 }
1824 }
1825 {
1826#line 2379 "Elevator.c"
1827 __utac_acc__Specification2_spec__3();
1828 }
1829#line 2385
1830 return;
1831}
1832}
1833#line 397 "Elevator.c"
1834void printState__wrappee__executivefloor(void)
1835{ int tmp ;
1836 int tmp___0 ;
1837 int tmp___1 ;
1838 int tmp___2 ;
1839 int tmp___3 ;
1840 char const * __restrict __cil_tmp6 ;
1841 char const * __restrict __cil_tmp7 ;
1842 char const * __restrict __cil_tmp8 ;
1843 char const * __restrict __cil_tmp9 ;
1844 char const * __restrict __cil_tmp10 ;
1845 char const * __restrict __cil_tmp11 ;
1846 char const * __restrict __cil_tmp12 ;
1847 char const * __restrict __cil_tmp13 ;
1848 char const * __restrict __cil_tmp14 ;
1849 char const * __restrict __cil_tmp15 ;
1850 char const * __restrict __cil_tmp16 ;
1851 char const * __restrict __cil_tmp17 ;
1852 char const * __restrict __cil_tmp18 ;
1853 char const * __restrict __cil_tmp19 ;
1854 char const * __restrict __cil_tmp20 ;
1855 char const * __restrict __cil_tmp21 ;
1856 char const * __restrict __cil_tmp22 ;
1857 char const * __restrict __cil_tmp23 ;
1858 char const * __restrict __cil_tmp24 ;
1859 char const * __restrict __cil_tmp25 ;
1860 char const * __restrict __cil_tmp26 ;
1861
1862 {
1863 {
1864#line 398
1865 __cil_tmp6 = (char const * __restrict )"Elevator ";
1866#line 398
1867 printf(__cil_tmp6);
1868 }
1869#line 399
1870 if (doorState) {
1871 {
1872#line 400
1873 __cil_tmp7 = (char const * __restrict )"[_]";
1874#line 400
1875 printf(__cil_tmp7);
1876 }
1877 } else {
1878 {
1879#line 401
1880 __cil_tmp8 = (char const * __restrict )"[] ";
1881#line 401
1882 printf(__cil_tmp8);
1883 }
1884 }
1885 {
1886#line 401
1887 __cil_tmp9 = (char const * __restrict )" at ";
1888#line 401
1889 printf(__cil_tmp9);
1890#line 402
1891 __cil_tmp10 = (char const * __restrict )"%i";
1892#line 402
1893 printf(__cil_tmp10, currentFloorID);
1894#line 403
1895 __cil_tmp11 = (char const * __restrict )" heading ";
1896#line 403
1897 printf(__cil_tmp11);
1898 }
1899#line 404
1900 if (currentHeading) {
1901 {
1902#line 405
1903 __cil_tmp12 = (char const * __restrict )"up";
1904#line 405
1905 printf(__cil_tmp12);
1906 }
1907 } else {
1908 {
1909#line 406
1910 __cil_tmp13 = (char const * __restrict )"down";
1911#line 406
1912 printf(__cil_tmp13);
1913 }
1914 }
1915 {
1916#line 406
1917 __cil_tmp14 = (char const * __restrict )" IL_p:";
1918#line 406
1919 printf(__cil_tmp14);
1920 }
1921#line 407
1922 if (floorButtons_0) {
1923 {
1924#line 408
1925 __cil_tmp15 = (char const * __restrict )" %i";
1926#line 408
1927 printf(__cil_tmp15, 0);
1928 }
1929 } else {
1930
1931 }
1932#line 408
1933 if (floorButtons_1) {
1934 {
1935#line 409
1936 __cil_tmp16 = (char const * __restrict )" %i";
1937#line 409
1938 printf(__cil_tmp16, 1);
1939 }
1940 } else {
1941
1942 }
1943#line 409
1944 if (floorButtons_2) {
1945 {
1946#line 410
1947 __cil_tmp17 = (char const * __restrict )" %i";
1948#line 410
1949 printf(__cil_tmp17, 2);
1950 }
1951 } else {
1952
1953 }
1954#line 410
1955 if (floorButtons_3) {
1956 {
1957#line 411
1958 __cil_tmp18 = (char const * __restrict )" %i";
1959#line 411
1960 printf(__cil_tmp18, 3);
1961 }
1962 } else {
1963
1964 }
1965#line 411
1966 if (floorButtons_4) {
1967 {
1968#line 412
1969 __cil_tmp19 = (char const * __restrict )" %i";
1970#line 412
1971 printf(__cil_tmp19, 4);
1972 }
1973 } else {
1974
1975 }
1976 {
1977#line 412
1978 __cil_tmp20 = (char const * __restrict )" F_p:";
1979#line 412
1980 printf(__cil_tmp20);
1981#line 413
1982 tmp = isFloorCalling(0);
1983 }
1984#line 413
1985 if (tmp) {
1986 {
1987#line 414
1988 __cil_tmp21 = (char const * __restrict )" %i";
1989#line 414
1990 printf(__cil_tmp21, 0);
1991 }
1992 } else {
1993
1994 }
1995 {
1996#line 414
1997 tmp___0 = isFloorCalling(1);
1998 }
1999#line 414
2000 if (tmp___0) {
2001 {
2002#line 415
2003 __cil_tmp22 = (char const * __restrict )" %i";
2004#line 415
2005 printf(__cil_tmp22, 1);
2006 }
2007 } else {
2008
2009 }
2010 {
2011#line 415
2012 tmp___1 = isFloorCalling(2);
2013 }
2014#line 415
2015 if (tmp___1) {
2016 {
2017#line 416
2018 __cil_tmp23 = (char const * __restrict )" %i";
2019#line 416
2020 printf(__cil_tmp23, 2);
2021 }
2022 } else {
2023
2024 }
2025 {
2026#line 416
2027 tmp___2 = isFloorCalling(3);
2028 }
2029#line 416
2030 if (tmp___2) {
2031 {
2032#line 417
2033 __cil_tmp24 = (char const * __restrict )" %i";
2034#line 417
2035 printf(__cil_tmp24, 3);
2036 }
2037 } else {
2038
2039 }
2040 {
2041#line 417
2042 tmp___3 = isFloorCalling(4);
2043 }
2044#line 417
2045 if (tmp___3) {
2046 {
2047#line 418
2048 __cil_tmp25 = (char const * __restrict )" %i";
2049#line 418
2050 printf(__cil_tmp25, 4);
2051 }
2052 } else {
2053
2054 }
2055 {
2056#line 418
2057 __cil_tmp26 = (char const * __restrict )"\n";
2058#line 418
2059 printf(__cil_tmp26);
2060 }
2061#line 2455 "Elevator.c"
2062 return;
2063}
2064}
2065#line 421 "Elevator.c"
2066void printState(void)
2067{ int tmp ;
2068 char const * __restrict __cil_tmp2 ;
2069
2070 {
2071 {
2072#line 423
2073 tmp = isBlocked();
2074 }
2075#line 423
2076 if (tmp) {
2077 {
2078#line 424
2079 __cil_tmp2 = (char const * __restrict )"Blocked ";
2080#line 424
2081 printf(__cil_tmp2);
2082 }
2083 } else {
2084
2085 }
2086 {
2087#line 423
2088 printState__wrappee__executivefloor();
2089 }
2090#line 2478 "Elevator.c"
2091 return;
2092}
2093}
2094#line 427 "Elevator.c"
2095int existInLiftCallsInDirection(int d )
2096{ int retValue_acc ;
2097 int i ;
2098 int i___0 ;
2099
2100 {
2101#line 448
2102 if (d == 1) {
2103#line 429 "Elevator.c"
2104 i = 0;
2105#line 430
2106 i = currentFloorID + 1;
2107 {
2108#line 430
2109 while (1) {
2110 while_0_continue: ;
2111#line 430
2112 if (i < 5) {
2113
2114 } else {
2115 goto while_0_break;
2116 }
2117#line 436
2118 if (i == 0) {
2119#line 436 "Elevator.c"
2120 if (floorButtons_0) {
2121#line 2506
2122 retValue_acc = 1;
2123#line 2508
2124 return (retValue_acc);
2125 } else {
2126 goto _L___2;
2127 }
2128 } else {
2129 _L___2:
2130#line 2510
2131 if (i == 1) {
2132#line 2510
2133 if (floorButtons_1) {
2134#line 2513
2135 retValue_acc = 1;
2136#line 2515
2137 return (retValue_acc);
2138 } else {
2139 goto _L___1;
2140 }
2141 } else {
2142 _L___1:
2143#line 2517
2144 if (i == 2) {
2145#line 2517
2146 if (floorButtons_2) {
2147#line 2520
2148 retValue_acc = 1;
2149#line 2522
2150 return (retValue_acc);
2151 } else {
2152 goto _L___0;
2153 }
2154 } else {
2155 _L___0:
2156#line 2524
2157 if (i == 3) {
2158#line 2524
2159 if (floorButtons_3) {
2160#line 2527
2161 retValue_acc = 1;
2162#line 2529
2163 return (retValue_acc);
2164 } else {
2165 goto _L;
2166 }
2167 } else {
2168 _L:
2169#line 2531
2170 if (i == 4) {
2171#line 2531
2172 if (floorButtons_4) {
2173#line 2534 "Elevator.c"
2174 retValue_acc = 1;
2175#line 2536
2176 return (retValue_acc);
2177 } else {
2178
2179 }
2180 } else {
2181
2182 }
2183 }
2184 }
2185 }
2186 }
2187#line 430
2188 i = i + 1;
2189 }
2190 while_0_break: ;
2191 }
2192 } else {
2193#line 2538 "Elevator.c"
2194 if (d == 0) {
2195#line 438
2196 i___0 = 0;
2197#line 439
2198 i___0 = currentFloorID - 1;
2199 {
2200#line 439
2201 while (1) {
2202 while_1_continue: ;
2203#line 439
2204 if (i___0 >= 0) {
2205
2206 } else {
2207 goto while_1_break;
2208 }
2209#line 439
2210 i___0 = currentFloorID + 1;
2211 {
2212#line 439
2213 while (1) {
2214 while_2_continue: ;
2215#line 439
2216 if (i___0 < 5) {
2217
2218 } else {
2219 goto while_2_break;
2220 }
2221#line 446
2222 if (i___0 == 0) {
2223#line 446 "Elevator.c"
2224 if (floorButtons_0) {
2225#line 2550
2226 retValue_acc = 1;
2227#line 2552
2228 return (retValue_acc);
2229 } else {
2230 goto _L___6;
2231 }
2232 } else {
2233 _L___6:
2234#line 2554
2235 if (i___0 == 1) {
2236#line 2554
2237 if (floorButtons_1) {
2238#line 2557
2239 retValue_acc = 1;
2240#line 2559
2241 return (retValue_acc);
2242 } else {
2243 goto _L___5;
2244 }
2245 } else {
2246 _L___5:
2247#line 2561
2248 if (i___0 == 2) {
2249#line 2561
2250 if (floorButtons_2) {
2251#line 2564
2252 retValue_acc = 1;
2253#line 2566
2254 return (retValue_acc);
2255 } else {
2256 goto _L___4;
2257 }
2258 } else {
2259 _L___4:
2260#line 2568
2261 if (i___0 == 3) {
2262#line 2568
2263 if (floorButtons_3) {
2264#line 2571
2265 retValue_acc = 1;
2266#line 2573
2267 return (retValue_acc);
2268 } else {
2269 goto _L___3;
2270 }
2271 } else {
2272 _L___3:
2273#line 2575
2274 if (i___0 == 4) {
2275#line 2575
2276 if (floorButtons_4) {
2277#line 2578 "Elevator.c"
2278 retValue_acc = 1;
2279#line 2580
2280 return (retValue_acc);
2281 } else {
2282
2283 }
2284 } else {
2285
2286 }
2287 }
2288 }
2289 }
2290 }
2291#line 439
2292 i___0 = i___0 + 1;
2293 }
2294 while_2_break: ;
2295 }
2296#line 439
2297 i___0 = i___0 - 1;
2298 }
2299 while_1_break: ;
2300 }
2301 } else {
2302
2303 }
2304 }
2305#line 2585 "Elevator.c"
2306 retValue_acc = 0;
2307#line 2587
2308 return (retValue_acc);
2309#line 2594
2310 return (retValue_acc);
2311}
2312}
2313#line 450 "Elevator.c"
2314int isExecutiveFloorCalling(void)
2315{ int retValue_acc ;
2316
2317 {
2318 {
2319#line 2616 "Elevator.c"
2320 retValue_acc = isFloorCalling(executiveFloor);
2321 }
2322#line 2618
2323 return (retValue_acc);
2324#line 2625
2325 return (retValue_acc);
2326}
2327}
2328#line 454 "Elevator.c"
2329int isExecutiveFloor(int floorID )
2330{ int retValue_acc ;
2331
2332 {
2333#line 2647 "Elevator.c"
2334 retValue_acc = executiveFloor == floorID;
2335#line 2649
2336 return (retValue_acc);
2337#line 2656
2338 return (retValue_acc);
2339}
2340}
2341#line 1 "featureselect.o"
2342#pragma merger(0,"featureselect.i","")
2343#line 9 "featureselect.h"
2344int select_one(void) ;
2345#line 11
2346void select_features(void) ;
2347#line 13
2348void select_helpers(void) ;
2349#line 15
2350int valid_product(void) ;
2351#line 8 "featureselect.c"
2352int select_one(void)
2353{ int retValue_acc ;
2354 int choice = __VERIFIER_nondet_int();
2355
2356 {
2357#line 63 "featureselect.c"
2358 retValue_acc = choice;
2359#line 65
2360 return (retValue_acc);
2361#line 72
2362 return (retValue_acc);
2363}
2364}
2365#line 14 "featureselect.c"
2366void select_features(void)
2367{
2368
2369 {
2370#line 94 "featureselect.c"
2371 return;
2372}
2373}
2374#line 20 "featureselect.c"
2375void select_helpers(void)
2376{
2377
2378 {
2379#line 112 "featureselect.c"
2380 return;
2381}
2382}
2383#line 25 "featureselect.c"
2384int valid_product(void)
2385{ int retValue_acc ;
2386
2387 {
2388#line 130 "featureselect.c"
2389 retValue_acc = 1;
2390#line 132
2391 return (retValue_acc);
2392#line 139
2393 return (retValue_acc);
2394}
2395}
2396#line 1 "wsllib_check.o"
2397#pragma merger(0,"wsllib_check.i","")
2398#line 3 "wsllib_check.c"
2399void __automaton_fail(void)
2400{
2401
2402 {
2403 goto ERROR;
2404 ERROR: ;
2405#line 53 "wsllib_check.c"
2406 return;
2407}
2408}
2409#line 1 "Floor.o"
2410#pragma merger(0,"Floor.i","")
2411#line 16 "Floor.h"
2412void callOnFloor(int floorID ) ;
2413#line 20
2414void initPersonOnFloor(int person , int floor ) ;
2415#line 9 "Floor.c"
2416int calls_0 ;
2417#line 11 "Floor.c"
2418int calls_1 ;
2419#line 13 "Floor.c"
2420int calls_2 ;
2421#line 15 "Floor.c"
2422int calls_3 ;
2423#line 17 "Floor.c"
2424int calls_4 ;
2425#line 20 "Floor.c"
2426int personOnFloor_0_0 ;
2427#line 22 "Floor.c"
2428int personOnFloor_0_1 ;
2429#line 24 "Floor.c"
2430int personOnFloor_0_2 ;
2431#line 26 "Floor.c"
2432int personOnFloor_0_3 ;
2433#line 28 "Floor.c"
2434int personOnFloor_0_4 ;
2435#line 30 "Floor.c"
2436int personOnFloor_1_0 ;
2437#line 32 "Floor.c"
2438int personOnFloor_1_1 ;
2439#line 34 "Floor.c"
2440int personOnFloor_1_2 ;
2441#line 36 "Floor.c"
2442int personOnFloor_1_3 ;
2443#line 38 "Floor.c"
2444int personOnFloor_1_4 ;
2445#line 40 "Floor.c"
2446int personOnFloor_2_0 ;
2447#line 42 "Floor.c"
2448int personOnFloor_2_1 ;
2449#line 44 "Floor.c"
2450int personOnFloor_2_2 ;
2451#line 46 "Floor.c"
2452int personOnFloor_2_3 ;
2453#line 48 "Floor.c"
2454int personOnFloor_2_4 ;
2455#line 50 "Floor.c"
2456int personOnFloor_3_0 ;
2457#line 52 "Floor.c"
2458int personOnFloor_3_1 ;
2459#line 54 "Floor.c"
2460int personOnFloor_3_2 ;
2461#line 56 "Floor.c"
2462int personOnFloor_3_3 ;
2463#line 58 "Floor.c"
2464int personOnFloor_3_4 ;
2465#line 60 "Floor.c"
2466int personOnFloor_4_0 ;
2467#line 62 "Floor.c"
2468int personOnFloor_4_1 ;
2469#line 64 "Floor.c"
2470int personOnFloor_4_2 ;
2471#line 66 "Floor.c"
2472int personOnFloor_4_3 ;
2473#line 68 "Floor.c"
2474int personOnFloor_4_4 ;
2475#line 70 "Floor.c"
2476int personOnFloor_5_0 ;
2477#line 72 "Floor.c"
2478int personOnFloor_5_1 ;
2479#line 74 "Floor.c"
2480int personOnFloor_5_2 ;
2481#line 76 "Floor.c"
2482int personOnFloor_5_3 ;
2483#line 78 "Floor.c"
2484int personOnFloor_5_4 ;
2485#line 81 "Floor.c"
2486void initFloors(void)
2487{
2488
2489 {
2490#line 82
2491 calls_0 = 0;
2492#line 83
2493 calls_1 = 0;
2494#line 84
2495 calls_2 = 0;
2496#line 85
2497 calls_3 = 0;
2498#line 86
2499 calls_4 = 0;
2500#line 87
2501 personOnFloor_0_0 = 0;
2502#line 88
2503 personOnFloor_0_1 = 0;
2504#line 89
2505 personOnFloor_0_2 = 0;
2506#line 90
2507 personOnFloor_0_3 = 0;
2508#line 91
2509 personOnFloor_0_4 = 0;
2510#line 92
2511 personOnFloor_1_0 = 0;
2512#line 93
2513 personOnFloor_1_1 = 0;
2514#line 94
2515 personOnFloor_1_2 = 0;
2516#line 95
2517 personOnFloor_1_3 = 0;
2518#line 96
2519 personOnFloor_1_4 = 0;
2520#line 97
2521 personOnFloor_2_0 = 0;
2522#line 98
2523 personOnFloor_2_1 = 0;
2524#line 99
2525 personOnFloor_2_2 = 0;
2526#line 100
2527 personOnFloor_2_3 = 0;
2528#line 101
2529 personOnFloor_2_4 = 0;
2530#line 102
2531 personOnFloor_3_0 = 0;
2532#line 103
2533 personOnFloor_3_1 = 0;
2534#line 104
2535 personOnFloor_3_2 = 0;
2536#line 105
2537 personOnFloor_3_3 = 0;
2538#line 106
2539 personOnFloor_3_4 = 0;
2540#line 107
2541 personOnFloor_4_0 = 0;
2542#line 108
2543 personOnFloor_4_1 = 0;
2544#line 109
2545 personOnFloor_4_2 = 0;
2546#line 110
2547 personOnFloor_4_3 = 0;
2548#line 111
2549 personOnFloor_4_4 = 0;
2550#line 112
2551 personOnFloor_5_0 = 0;
2552#line 113
2553 personOnFloor_5_1 = 0;
2554#line 114
2555 personOnFloor_5_2 = 0;
2556#line 115
2557 personOnFloor_5_3 = 0;
2558#line 116
2559 personOnFloor_5_4 = 0;
2560#line 1120 "Floor.c"
2561 return;
2562}
2563}
2564#line 120 "Floor.c"
2565int isFloorCalling(int floorID )
2566{ int retValue_acc ;
2567
2568 {
2569#line 126 "Floor.c"
2570 if (floorID == 0) {
2571#line 1139
2572 retValue_acc = calls_0;
2573#line 1141
2574 return (retValue_acc);
2575 } else {
2576#line 1143
2577 if (floorID == 1) {
2578#line 1146
2579 retValue_acc = calls_1;
2580#line 1148
2581 return (retValue_acc);
2582 } else {
2583#line 1150
2584 if (floorID == 2) {
2585#line 1153
2586 retValue_acc = calls_2;
2587#line 1155
2588 return (retValue_acc);
2589 } else {
2590#line 1157
2591 if (floorID == 3) {
2592#line 1160
2593 retValue_acc = calls_3;
2594#line 1162
2595 return (retValue_acc);
2596 } else {
2597#line 1164
2598 if (floorID == 4) {
2599#line 1167 "Floor.c"
2600 retValue_acc = calls_4;
2601#line 1169
2602 return (retValue_acc);
2603 } else {
2604
2605 }
2606 }
2607 }
2608 }
2609 }
2610#line 1174 "Floor.c"
2611 retValue_acc = 0;
2612#line 1176
2613 return (retValue_acc);
2614#line 1183
2615 return (retValue_acc);
2616}
2617}
2618#line 130 "Floor.c"
2619void resetCallOnFloor(int floorID )
2620{
2621
2622 {
2623#line 136
2624 if (floorID == 0) {
2625#line 137
2626 calls_0 = 0;
2627 } else {
2628#line 138
2629 if (floorID == 1) {
2630#line 139
2631 calls_1 = 0;
2632 } else {
2633#line 140
2634 if (floorID == 2) {
2635#line 141
2636 calls_2 = 0;
2637 } else {
2638#line 142
2639 if (floorID == 3) {
2640#line 143
2641 calls_3 = 0;
2642 } else {
2643#line 144
2644 if (floorID == 4) {
2645#line 145
2646 calls_4 = 0;
2647 } else {
2648
2649 }
2650 }
2651 }
2652 }
2653 }
2654#line 1216 "Floor.c"
2655 return;
2656}
2657}
2658#line 139 "Floor.c"
2659void callOnFloor(int floorID )
2660{
2661
2662 {
2663#line 145
2664 if (floorID == 0) {
2665#line 146
2666 calls_0 = 1;
2667 } else {
2668#line 147
2669 if (floorID == 1) {
2670#line 148
2671 calls_1 = 1;
2672 } else {
2673#line 149
2674 if (floorID == 2) {
2675#line 150
2676 calls_2 = 1;
2677 } else {
2678#line 151
2679 if (floorID == 3) {
2680#line 152
2681 calls_3 = 1;
2682 } else {
2683#line 153
2684 if (floorID == 4) {
2685#line 154
2686 calls_4 = 1;
2687 } else {
2688
2689 }
2690 }
2691 }
2692 }
2693 }
2694#line 1245 "Floor.c"
2695 return;
2696}
2697}
2698#line 148 "Floor.c"
2699int isPersonOnFloor(int person , int floor )
2700{ int retValue_acc ;
2701
2702 {
2703#line 185
2704 if (floor == 0) {
2705#line 156 "Floor.c"
2706 if (person == 0) {
2707#line 1267
2708 retValue_acc = personOnFloor_0_0;
2709#line 1269
2710 return (retValue_acc);
2711 } else {
2712#line 1271
2713 if (person == 1) {
2714#line 1274
2715 retValue_acc = personOnFloor_1_0;
2716#line 1276
2717 return (retValue_acc);
2718 } else {
2719#line 1278
2720 if (person == 2) {
2721#line 1281
2722 retValue_acc = personOnFloor_2_0;
2723#line 1283
2724 return (retValue_acc);
2725 } else {
2726#line 1285
2727 if (person == 3) {
2728#line 1288
2729 retValue_acc = personOnFloor_3_0;
2730#line 1290
2731 return (retValue_acc);
2732 } else {
2733#line 1292
2734 if (person == 4) {
2735#line 1295
2736 retValue_acc = personOnFloor_4_0;
2737#line 1297
2738 return (retValue_acc);
2739 } else {
2740#line 1299
2741 if (person == 5) {
2742#line 1302
2743 retValue_acc = personOnFloor_5_0;
2744#line 1304
2745 return (retValue_acc);
2746 } else {
2747
2748 }
2749 }
2750 }
2751 }
2752 }
2753 }
2754 } else {
2755#line 1306 "Floor.c"
2756 if (floor == 1) {
2757#line 163 "Floor.c"
2758 if (person == 0) {
2759#line 1312
2760 retValue_acc = personOnFloor_0_1;
2761#line 1314
2762 return (retValue_acc);
2763 } else {
2764#line 1316
2765 if (person == 1) {
2766#line 1319
2767 retValue_acc = personOnFloor_1_1;
2768#line 1321
2769 return (retValue_acc);
2770 } else {
2771#line 1323
2772 if (person == 2) {
2773#line 1326
2774 retValue_acc = personOnFloor_2_1;
2775#line 1328
2776 return (retValue_acc);
2777 } else {
2778#line 1330
2779 if (person == 3) {
2780#line 1333
2781 retValue_acc = personOnFloor_3_1;
2782#line 1335
2783 return (retValue_acc);
2784 } else {
2785#line 1337
2786 if (person == 4) {
2787#line 1340
2788 retValue_acc = personOnFloor_4_1;
2789#line 1342
2790 return (retValue_acc);
2791 } else {
2792#line 1344
2793 if (person == 5) {
2794#line 1347
2795 retValue_acc = personOnFloor_5_1;
2796#line 1349
2797 return (retValue_acc);
2798 } else {
2799
2800 }
2801 }
2802 }
2803 }
2804 }
2805 }
2806 } else {
2807#line 1351 "Floor.c"
2808 if (floor == 2) {
2809#line 170 "Floor.c"
2810 if (person == 0) {
2811#line 1357
2812 retValue_acc = personOnFloor_0_2;
2813#line 1359
2814 return (retValue_acc);
2815 } else {
2816#line 1361
2817 if (person == 1) {
2818#line 1364
2819 retValue_acc = personOnFloor_1_2;
2820#line 1366
2821 return (retValue_acc);
2822 } else {
2823#line 1368
2824 if (person == 2) {
2825#line 1371
2826 retValue_acc = personOnFloor_2_2;
2827#line 1373
2828 return (retValue_acc);
2829 } else {
2830#line 1375
2831 if (person == 3) {
2832#line 1378
2833 retValue_acc = personOnFloor_3_2;
2834#line 1380
2835 return (retValue_acc);
2836 } else {
2837#line 1382
2838 if (person == 4) {
2839#line 1385
2840 retValue_acc = personOnFloor_4_2;
2841#line 1387
2842 return (retValue_acc);
2843 } else {
2844#line 1389
2845 if (person == 5) {
2846#line 1392
2847 retValue_acc = personOnFloor_5_2;
2848#line 1394
2849 return (retValue_acc);
2850 } else {
2851
2852 }
2853 }
2854 }
2855 }
2856 }
2857 }
2858 } else {
2859#line 1396 "Floor.c"
2860 if (floor == 3) {
2861#line 177 "Floor.c"
2862 if (person == 0) {
2863#line 1402
2864 retValue_acc = personOnFloor_0_3;
2865#line 1404
2866 return (retValue_acc);
2867 } else {
2868#line 1406
2869 if (person == 1) {
2870#line 1409
2871 retValue_acc = personOnFloor_1_3;
2872#line 1411
2873 return (retValue_acc);
2874 } else {
2875#line 1413
2876 if (person == 2) {
2877#line 1416
2878 retValue_acc = personOnFloor_2_3;
2879#line 1418
2880 return (retValue_acc);
2881 } else {
2882#line 1420
2883 if (person == 3) {
2884#line 1423
2885 retValue_acc = personOnFloor_3_3;
2886#line 1425
2887 return (retValue_acc);
2888 } else {
2889#line 1427
2890 if (person == 4) {
2891#line 1430
2892 retValue_acc = personOnFloor_4_3;
2893#line 1432
2894 return (retValue_acc);
2895 } else {
2896#line 1434
2897 if (person == 5) {
2898#line 1437
2899 retValue_acc = personOnFloor_5_3;
2900#line 1439
2901 return (retValue_acc);
2902 } else {
2903
2904 }
2905 }
2906 }
2907 }
2908 }
2909 }
2910 } else {
2911#line 1441 "Floor.c"
2912 if (floor == 4) {
2913#line 184 "Floor.c"
2914 if (person == 0) {
2915#line 1447
2916 retValue_acc = personOnFloor_0_4;
2917#line 1449
2918 return (retValue_acc);
2919 } else {
2920#line 1451
2921 if (person == 1) {
2922#line 1454
2923 retValue_acc = personOnFloor_1_4;
2924#line 1456
2925 return (retValue_acc);
2926 } else {
2927#line 1458
2928 if (person == 2) {
2929#line 1461
2930 retValue_acc = personOnFloor_2_4;
2931#line 1463
2932 return (retValue_acc);
2933 } else {
2934#line 1465
2935 if (person == 3) {
2936#line 1468
2937 retValue_acc = personOnFloor_3_4;
2938#line 1470
2939 return (retValue_acc);
2940 } else {
2941#line 1472
2942 if (person == 4) {
2943#line 1475
2944 retValue_acc = personOnFloor_4_4;
2945#line 1477
2946 return (retValue_acc);
2947 } else {
2948#line 1479
2949 if (person == 5) {
2950#line 1482 "Floor.c"
2951 retValue_acc = personOnFloor_5_4;
2952#line 1484
2953 return (retValue_acc);
2954 } else {
2955
2956 }
2957 }
2958 }
2959 }
2960 }
2961 }
2962 } else {
2963
2964 }
2965 }
2966 }
2967 }
2968 }
2969#line 1489 "Floor.c"
2970 retValue_acc = 0;
2971#line 1491
2972 return (retValue_acc);
2973#line 1498
2974 return (retValue_acc);
2975}
2976}
2977#line 188 "Floor.c"
2978void initPersonOnFloor(int person , int floor )
2979{
2980
2981 {
2982#line 225
2983 if (floor == 0) {
2984#line 196
2985 if (person == 0) {
2986#line 197
2987 personOnFloor_0_0 = 1;
2988 } else {
2989#line 198
2990 if (person == 1) {
2991#line 199
2992 personOnFloor_1_0 = 1;
2993 } else {
2994#line 200
2995 if (person == 2) {
2996#line 201
2997 personOnFloor_2_0 = 1;
2998 } else {
2999#line 202
3000 if (person == 3) {
3001#line 203
3002 personOnFloor_3_0 = 1;
3003 } else {
3004#line 204
3005 if (person == 4) {
3006#line 205
3007 personOnFloor_4_0 = 1;
3008 } else {
3009#line 206
3010 if (person == 5) {
3011#line 207
3012 personOnFloor_5_0 = 1;
3013 } else {
3014
3015 }
3016 }
3017 }
3018 }
3019 }
3020 }
3021 } else {
3022#line 208
3023 if (floor == 1) {
3024#line 203
3025 if (person == 0) {
3026#line 204
3027 personOnFloor_0_1 = 1;
3028 } else {
3029#line 205
3030 if (person == 1) {
3031#line 206
3032 personOnFloor_1_1 = 1;
3033 } else {
3034#line 207
3035 if (person == 2) {
3036#line 208
3037 personOnFloor_2_1 = 1;
3038 } else {
3039#line 209
3040 if (person == 3) {
3041#line 210
3042 personOnFloor_3_1 = 1;
3043 } else {
3044#line 211
3045 if (person == 4) {
3046#line 212
3047 personOnFloor_4_1 = 1;
3048 } else {
3049#line 213
3050 if (person == 5) {
3051#line 214
3052 personOnFloor_5_1 = 1;
3053 } else {
3054
3055 }
3056 }
3057 }
3058 }
3059 }
3060 }
3061 } else {
3062#line 215
3063 if (floor == 2) {
3064#line 210
3065 if (person == 0) {
3066#line 211
3067 personOnFloor_0_2 = 1;
3068 } else {
3069#line 212
3070 if (person == 1) {
3071#line 213
3072 personOnFloor_1_2 = 1;
3073 } else {
3074#line 214
3075 if (person == 2) {
3076#line 215
3077 personOnFloor_2_2 = 1;
3078 } else {
3079#line 216
3080 if (person == 3) {
3081#line 217
3082 personOnFloor_3_2 = 1;
3083 } else {
3084#line 218
3085 if (person == 4) {
3086#line 219
3087 personOnFloor_4_2 = 1;
3088 } else {
3089#line 220
3090 if (person == 5) {
3091#line 221
3092 personOnFloor_5_2 = 1;
3093 } else {
3094
3095 }
3096 }
3097 }
3098 }
3099 }
3100 }
3101 } else {
3102#line 222
3103 if (floor == 3) {
3104#line 217
3105 if (person == 0) {
3106#line 218
3107 personOnFloor_0_3 = 1;
3108 } else {
3109#line 219
3110 if (person == 1) {
3111#line 220
3112 personOnFloor_1_3 = 1;
3113 } else {
3114#line 221
3115 if (person == 2) {
3116#line 222
3117 personOnFloor_2_3 = 1;
3118 } else {
3119#line 223
3120 if (person == 3) {
3121#line 224
3122 personOnFloor_3_3 = 1;
3123 } else {
3124#line 225
3125 if (person == 4) {
3126#line 226
3127 personOnFloor_4_3 = 1;
3128 } else {
3129#line 227
3130 if (person == 5) {
3131#line 228
3132 personOnFloor_5_3 = 1;
3133 } else {
3134
3135 }
3136 }
3137 }
3138 }
3139 }
3140 }
3141 } else {
3142#line 229
3143 if (floor == 4) {
3144#line 224
3145 if (person == 0) {
3146#line 225
3147 personOnFloor_0_4 = 1;
3148 } else {
3149#line 226
3150 if (person == 1) {
3151#line 227
3152 personOnFloor_1_4 = 1;
3153 } else {
3154#line 228
3155 if (person == 2) {
3156#line 229
3157 personOnFloor_2_4 = 1;
3158 } else {
3159#line 230
3160 if (person == 3) {
3161#line 231
3162 personOnFloor_3_4 = 1;
3163 } else {
3164#line 232
3165 if (person == 4) {
3166#line 233
3167 personOnFloor_4_4 = 1;
3168 } else {
3169#line 234
3170 if (person == 5) {
3171#line 235
3172 personOnFloor_5_4 = 1;
3173 } else {
3174
3175 }
3176 }
3177 }
3178 }
3179 }
3180 }
3181 } else {
3182
3183 }
3184 }
3185 }
3186 }
3187 }
3188 {
3189#line 225
3190 callOnFloor(floor);
3191 }
3192#line 1598 "Floor.c"
3193 return;
3194}
3195}
3196#line 228 "Floor.c"
3197void removePersonFromFloor(int person , int floor )
3198{
3199
3200 {
3201#line 265
3202 if (floor == 0) {
3203#line 236
3204 if (person == 0) {
3205#line 237
3206 personOnFloor_0_0 = 0;
3207 } else {
3208#line 238
3209 if (person == 1) {
3210#line 239
3211 personOnFloor_1_0 = 0;
3212 } else {
3213#line 240
3214 if (person == 2) {
3215#line 241
3216 personOnFloor_2_0 = 0;
3217 } else {
3218#line 242
3219 if (person == 3) {
3220#line 243
3221 personOnFloor_3_0 = 0;
3222 } else {
3223#line 244
3224 if (person == 4) {
3225#line 245
3226 personOnFloor_4_0 = 0;
3227 } else {
3228#line 246
3229 if (person == 5) {
3230#line 247
3231 personOnFloor_5_0 = 0;
3232 } else {
3233
3234 }
3235 }
3236 }
3237 }
3238 }
3239 }
3240 } else {
3241#line 248
3242 if (floor == 1) {
3243#line 243
3244 if (person == 0) {
3245#line 244
3246 personOnFloor_0_1 = 0;
3247 } else {
3248#line 245
3249 if (person == 1) {
3250#line 246
3251 personOnFloor_1_1 = 0;
3252 } else {
3253#line 247
3254 if (person == 2) {
3255#line 248
3256 personOnFloor_2_1 = 0;
3257 } else {
3258#line 249
3259 if (person == 3) {
3260#line 250
3261 personOnFloor_3_1 = 0;
3262 } else {
3263#line 251
3264 if (person == 4) {
3265#line 252
3266 personOnFloor_4_1 = 0;
3267 } else {
3268#line 253
3269 if (person == 5) {
3270#line 254
3271 personOnFloor_5_1 = 0;
3272 } else {
3273
3274 }
3275 }
3276 }
3277 }
3278 }
3279 }
3280 } else {
3281#line 255
3282 if (floor == 2) {
3283#line 250
3284 if (person == 0) {
3285#line 251
3286 personOnFloor_0_2 = 0;
3287 } else {
3288#line 252
3289 if (person == 1) {
3290#line 253
3291 personOnFloor_1_2 = 0;
3292 } else {
3293#line 254
3294 if (person == 2) {
3295#line 255
3296 personOnFloor_2_2 = 0;
3297 } else {
3298#line 256
3299 if (person == 3) {
3300#line 257
3301 personOnFloor_3_2 = 0;
3302 } else {
3303#line 258
3304 if (person == 4) {
3305#line 259
3306 personOnFloor_4_2 = 0;
3307 } else {
3308#line 260
3309 if (person == 5) {
3310#line 261
3311 personOnFloor_5_2 = 0;
3312 } else {
3313
3314 }
3315 }
3316 }
3317 }
3318 }
3319 }
3320 } else {
3321#line 262
3322 if (floor == 3) {
3323#line 257
3324 if (person == 0) {
3325#line 258
3326 personOnFloor_0_3 = 0;
3327 } else {
3328#line 259
3329 if (person == 1) {
3330#line 260
3331 personOnFloor_1_3 = 0;
3332 } else {
3333#line 261
3334 if (person == 2) {
3335#line 262
3336 personOnFloor_2_3 = 0;
3337 } else {
3338#line 263
3339 if (person == 3) {
3340#line 264
3341 personOnFloor_3_3 = 0;
3342 } else {
3343#line 265
3344 if (person == 4) {
3345#line 266
3346 personOnFloor_4_3 = 0;
3347 } else {
3348#line 267
3349 if (person == 5) {
3350#line 268
3351 personOnFloor_5_3 = 0;
3352 } else {
3353
3354 }
3355 }
3356 }
3357 }
3358 }
3359 }
3360 } else {
3361#line 269
3362 if (floor == 4) {
3363#line 264
3364 if (person == 0) {
3365#line 265
3366 personOnFloor_0_4 = 0;
3367 } else {
3368#line 266
3369 if (person == 1) {
3370#line 267
3371 personOnFloor_1_4 = 0;
3372 } else {
3373#line 268
3374 if (person == 2) {
3375#line 269
3376 personOnFloor_2_4 = 0;
3377 } else {
3378#line 270
3379 if (person == 3) {
3380#line 271
3381 personOnFloor_3_4 = 0;
3382 } else {
3383#line 272
3384 if (person == 4) {
3385#line 273
3386 personOnFloor_4_4 = 0;
3387 } else {
3388#line 274
3389 if (person == 5) {
3390#line 275
3391 personOnFloor_5_4 = 0;
3392 } else {
3393
3394 }
3395 }
3396 }
3397 }
3398 }
3399 }
3400 } else {
3401
3402 }
3403 }
3404 }
3405 }
3406 }
3407 {
3408#line 265
3409 resetCallOnFloor(floor);
3410 }
3411#line 1694 "Floor.c"
3412 return;
3413}
3414}
3415#line 268 "Floor.c"
3416int isTopFloor(int floorID )
3417{ int retValue_acc ;
3418
3419 {
3420#line 1712 "Floor.c"
3421 retValue_acc = floorID == 4;
3422#line 1714
3423 return (retValue_acc);
3424#line 1721
3425 return (retValue_acc);
3426}
3427}
3428#line 1 "scenario.o"
3429#pragma merger(0,"scenario.i","")
3430#line 2 "scenario.c"
3431void bigMacCall(void) ;
3432#line 3
3433void cleanup(void) ;
3434#line 1 "scenario.c"
3435void test(void)
3436{
3437
3438 {
3439 {
3440#line 2
3441 bigMacCall();
3442#line 3
3443 cleanup();
3444 }
3445#line 53 "scenario.c"
3446 return;
3447}
3448}
3449#line 1 "Person.o"
3450#pragma merger(0,"Person.i","")
3451#line 12 "Person.h"
3452int getOrigin(int person ) ;
3453#line 20 "Person.c"
3454int getWeight(int person )
3455{ int retValue_acc ;
3456
3457 {
3458#line 35 "Person.c"
3459 if (person == 0) {
3460#line 974
3461 retValue_acc = 40;
3462#line 976
3463 return (retValue_acc);
3464 } else {
3465#line 978
3466 if (person == 1) {
3467#line 983
3468 retValue_acc = 40;
3469#line 985
3470 return (retValue_acc);
3471 } else {
3472#line 987
3473 if (person == 2) {
3474#line 992
3475 retValue_acc = 40;
3476#line 994
3477 return (retValue_acc);
3478 } else {
3479#line 996
3480 if (person == 3) {
3481#line 1001
3482 retValue_acc = 40;
3483#line 1003
3484 return (retValue_acc);
3485 } else {
3486#line 1005
3487 if (person == 4) {
3488#line 1010
3489 retValue_acc = 30;
3490#line 1012
3491 return (retValue_acc);
3492 } else {
3493#line 1014
3494 if (person == 5) {
3495#line 1019
3496 retValue_acc = 150;
3497#line 1021
3498 return (retValue_acc);
3499 } else {
3500#line 1027 "Person.c"
3501 retValue_acc = 0;
3502#line 1029
3503 return (retValue_acc);
3504 }
3505 }
3506 }
3507 }
3508 }
3509 }
3510#line 1036 "Person.c"
3511 return (retValue_acc);
3512}
3513}
3514#line 39 "Person.c"
3515int getOrigin(int person )
3516{ int retValue_acc ;
3517
3518 {
3519#line 54 "Person.c"
3520 if (person == 0) {
3521#line 1061
3522 retValue_acc = 4;
3523#line 1063
3524 return (retValue_acc);
3525 } else {
3526#line 1065
3527 if (person == 1) {
3528#line 1070
3529 retValue_acc = 3;
3530#line 1072
3531 return (retValue_acc);
3532 } else {
3533#line 1074
3534 if (person == 2) {
3535#line 1079
3536 retValue_acc = 2;
3537#line 1081
3538 return (retValue_acc);
3539 } else {
3540#line 1083
3541 if (person == 3) {
3542#line 1088
3543 retValue_acc = 1;
3544#line 1090
3545 return (retValue_acc);
3546 } else {
3547#line 1092
3548 if (person == 4) {
3549#line 1097
3550 retValue_acc = 0;
3551#line 1099
3552 return (retValue_acc);
3553 } else {
3554#line 1101
3555 if (person == 5) {
3556#line 1106
3557 retValue_acc = 1;
3558#line 1108
3559 return (retValue_acc);
3560 } else {
3561#line 1114 "Person.c"
3562 retValue_acc = 0;
3563#line 1116
3564 return (retValue_acc);
3565 }
3566 }
3567 }
3568 }
3569 }
3570 }
3571#line 1123 "Person.c"
3572 return (retValue_acc);
3573}
3574}
3575#line 57 "Person.c"
3576int getDestination(int person )
3577{ int retValue_acc ;
3578
3579 {
3580#line 72 "Person.c"
3581 if (person == 0) {
3582#line 1148
3583 retValue_acc = 0;
3584#line 1150
3585 return (retValue_acc);
3586 } else {
3587#line 1152
3588 if (person == 1) {
3589#line 1157
3590 retValue_acc = 0;
3591#line 1159
3592 return (retValue_acc);
3593 } else {
3594#line 1161
3595 if (person == 2) {
3596#line 1166
3597 retValue_acc = 1;
3598#line 1168
3599 return (retValue_acc);
3600 } else {
3601#line 1170
3602 if (person == 3) {
3603#line 1175
3604 retValue_acc = 3;
3605#line 1177
3606 return (retValue_acc);
3607 } else {
3608#line 1179
3609 if (person == 4) {
3610#line 1184
3611 retValue_acc = 1;
3612#line 1186
3613 return (retValue_acc);
3614 } else {
3615#line 1188
3616 if (person == 5) {
3617#line 1193
3618 retValue_acc = 3;
3619#line 1195
3620 return (retValue_acc);
3621 } else {
3622#line 1201 "Person.c"
3623 retValue_acc = 0;
3624#line 1203
3625 return (retValue_acc);
3626 }
3627 }
3628 }
3629 }
3630 }
3631 }
3632#line 1210 "Person.c"
3633 return (retValue_acc);
3634}
3635}
3636#line 1 "Test.o"
3637#pragma merger(0,"Test.i","")
3638#line 544 "/usr/include/stdlib.h"
3639extern __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
3640#line 13 "Test.c"
3641int cleanupTimeShifts = 12;
3642#line 17 "Test.c"
3643#line 23 "Test.c"
3644int get_nondetMinMax07(void)
3645{ int retValue_acc ;
3646 int nd ;
3647 nd = __VERIFIER_nondet_int();
3648
3649 {
3650#line 26 "Test.c"
3651 if (nd == 0) {
3652#line 1108
3653 retValue_acc = 0;
3654#line 1110
3655 return (retValue_acc);
3656 } else {
3657#line 1112
3658 if (nd == 1) {
3659#line 1117
3660 retValue_acc = 1;
3661#line 1119
3662 return (retValue_acc);
3663 } else {
3664#line 1121
3665 if (nd == 2) {
3666#line 1126
3667 retValue_acc = 2;
3668#line 1128
3669 return (retValue_acc);
3670 } else {
3671#line 1130
3672 if (nd == 3) {
3673#line 1135
3674 retValue_acc = 3;
3675#line 1137
3676 return (retValue_acc);
3677 } else {
3678#line 1139
3679 if (nd == 4) {
3680#line 1144
3681 retValue_acc = 4;
3682#line 1146
3683 return (retValue_acc);
3684 } else {
3685#line 1148
3686 if (nd == 5) {
3687#line 1153
3688 retValue_acc = 5;
3689#line 1155
3690 return (retValue_acc);
3691 } else {
3692#line 1157
3693 if (nd == 6) {
3694#line 1162
3695 retValue_acc = 6;
3696#line 1164
3697 return (retValue_acc);
3698 } else {
3699#line 1166
3700 if (nd == 7) {
3701#line 1171 "Test.c"
3702 retValue_acc = 7;
3703#line 1173
3704 return (retValue_acc);
3705 } else {
3706 {
3707#line 43
3708 exit(0);
3709 }
3710 }
3711 }
3712 }
3713 }
3714 }
3715 }
3716 }
3717 }
3718#line 1183 "Test.c"
3719 return (retValue_acc);
3720}
3721}
3722#line 48 "Test.c"
3723void bobCall(void)
3724{ int tmp ;
3725
3726 {
3727 {
3728#line 48
3729 tmp = getOrigin(0);
3730#line 48
3731 initPersonOnFloor(0, tmp);
3732 }
3733#line 1207 "Test.c"
3734 return;
3735}
3736}
3737#line 50 "Test.c"
3738void aliceCall(void)
3739{ int tmp ;
3740
3741 {
3742 {
3743#line 50
3744 tmp = getOrigin(1);
3745#line 50
3746 initPersonOnFloor(1, tmp);
3747 }
3748#line 1227 "Test.c"
3749 return;
3750}
3751}
3752#line 52 "Test.c"
3753void angelinaCall(void)
3754{ int tmp ;
3755
3756 {
3757 {
3758#line 52
3759 tmp = getOrigin(2);
3760#line 52
3761 initPersonOnFloor(2, tmp);
3762 }
3763#line 1247 "Test.c"
3764 return;
3765}
3766}
3767#line 54 "Test.c"
3768void chuckCall(void)
3769{ int tmp ;
3770
3771 {
3772 {
3773#line 54
3774 tmp = getOrigin(3);
3775#line 54
3776 initPersonOnFloor(3, tmp);
3777 }
3778#line 1267 "Test.c"
3779 return;
3780}
3781}
3782#line 56 "Test.c"
3783void monicaCall(void)
3784{ int tmp ;
3785
3786 {
3787 {
3788#line 56
3789 tmp = getOrigin(4);
3790#line 56
3791 initPersonOnFloor(4, tmp);
3792 }
3793#line 1287 "Test.c"
3794 return;
3795}
3796}
3797#line 58 "Test.c"
3798void bigMacCall(void)
3799{ int tmp ;
3800
3801 {
3802 {
3803#line 58
3804 tmp = getOrigin(5);
3805#line 58
3806 initPersonOnFloor(5, tmp);
3807 }
3808#line 1307 "Test.c"
3809 return;
3810}
3811}
3812#line 60 "Test.c"
3813void threeTS(void)
3814{
3815
3816 {
3817 {
3818#line 60
3819 timeShift();
3820#line 60
3821 timeShift();
3822#line 60
3823 timeShift();
3824 }
3825#line 1331 "Test.c"
3826 return;
3827}
3828}
3829#line 62 "Test.c"
3830void cleanup(void)
3831{ int i ;
3832 int tmp ;
3833 int tmp___0 ;
3834 int __cil_tmp4 ;
3835
3836 {
3837 {
3838#line 65
3839 timeShift();
3840#line 67
3841 i = 0;
3842 }
3843 {
3844#line 67
3845 while (1) {
3846 while_3_continue: ;
3847 {
3848#line 67
3849 __cil_tmp4 = cleanupTimeShifts - 1;
3850#line 67
3851 if (i < __cil_tmp4) {
3852 {
3853#line 67
3854 tmp___0 = isBlocked();
3855 }
3856#line 67
3857 if (tmp___0 != 1) {
3858
3859 } else {
3860 goto while_3_break;
3861 }
3862 } else {
3863 goto while_3_break;
3864 }
3865 }
3866 {
3867#line 71
3868 tmp = isIdle();
3869 }
3870#line 71
3871 if (tmp) {
3872#line 72
3873 return;
3874 } else {
3875 {
3876#line 74
3877 timeShift();
3878 }
3879 }
3880#line 67
3881 i = i + 1;
3882 }
3883 while_3_break: ;
3884 }
3885#line 1362 "Test.c"
3886 return;
3887}
3888}
3889#line 77 "Test.c"
3890void randomSequenceOfActions(void)
3891{ int maxLength ;
3892 int tmp ;
3893 int counter ;
3894 int action ;
3895 int tmp___0 ;
3896 int origin ;
3897 int tmp___1 ;
3898 int tmp___2 ;
3899
3900 {
3901 {
3902#line 78
3903 maxLength = 4;
3904#line 79
3905 tmp = __VERIFIER_nondet_int();
3906 }
3907#line 79
3908 if (tmp) {
3909 {
3910#line 81
3911 initTopDown();
3912 }
3913 } else {
3914 {
3915#line 85
3916 initBottomUp();
3917 }
3918 }
3919#line 90
3920 counter = 0;
3921 {
3922#line 91
3923 while (1) {
3924 while_4_continue: ;
3925#line 91
3926 if (counter < maxLength) {
3927
3928 } else {
3929 goto while_4_break;
3930 }
3931 {
3932#line 92
3933 counter = counter + 1;
3934#line 93
3935 tmp___0 = get_nondetMinMax07();
3936#line 93
3937 action = tmp___0;
3938 }
3939#line 99
3940 if (action < 6) {
3941 {
3942#line 100
3943 tmp___1 = getOrigin(action);
3944#line 100
3945 origin = tmp___1;
3946#line 101
3947 initPersonOnFloor(action, origin);
3948 }
3949 } else {
3950#line 102
3951 if (action == 6) {
3952 {
3953#line 103
3954 timeShift();
3955 }
3956 } else {
3957#line 104
3958 if (action == 7) {
3959 {
3960#line 106
3961 timeShift();
3962#line 107
3963 timeShift();
3964#line 108
3965 timeShift();
3966 }
3967 } else {
3968
3969 }
3970 }
3971 }
3972 {
3973#line 113
3974 tmp___2 = isBlocked();
3975 }
3976#line 113
3977 if (tmp___2) {
3978#line 114
3979 return;
3980 } else {
3981
3982 }
3983 }
3984 while_4_break: ;
3985 }
3986 {
3987#line 117
3988 cleanup();
3989 }
3990#line 1433 "Test.c"
3991 return;
3992}
3993}
3994#line 122 "Test.c"
3995void runTest_Simple(void)
3996{
3997
3998 {
3999 {
4000#line 123
4001 bigMacCall();
4002#line 124
4003 angelinaCall();
4004#line 125
4005 cleanup();
4006 }
4007#line 1457 "Test.c"
4008 return;
4009}
4010}
4011#line 130 "Test.c"
4012void Specification1(void)
4013{
4014
4015 {
4016 {
4017#line 131
4018 bigMacCall();
4019#line 132
4020 angelinaCall();
4021#line 133
4022 cleanup();
4023 }
4024#line 1481 "Test.c"
4025 return;
4026}
4027}
4028#line 137 "Test.c"
4029void Specification2(void)
4030{
4031
4032 {
4033 {
4034#line 138
4035 bigMacCall();
4036#line 139
4037 cleanup();
4038 }
4039#line 1503 "Test.c"
4040 return;
4041}
4042}
4043#line 142 "Test.c"
4044void Specification3(void)
4045{
4046
4047 {
4048 {
4049#line 143
4050 bobCall();
4051#line 144
4052 timeShift();
4053#line 145
4054 timeShift();
4055#line 146
4056 timeShift();
4057#line 147
4058 timeShift();
4059#line 149
4060 timeShift();
4061#line 154
4062 bobCall();
4063#line 155
4064 cleanup();
4065 }
4066#line 1537 "Test.c"
4067 return;
4068}
4069}
4070#line 160 "Test.c"
4071void setup(void)
4072{
4073
4074 {
4075#line 1555 "Test.c"
4076 return;
4077}
4078}
4079#line 1557
4080void __utac_acc__Specification2_spec__1(void) ;
4081#line 1560
4082void __utac_acc__Specification2_spec__4(void) ;
4083#line 165 "Test.c"
4084void runTest(void)
4085{
4086
4087 {
4088 {
4089#line 1571 "Test.c"
4090 __utac_acc__Specification2_spec__1();
4091#line 168 "Test.c"
4092 test();
4093#line 1585 "Test.c"
4094 __utac_acc__Specification2_spec__4();
4095 }
4096#line 1591
4097 return;
4098}
4099}
4100#line 173 "Test.c"
4101int main(void)
4102{ int retValue_acc ;
4103 int tmp ;
4104
4105 {
4106 {
4107#line 174
4108 select_helpers();
4109#line 175
4110 select_features();
4111#line 176
4112 tmp = valid_product();
4113 }
4114#line 176
4115 if (tmp) {
4116 {
4117#line 177
4118 setup();
4119#line 178
4120 runTest();
4121 }
4122 } else {
4123
4124 }
4125#line 1620 "Test.c"
4126 retValue_acc = 0;
4127#line 1622
4128 return (retValue_acc);
4129#line 1629
4130 return (retValue_acc);
4131}
4132}
4133#line 1 "libacc.o"
4134#pragma merger(0,"libacc.i","")
4135#line 73 "/usr/include/assert.h"
4136extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
4137 char const *__file ,
4138 unsigned int __line ,
4139 char const *__function ) ;
4140#line 471 "/usr/include/stdlib.h"
4141extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
4142#line 488
4143extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
4144#line 32 "libacc.c"
4145void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
4146 int ) ,
4147 int val )
4148{ struct __UTAC__EXCEPTION *excep ;
4149 struct __UTAC__CFLOW_FUNC *cf ;
4150 void *tmp ;
4151 unsigned long __cil_tmp7 ;
4152 unsigned long __cil_tmp8 ;
4153 unsigned long __cil_tmp9 ;
4154 unsigned long __cil_tmp10 ;
4155 unsigned long __cil_tmp11 ;
4156 unsigned long __cil_tmp12 ;
4157 unsigned long __cil_tmp13 ;
4158 unsigned long __cil_tmp14 ;
4159 int (**mem_15)(int , int ) ;
4160 int *mem_16 ;
4161 struct __UTAC__CFLOW_FUNC **mem_17 ;
4162 struct __UTAC__CFLOW_FUNC **mem_18 ;
4163 struct __UTAC__CFLOW_FUNC **mem_19 ;
4164
4165 {
4166 {
4167#line 33
4168 excep = (struct __UTAC__EXCEPTION *)exception;
4169#line 34
4170 tmp = malloc(24UL);
4171#line 34
4172 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
4173#line 36
4174 mem_15 = (int (**)(int , int ))cf;
4175#line 36
4176 *mem_15 = cflow_func;
4177#line 37
4178 __cil_tmp7 = (unsigned long )cf;
4179#line 37
4180 __cil_tmp8 = __cil_tmp7 + 8;
4181#line 37
4182 mem_16 = (int *)__cil_tmp8;
4183#line 37
4184 *mem_16 = val;
4185#line 38
4186 __cil_tmp9 = (unsigned long )cf;
4187#line 38
4188 __cil_tmp10 = __cil_tmp9 + 16;
4189#line 38
4190 __cil_tmp11 = (unsigned long )excep;
4191#line 38
4192 __cil_tmp12 = __cil_tmp11 + 24;
4193#line 38
4194 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
4195#line 38
4196 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
4197#line 38
4198 *mem_17 = *mem_18;
4199#line 39
4200 __cil_tmp13 = (unsigned long )excep;
4201#line 39
4202 __cil_tmp14 = __cil_tmp13 + 24;
4203#line 39
4204 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4205#line 39
4206 *mem_19 = cf;
4207 }
4208#line 654 "libacc.c"
4209 return;
4210}
4211}
4212#line 44 "libacc.c"
4213void __utac__exception__cf_handler_free(void *exception )
4214{ struct __UTAC__EXCEPTION *excep ;
4215 struct __UTAC__CFLOW_FUNC *cf ;
4216 struct __UTAC__CFLOW_FUNC *tmp ;
4217 unsigned long __cil_tmp5 ;
4218 unsigned long __cil_tmp6 ;
4219 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4220 unsigned long __cil_tmp8 ;
4221 unsigned long __cil_tmp9 ;
4222 unsigned long __cil_tmp10 ;
4223 unsigned long __cil_tmp11 ;
4224 void *__cil_tmp12 ;
4225 unsigned long __cil_tmp13 ;
4226 unsigned long __cil_tmp14 ;
4227 struct __UTAC__CFLOW_FUNC **mem_15 ;
4228 struct __UTAC__CFLOW_FUNC **mem_16 ;
4229 struct __UTAC__CFLOW_FUNC **mem_17 ;
4230
4231 {
4232#line 45
4233 excep = (struct __UTAC__EXCEPTION *)exception;
4234#line 46
4235 __cil_tmp5 = (unsigned long )excep;
4236#line 46
4237 __cil_tmp6 = __cil_tmp5 + 24;
4238#line 46
4239 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4240#line 46
4241 cf = *mem_15;
4242 {
4243#line 49
4244 while (1) {
4245 while_5_continue: ;
4246 {
4247#line 49
4248 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4249#line 49
4250 __cil_tmp8 = (unsigned long )__cil_tmp7;
4251#line 49
4252 __cil_tmp9 = (unsigned long )cf;
4253#line 49
4254 if (__cil_tmp9 != __cil_tmp8) {
4255
4256 } else {
4257 goto while_5_break;
4258 }
4259 }
4260 {
4261#line 50
4262 tmp = cf;
4263#line 51
4264 __cil_tmp10 = (unsigned long )cf;
4265#line 51
4266 __cil_tmp11 = __cil_tmp10 + 16;
4267#line 51
4268 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
4269#line 51
4270 cf = *mem_16;
4271#line 52
4272 __cil_tmp12 = (void *)tmp;
4273#line 52
4274 free(__cil_tmp12);
4275 }
4276 }
4277 while_5_break: ;
4278 }
4279#line 55
4280 __cil_tmp13 = (unsigned long )excep;
4281#line 55
4282 __cil_tmp14 = __cil_tmp13 + 24;
4283#line 55
4284 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4285#line 55
4286 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
4287#line 694 "libacc.c"
4288 return;
4289}
4290}
4291#line 59 "libacc.c"
4292void __utac__exception__cf_handler_reset(void *exception )
4293{ struct __UTAC__EXCEPTION *excep ;
4294 struct __UTAC__CFLOW_FUNC *cf ;
4295 unsigned long __cil_tmp5 ;
4296 unsigned long __cil_tmp6 ;
4297 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4298 unsigned long __cil_tmp8 ;
4299 unsigned long __cil_tmp9 ;
4300 int (*__cil_tmp10)(int , int ) ;
4301 unsigned long __cil_tmp11 ;
4302 unsigned long __cil_tmp12 ;
4303 int __cil_tmp13 ;
4304 unsigned long __cil_tmp14 ;
4305 unsigned long __cil_tmp15 ;
4306 struct __UTAC__CFLOW_FUNC **mem_16 ;
4307 int (**mem_17)(int , int ) ;
4308 int *mem_18 ;
4309 struct __UTAC__CFLOW_FUNC **mem_19 ;
4310
4311 {
4312#line 60
4313 excep = (struct __UTAC__EXCEPTION *)exception;
4314#line 61
4315 __cil_tmp5 = (unsigned long )excep;
4316#line 61
4317 __cil_tmp6 = __cil_tmp5 + 24;
4318#line 61
4319 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4320#line 61
4321 cf = *mem_16;
4322 {
4323#line 64
4324 while (1) {
4325 while_6_continue: ;
4326 {
4327#line 64
4328 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4329#line 64
4330 __cil_tmp8 = (unsigned long )__cil_tmp7;
4331#line 64
4332 __cil_tmp9 = (unsigned long )cf;
4333#line 64
4334 if (__cil_tmp9 != __cil_tmp8) {
4335
4336 } else {
4337 goto while_6_break;
4338 }
4339 }
4340 {
4341#line 65
4342 mem_17 = (int (**)(int , int ))cf;
4343#line 65
4344 __cil_tmp10 = *mem_17;
4345#line 65
4346 __cil_tmp11 = (unsigned long )cf;
4347#line 65
4348 __cil_tmp12 = __cil_tmp11 + 8;
4349#line 65
4350 mem_18 = (int *)__cil_tmp12;
4351#line 65
4352 __cil_tmp13 = *mem_18;
4353#line 65
4354 (*__cil_tmp10)(4, __cil_tmp13);
4355#line 66
4356 __cil_tmp14 = (unsigned long )cf;
4357#line 66
4358 __cil_tmp15 = __cil_tmp14 + 16;
4359#line 66
4360 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
4361#line 66
4362 cf = *mem_19;
4363 }
4364 }
4365 while_6_break: ;
4366 }
4367 {
4368#line 69
4369 __utac__exception__cf_handler_free(exception);
4370 }
4371#line 732 "libacc.c"
4372 return;
4373}
4374}
4375#line 80 "libacc.c"
4376void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
4377#line 80 "libacc.c"
4378static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
4379#line 79 "libacc.c"
4380void *__utac__error_stack_mgt(void *env , int mode , int count )
4381{ void *retValue_acc ;
4382 struct __ACC__ERR *new ;
4383 void *tmp ;
4384 struct __ACC__ERR *temp ;
4385 struct __ACC__ERR *next ;
4386 void *excep ;
4387 unsigned long __cil_tmp10 ;
4388 unsigned long __cil_tmp11 ;
4389 unsigned long __cil_tmp12 ;
4390 unsigned long __cil_tmp13 ;
4391 void *__cil_tmp14 ;
4392 unsigned long __cil_tmp15 ;
4393 unsigned long __cil_tmp16 ;
4394 void *__cil_tmp17 ;
4395 void **mem_18 ;
4396 struct __ACC__ERR **mem_19 ;
4397 struct __ACC__ERR **mem_20 ;
4398 void **mem_21 ;
4399 struct __ACC__ERR **mem_22 ;
4400 void **mem_23 ;
4401 void **mem_24 ;
4402
4403 {
4404#line 82 "libacc.c"
4405 if (count == 0) {
4406#line 758 "libacc.c"
4407 return (retValue_acc);
4408 } else {
4409
4410 }
4411#line 86 "libacc.c"
4412 if (mode == 0) {
4413 {
4414#line 87
4415 tmp = malloc(16UL);
4416#line 87
4417 new = (struct __ACC__ERR *)tmp;
4418#line 88
4419 mem_18 = (void **)new;
4420#line 88
4421 *mem_18 = env;
4422#line 89
4423 __cil_tmp10 = (unsigned long )new;
4424#line 89
4425 __cil_tmp11 = __cil_tmp10 + 8;
4426#line 89
4427 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
4428#line 89
4429 *mem_19 = head;
4430#line 90
4431 head = new;
4432#line 776 "libacc.c"
4433 retValue_acc = (void *)new;
4434 }
4435#line 778
4436 return (retValue_acc);
4437 } else {
4438
4439 }
4440#line 94 "libacc.c"
4441 if (mode == 1) {
4442#line 95
4443 temp = head;
4444 {
4445#line 98
4446 while (1) {
4447 while_7_continue: ;
4448#line 98
4449 if (count > 1) {
4450
4451 } else {
4452 goto while_7_break;
4453 }
4454 {
4455#line 99
4456 __cil_tmp12 = (unsigned long )temp;
4457#line 99
4458 __cil_tmp13 = __cil_tmp12 + 8;
4459#line 99
4460 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
4461#line 99
4462 next = *mem_20;
4463#line 100
4464 mem_21 = (void **)temp;
4465#line 100
4466 excep = *mem_21;
4467#line 101
4468 __cil_tmp14 = (void *)temp;
4469#line 101
4470 free(__cil_tmp14);
4471#line 102
4472 __utac__exception__cf_handler_reset(excep);
4473#line 103
4474 temp = next;
4475#line 104
4476 count = count - 1;
4477 }
4478 }
4479 while_7_break: ;
4480 }
4481 {
4482#line 107
4483 __cil_tmp15 = (unsigned long )temp;
4484#line 107
4485 __cil_tmp16 = __cil_tmp15 + 8;
4486#line 107
4487 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
4488#line 107
4489 head = *mem_22;
4490#line 108
4491 mem_23 = (void **)temp;
4492#line 108
4493 excep = *mem_23;
4494#line 109
4495 __cil_tmp17 = (void *)temp;
4496#line 109
4497 free(__cil_tmp17);
4498#line 110
4499 __utac__exception__cf_handler_reset(excep);
4500#line 820 "libacc.c"
4501 retValue_acc = excep;
4502 }
4503#line 822
4504 return (retValue_acc);
4505 } else {
4506
4507 }
4508#line 114
4509 if (mode == 2) {
4510#line 118 "libacc.c"
4511 if (head) {
4512#line 831
4513 mem_24 = (void **)head;
4514#line 831
4515 retValue_acc = *mem_24;
4516#line 833
4517 return (retValue_acc);
4518 } else {
4519#line 837 "libacc.c"
4520 retValue_acc = (void *)0;
4521#line 839
4522 return (retValue_acc);
4523 }
4524 } else {
4525
4526 }
4527#line 846 "libacc.c"
4528 return (retValue_acc);
4529}
4530}
4531#line 122 "libacc.c"
4532void *__utac__get_this_arg(int i , struct JoinPoint *this )
4533{ void *retValue_acc ;
4534 unsigned long __cil_tmp4 ;
4535 unsigned long __cil_tmp5 ;
4536 int __cil_tmp6 ;
4537 int __cil_tmp7 ;
4538 unsigned long __cil_tmp8 ;
4539 unsigned long __cil_tmp9 ;
4540 void **__cil_tmp10 ;
4541 void **__cil_tmp11 ;
4542 int *mem_12 ;
4543 void ***mem_13 ;
4544
4545 {
4546#line 123
4547 if (i > 0) {
4548 {
4549#line 123
4550 __cil_tmp4 = (unsigned long )this;
4551#line 123
4552 __cil_tmp5 = __cil_tmp4 + 16;
4553#line 123
4554 mem_12 = (int *)__cil_tmp5;
4555#line 123
4556 __cil_tmp6 = *mem_12;
4557#line 123
4558 if (i <= __cil_tmp6) {
4559
4560 } else {
4561 {
4562#line 123
4563 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4564 123U, "__utac__get_this_arg");
4565 }
4566 }
4567 }
4568 } else {
4569 {
4570#line 123
4571 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4572 123U, "__utac__get_this_arg");
4573 }
4574 }
4575#line 870 "libacc.c"
4576 __cil_tmp7 = i - 1;
4577#line 870
4578 __cil_tmp8 = (unsigned long )this;
4579#line 870
4580 __cil_tmp9 = __cil_tmp8 + 8;
4581#line 870
4582 mem_13 = (void ***)__cil_tmp9;
4583#line 870
4584 __cil_tmp10 = *mem_13;
4585#line 870
4586 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4587#line 870
4588 retValue_acc = *__cil_tmp11;
4589#line 872
4590 return (retValue_acc);
4591#line 879
4592 return (retValue_acc);
4593}
4594}
4595#line 129 "libacc.c"
4596char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
4597{ char const *retValue_acc ;
4598 unsigned long __cil_tmp4 ;
4599 unsigned long __cil_tmp5 ;
4600 int __cil_tmp6 ;
4601 int __cil_tmp7 ;
4602 unsigned long __cil_tmp8 ;
4603 unsigned long __cil_tmp9 ;
4604 char const **__cil_tmp10 ;
4605 char const **__cil_tmp11 ;
4606 int *mem_12 ;
4607 char const ***mem_13 ;
4608
4609 {
4610#line 131
4611 if (i > 0) {
4612 {
4613#line 131
4614 __cil_tmp4 = (unsigned long )this;
4615#line 131
4616 __cil_tmp5 = __cil_tmp4 + 16;
4617#line 131
4618 mem_12 = (int *)__cil_tmp5;
4619#line 131
4620 __cil_tmp6 = *mem_12;
4621#line 131
4622 if (i <= __cil_tmp6) {
4623
4624 } else {
4625 {
4626#line 131
4627 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4628 131U, "__utac__get_this_argtype");
4629 }
4630 }
4631 }
4632 } else {
4633 {
4634#line 131
4635 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4636 131U, "__utac__get_this_argtype");
4637 }
4638 }
4639#line 903 "libacc.c"
4640 __cil_tmp7 = i - 1;
4641#line 903
4642 __cil_tmp8 = (unsigned long )this;
4643#line 903
4644 __cil_tmp9 = __cil_tmp8 + 24;
4645#line 903
4646 mem_13 = (char const ***)__cil_tmp9;
4647#line 903
4648 __cil_tmp10 = *mem_13;
4649#line 903
4650 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4651#line 903
4652 retValue_acc = *__cil_tmp11;
4653#line 905
4654 return (retValue_acc);
4655#line 912
4656 return (retValue_acc);
4657}
4658}
4659#line 1 "UnitTests.o"
4660#pragma merger(0,"UnitTests.i","")
4661#line 24 "UnitTests.c"
4662void spec1(void)
4663{ int tmp ;
4664 int tmp___0 ;
4665 int i ;
4666 int tmp___1 ;
4667
4668 {
4669 {
4670#line 25
4671 initBottomUp();
4672#line 26
4673 tmp = getOrigin(5);
4674#line 26
4675 initPersonOnFloor(5, tmp);
4676#line 27
4677 printState();
4678#line 30
4679 tmp___0 = getOrigin(2);
4680#line 30
4681 initPersonOnFloor(2, tmp___0);
4682#line 31
4683 printState();
4684#line 35
4685 i = 0;
4686 }
4687 {
4688#line 35
4689 while (1) {
4690 while_8_continue: ;
4691#line 35
4692 if (i < cleanupTimeShifts) {
4693 {
4694#line 35
4695 tmp___1 = isBlocked();
4696 }
4697#line 35
4698 if (tmp___1 != 1) {
4699
4700 } else {
4701 goto while_8_break;
4702 }
4703 } else {
4704 goto while_8_break;
4705 }
4706 {
4707#line 36
4708 timeShift();
4709#line 37
4710 printState();
4711#line 35
4712 i = i + 1;
4713 }
4714 }
4715 while_8_break: ;
4716 }
4717#line 1079 "UnitTests.c"
4718 return;
4719}
4720}
4721#line 42 "UnitTests.c"
4722void spec14(void)
4723{ int tmp ;
4724 int tmp___0 ;
4725 int i ;
4726 int tmp___1 ;
4727
4728 {
4729 {
4730#line 43
4731 initTopDown();
4732#line 44
4733 tmp = getOrigin(5);
4734#line 44
4735 initPersonOnFloor(5, tmp);
4736#line 45
4737 printState();
4738#line 47
4739 timeShift();
4740#line 48
4741 timeShift();
4742#line 49
4743 timeShift();
4744#line 50
4745 timeShift();
4746#line 52
4747 tmp___0 = getOrigin(0);
4748#line 52
4749 initPersonOnFloor(0, tmp___0);
4750#line 53
4751 printState();
4752#line 57
4753 i = 0;
4754 }
4755 {
4756#line 57
4757 while (1) {
4758 while_9_continue: ;
4759#line 57
4760 if (i < cleanupTimeShifts) {
4761 {
4762#line 57
4763 tmp___1 = isBlocked();
4764 }
4765#line 57
4766 if (tmp___1 != 1) {
4767
4768 } else {
4769 goto while_9_break;
4770 }
4771 } else {
4772 goto while_9_break;
4773 }
4774 {
4775#line 58
4776 timeShift();
4777#line 59
4778 printState();
4779#line 57
4780 i = i + 1;
4781 }
4782 }
4783 while_9_break: ;
4784 }
4785#line 1125 "UnitTests.c"
4786 return;
4787}
4788}
4789#line 1 "Specification2_spec.o"
4790#pragma merger(0,"Specification2_spec.i","")
4791#line 7 "Specification2_spec.c"
4792int floorButtons_spc2_0 ;
4793#line 8 "Specification2_spec.c"
4794int floorButtons_spc2_1 ;
4795#line 9 "Specification2_spec.c"
4796int floorButtons_spc2_2 ;
4797#line 10 "Specification2_spec.c"
4798int floorButtons_spc2_3 ;
4799#line 11 "Specification2_spec.c"
4800int floorButtons_spc2_4 ;
4801#line 15 "Specification2_spec.c"
4802void __utac_acc__Specification2_spec__1(void)
4803{
4804
4805 {
4806#line 17
4807 floorButtons_spc2_0 = 0;
4808#line 18
4809 floorButtons_spc2_1 = 0;
4810#line 19
4811 floorButtons_spc2_2 = 0;
4812#line 20
4813 floorButtons_spc2_3 = 0;
4814#line 21
4815 floorButtons_spc2_4 = 0;
4816#line 21
4817 return;
4818}
4819}
4820#line 25 "Specification2_spec.c"
4821void __utac_acc__Specification2_spec__2(int floor )
4822{
4823
4824 {
4825#line 33
4826 if (floor == 0) {
4827#line 34
4828 floorButtons_spc2_0 = 1;
4829 } else {
4830#line 35
4831 if (floor == 1) {
4832#line 36
4833 floorButtons_spc2_1 = 1;
4834 } else {
4835#line 37
4836 if (floor == 2) {
4837#line 38
4838 floorButtons_spc2_2 = 1;
4839 } else {
4840#line 39
4841 if (floor == 3) {
4842#line 40
4843 floorButtons_spc2_3 = 1;
4844 } else {
4845#line 41
4846 if (floor == 4) {
4847#line 42
4848 floorButtons_spc2_4 = 1;
4849 } else {
4850
4851 }
4852 }
4853 }
4854 }
4855 }
4856#line 42
4857 return;
4858}
4859}
4860#line 35 "Specification2_spec.c"
4861void __utac_acc__Specification2_spec__3(void)
4862{ int floor ;
4863 int tmp ;
4864 int tmp___0 ;
4865 int tmp___1 ;
4866 int tmp___2 ;
4867 int tmp___3 ;
4868 int tmp___4 ;
4869
4870 {
4871 {
4872#line 37
4873 tmp = getCurrentFloorID();
4874#line 37
4875 floor = tmp;
4876 }
4877#line 38
4878 if (floor == 0) {
4879#line 38
4880 if (floorButtons_spc2_0) {
4881 {
4882#line 38
4883 tmp___4 = areDoorsOpen();
4884 }
4885#line 38
4886 if (tmp___4) {
4887#line 39
4888 floorButtons_spc2_0 = 0;
4889 } else {
4890 goto _L___6;
4891 }
4892 } else {
4893 goto _L___6;
4894 }
4895 } else {
4896 _L___6:
4897#line 40
4898 if (floor == 1) {
4899#line 40
4900 if (floorButtons_spc2_1) {
4901 {
4902#line 40
4903 tmp___3 = areDoorsOpen();
4904 }
4905#line 40
4906 if (tmp___3) {
4907#line 41
4908 floorButtons_spc2_1 = 0;
4909 } else {
4910 goto _L___4;
4911 }
4912 } else {
4913 goto _L___4;
4914 }
4915 } else {
4916 _L___4:
4917#line 42
4918 if (floor == 2) {
4919#line 42
4920 if (floorButtons_spc2_2) {
4921 {
4922#line 42
4923 tmp___2 = areDoorsOpen();
4924 }
4925#line 42
4926 if (tmp___2) {
4927#line 43
4928 floorButtons_spc2_2 = 0;
4929 } else {
4930 goto _L___2;
4931 }
4932 } else {
4933 goto _L___2;
4934 }
4935 } else {
4936 _L___2:
4937#line 44
4938 if (floor == 3) {
4939#line 44
4940 if (floorButtons_spc2_3) {
4941 {
4942#line 44
4943 tmp___1 = areDoorsOpen();
4944 }
4945#line 44
4946 if (tmp___1) {
4947#line 45
4948 floorButtons_spc2_3 = 0;
4949 } else {
4950 goto _L___0;
4951 }
4952 } else {
4953 goto _L___0;
4954 }
4955 } else {
4956 _L___0:
4957#line 46
4958 if (floor == 4) {
4959#line 46
4960 if (floorButtons_spc2_4) {
4961 {
4962#line 46
4963 tmp___0 = areDoorsOpen();
4964 }
4965#line 46
4966 if (tmp___0) {
4967#line 47
4968 floorButtons_spc2_4 = 0;
4969 } else {
4970
4971 }
4972 } else {
4973
4974 }
4975 } else {
4976
4977 }
4978 }
4979 }
4980 }
4981 }
4982#line 47
4983 return;
4984}
4985}
4986#line 52 "Specification2_spec.c"
4987void __utac_acc__Specification2_spec__4(void)
4988{
4989
4990 {
4991#line 60
4992 if (floorButtons_spc2_0) {
4993 {
4994#line 61
4995 __automaton_fail();
4996 }
4997 } else {
4998#line 62
4999 if (floorButtons_spc2_1) {
5000 {
5001#line 63
5002 __automaton_fail();
5003 }
5004 } else {
5005#line 64
5006 if (floorButtons_spc2_2) {
5007 {
5008#line 65
5009 __automaton_fail();
5010 }
5011 } else {
5012#line 66
5013 if (floorButtons_spc2_3) {
5014 {
5015#line 67
5016 __automaton_fail();
5017 }
5018 } else {
5019#line 68
5020 if (floorButtons_spc2_4) {
5021 {
5022#line 69
5023 __automaton_fail();
5024 }
5025 } else {
5026
5027 }
5028 }
5029 }
5030 }
5031 }
5032#line 69
5033 return;
5034}
5035}