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