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