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