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