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