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