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