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