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