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