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