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