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