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