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