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