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