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