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