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