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