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