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