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