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