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