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