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