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