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