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