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