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