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