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