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