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