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