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