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