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