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