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