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