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