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