1extern int __VERIFIER_nondet_int(void);
2extern int printf (__const char *__restrict __format, ...);
3
4
5
6#line 2 "libacc.c"
7struct JoinPoint {
8 void **(*fp)(struct JoinPoint * ) ;
9 void **args ;
10 int argsCount ;
11 char const **argsType ;
12 void *(*arg)(int , struct JoinPoint * ) ;
13 char const *(*argType)(int , struct JoinPoint * ) ;
14 void **retValue ;
15 char const *retType ;
16 char const *funcName ;
17 char const *targetName ;
18 char const *fileName ;
19 char const *kind ;
20 void *excep_return ;
21};
22#line 18 "libacc.c"
23struct __UTAC__CFLOW_FUNC {
24 int (*func)(int , int ) ;
25 int val ;
26 struct __UTAC__CFLOW_FUNC *next ;
27};
28#line 18 "libacc.c"
29struct __UTAC__EXCEPTION {
30 void *jumpbuf ;
31 unsigned long long prtValue ;
32 int pops ;
33 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
34};
35#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
36typedef unsigned long size_t;
37#line 76 "libacc.c"
38struct __ACC__ERR {
39 void *v ;
40 struct __ACC__ERR *next ;
41};
42#line 1 "Specification2_spec.o"
43#pragma merger(0,"Specification2_spec.i","")
44#line 4 "wsllib.h"
45void __automaton_fail(void) ;
46#line 10 "MinePump.h"
47int isPumpRunning(void) ;
48#line 10 "Environment.h"
49int isMethaneLevelCritical(void) ;
50#line 7 "Specification2_spec.c"
51int methAndRunningLastTime ;
52#line 11 "Specification2_spec.c"
53__inline void __utac_acc__Specification2_spec__1(void)
54{
55
56 {
57#line 13
58 methAndRunningLastTime = 0;
59#line 13
60 return;
61}
62}
63#line 17 "Specification2_spec.c"
64__inline void __utac_acc__Specification2_spec__2(void)
65{ int tmp ;
66 int tmp___0 ;
67
68 {
69 {
70#line 27
71 tmp = isMethaneLevelCritical();
72 }
73#line 27
74 if (tmp) {
75 {
76#line 27
77 tmp___0 = isPumpRunning();
78 }
79#line 27
80 if (tmp___0) {
81#line 24
82 if (methAndRunningLastTime) {
83 {
84#line 21
85 __automaton_fail();
86 }
87 } else {
88#line 23
89 methAndRunningLastTime = 1;
90 }
91 } else {
92#line 26
93 methAndRunningLastTime = 0;
94 }
95 } else {
96#line 26
97 methAndRunningLastTime = 0;
98 }
99#line 26
100 return;
101}
102}
103#line 1 "libacc.o"
104#pragma merger(0,"libacc.i","")
105#line 73 "/usr/include/assert.h"
106extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
107 char const *__file ,
108 unsigned int __line ,
109 char const *__function ) ;
110#line 471 "/usr/include/stdlib.h"
111extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
112#line 488
113extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
114#line 32 "libacc.c"
115void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
116 int ) ,
117 int val )
118{ struct __UTAC__EXCEPTION *excep ;
119 struct __UTAC__CFLOW_FUNC *cf ;
120 void *tmp ;
121 unsigned long __cil_tmp7 ;
122 unsigned long __cil_tmp8 ;
123 unsigned long __cil_tmp9 ;
124 unsigned long __cil_tmp10 ;
125 unsigned long __cil_tmp11 ;
126 unsigned long __cil_tmp12 ;
127 unsigned long __cil_tmp13 ;
128 unsigned long __cil_tmp14 ;
129 int (**mem_15)(int , int ) ;
130 int *mem_16 ;
131 struct __UTAC__CFLOW_FUNC **mem_17 ;
132 struct __UTAC__CFLOW_FUNC **mem_18 ;
133 struct __UTAC__CFLOW_FUNC **mem_19 ;
134
135 {
136 {
137#line 33
138 excep = (struct __UTAC__EXCEPTION *)exception;
139#line 34
140 tmp = malloc(24UL);
141#line 34
142 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
143#line 36
144 mem_15 = (int (**)(int , int ))cf;
145#line 36
146 *mem_15 = cflow_func;
147#line 37
148 __cil_tmp7 = (unsigned long )cf;
149#line 37
150 __cil_tmp8 = __cil_tmp7 + 8;
151#line 37
152 mem_16 = (int *)__cil_tmp8;
153#line 37
154 *mem_16 = val;
155#line 38
156 __cil_tmp9 = (unsigned long )cf;
157#line 38
158 __cil_tmp10 = __cil_tmp9 + 16;
159#line 38
160 __cil_tmp11 = (unsigned long )excep;
161#line 38
162 __cil_tmp12 = __cil_tmp11 + 24;
163#line 38
164 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
165#line 38
166 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
167#line 38
168 *mem_17 = *mem_18;
169#line 39
170 __cil_tmp13 = (unsigned long )excep;
171#line 39
172 __cil_tmp14 = __cil_tmp13 + 24;
173#line 39
174 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
175#line 39
176 *mem_19 = cf;
177 }
178#line 654 "libacc.c"
179 return;
180}
181}
182#line 44 "libacc.c"
183void __utac__exception__cf_handler_free(void *exception )
184{ struct __UTAC__EXCEPTION *excep ;
185 struct __UTAC__CFLOW_FUNC *cf ;
186 struct __UTAC__CFLOW_FUNC *tmp ;
187 unsigned long __cil_tmp5 ;
188 unsigned long __cil_tmp6 ;
189 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
190 unsigned long __cil_tmp8 ;
191 unsigned long __cil_tmp9 ;
192 unsigned long __cil_tmp10 ;
193 unsigned long __cil_tmp11 ;
194 void *__cil_tmp12 ;
195 unsigned long __cil_tmp13 ;
196 unsigned long __cil_tmp14 ;
197 struct __UTAC__CFLOW_FUNC **mem_15 ;
198 struct __UTAC__CFLOW_FUNC **mem_16 ;
199 struct __UTAC__CFLOW_FUNC **mem_17 ;
200
201 {
202#line 45
203 excep = (struct __UTAC__EXCEPTION *)exception;
204#line 46
205 __cil_tmp5 = (unsigned long )excep;
206#line 46
207 __cil_tmp6 = __cil_tmp5 + 24;
208#line 46
209 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
210#line 46
211 cf = *mem_15;
212 {
213#line 49
214 while (1) {
215 while_0_continue: ;
216 {
217#line 49
218 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
219#line 49
220 __cil_tmp8 = (unsigned long )__cil_tmp7;
221#line 49
222 __cil_tmp9 = (unsigned long )cf;
223#line 49
224 if (__cil_tmp9 != __cil_tmp8) {
225
226 } else {
227 goto while_0_break;
228 }
229 }
230 {
231#line 50
232 tmp = cf;
233#line 51
234 __cil_tmp10 = (unsigned long )cf;
235#line 51
236 __cil_tmp11 = __cil_tmp10 + 16;
237#line 51
238 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
239#line 51
240 cf = *mem_16;
241#line 52
242 __cil_tmp12 = (void *)tmp;
243#line 52
244 free(__cil_tmp12);
245 }
246 }
247 while_0_break: ;
248 }
249#line 55
250 __cil_tmp13 = (unsigned long )excep;
251#line 55
252 __cil_tmp14 = __cil_tmp13 + 24;
253#line 55
254 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
255#line 55
256 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
257#line 694 "libacc.c"
258 return;
259}
260}
261#line 59 "libacc.c"
262void __utac__exception__cf_handler_reset(void *exception )
263{ struct __UTAC__EXCEPTION *excep ;
264 struct __UTAC__CFLOW_FUNC *cf ;
265 unsigned long __cil_tmp5 ;
266 unsigned long __cil_tmp6 ;
267 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
268 unsigned long __cil_tmp8 ;
269 unsigned long __cil_tmp9 ;
270 int (*__cil_tmp10)(int , int ) ;
271 unsigned long __cil_tmp11 ;
272 unsigned long __cil_tmp12 ;
273 int __cil_tmp13 ;
274 unsigned long __cil_tmp14 ;
275 unsigned long __cil_tmp15 ;
276 struct __UTAC__CFLOW_FUNC **mem_16 ;
277 int (**mem_17)(int , int ) ;
278 int *mem_18 ;
279 struct __UTAC__CFLOW_FUNC **mem_19 ;
280
281 {
282#line 60
283 excep = (struct __UTAC__EXCEPTION *)exception;
284#line 61
285 __cil_tmp5 = (unsigned long )excep;
286#line 61
287 __cil_tmp6 = __cil_tmp5 + 24;
288#line 61
289 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
290#line 61
291 cf = *mem_16;
292 {
293#line 64
294 while (1) {
295 while_1_continue: ;
296 {
297#line 64
298 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
299#line 64
300 __cil_tmp8 = (unsigned long )__cil_tmp7;
301#line 64
302 __cil_tmp9 = (unsigned long )cf;
303#line 64
304 if (__cil_tmp9 != __cil_tmp8) {
305
306 } else {
307 goto while_1_break;
308 }
309 }
310 {
311#line 65
312 mem_17 = (int (**)(int , int ))cf;
313#line 65
314 __cil_tmp10 = *mem_17;
315#line 65
316 __cil_tmp11 = (unsigned long )cf;
317#line 65
318 __cil_tmp12 = __cil_tmp11 + 8;
319#line 65
320 mem_18 = (int *)__cil_tmp12;
321#line 65
322 __cil_tmp13 = *mem_18;
323#line 65
324 (*__cil_tmp10)(4, __cil_tmp13);
325#line 66
326 __cil_tmp14 = (unsigned long )cf;
327#line 66
328 __cil_tmp15 = __cil_tmp14 + 16;
329#line 66
330 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
331#line 66
332 cf = *mem_19;
333 }
334 }
335 while_1_break: ;
336 }
337 {
338#line 69
339 __utac__exception__cf_handler_free(exception);
340 }
341#line 732 "libacc.c"
342 return;
343}
344}
345#line 80 "libacc.c"
346void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
347#line 80 "libacc.c"
348static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
349#line 79 "libacc.c"
350void *__utac__error_stack_mgt(void *env , int mode , int count )
351{ void *retValue_acc ;
352 struct __ACC__ERR *new ;
353 void *tmp ;
354 struct __ACC__ERR *temp ;
355 struct __ACC__ERR *next ;
356 void *excep ;
357 unsigned long __cil_tmp10 ;
358 unsigned long __cil_tmp11 ;
359 unsigned long __cil_tmp12 ;
360 unsigned long __cil_tmp13 ;
361 void *__cil_tmp14 ;
362 unsigned long __cil_tmp15 ;
363 unsigned long __cil_tmp16 ;
364 void *__cil_tmp17 ;
365 void **mem_18 ;
366 struct __ACC__ERR **mem_19 ;
367 struct __ACC__ERR **mem_20 ;
368 void **mem_21 ;
369 struct __ACC__ERR **mem_22 ;
370 void **mem_23 ;
371 void **mem_24 ;
372
373 {
374#line 82 "libacc.c"
375 if (count == 0) {
376#line 758 "libacc.c"
377 return (retValue_acc);
378 } else {
379
380 }
381#line 86 "libacc.c"
382 if (mode == 0) {
383 {
384#line 87
385 tmp = malloc(16UL);
386#line 87
387 new = (struct __ACC__ERR *)tmp;
388#line 88
389 mem_18 = (void **)new;
390#line 88
391 *mem_18 = env;
392#line 89
393 __cil_tmp10 = (unsigned long )new;
394#line 89
395 __cil_tmp11 = __cil_tmp10 + 8;
396#line 89
397 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
398#line 89
399 *mem_19 = head;
400#line 90
401 head = new;
402#line 776 "libacc.c"
403 retValue_acc = (void *)new;
404 }
405#line 778
406 return (retValue_acc);
407 } else {
408
409 }
410#line 94 "libacc.c"
411 if (mode == 1) {
412#line 95
413 temp = head;
414 {
415#line 98
416 while (1) {
417 while_2_continue: ;
418#line 98
419 if (count > 1) {
420
421 } else {
422 goto while_2_break;
423 }
424 {
425#line 99
426 __cil_tmp12 = (unsigned long )temp;
427#line 99
428 __cil_tmp13 = __cil_tmp12 + 8;
429#line 99
430 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
431#line 99
432 next = *mem_20;
433#line 100
434 mem_21 = (void **)temp;
435#line 100
436 excep = *mem_21;
437#line 101
438 __cil_tmp14 = (void *)temp;
439#line 101
440 free(__cil_tmp14);
441#line 102
442 __utac__exception__cf_handler_reset(excep);
443#line 103
444 temp = next;
445#line 104
446 count = count - 1;
447 }
448 }
449 while_2_break: ;
450 }
451 {
452#line 107
453 __cil_tmp15 = (unsigned long )temp;
454#line 107
455 __cil_tmp16 = __cil_tmp15 + 8;
456#line 107
457 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
458#line 107
459 head = *mem_22;
460#line 108
461 mem_23 = (void **)temp;
462#line 108
463 excep = *mem_23;
464#line 109
465 __cil_tmp17 = (void *)temp;
466#line 109
467 free(__cil_tmp17);
468#line 110
469 __utac__exception__cf_handler_reset(excep);
470#line 820 "libacc.c"
471 retValue_acc = excep;
472 }
473#line 822
474 return (retValue_acc);
475 } else {
476
477 }
478#line 114
479 if (mode == 2) {
480#line 118 "libacc.c"
481 if (head) {
482#line 831
483 mem_24 = (void **)head;
484#line 831
485 retValue_acc = *mem_24;
486#line 833
487 return (retValue_acc);
488 } else {
489#line 837 "libacc.c"
490 retValue_acc = (void *)0;
491#line 839
492 return (retValue_acc);
493 }
494 } else {
495
496 }
497#line 846 "libacc.c"
498 return (retValue_acc);
499}
500}
501#line 122 "libacc.c"
502void *__utac__get_this_arg(int i , struct JoinPoint *this )
503{ void *retValue_acc ;
504 unsigned long __cil_tmp4 ;
505 unsigned long __cil_tmp5 ;
506 int __cil_tmp6 ;
507 int __cil_tmp7 ;
508 unsigned long __cil_tmp8 ;
509 unsigned long __cil_tmp9 ;
510 void **__cil_tmp10 ;
511 void **__cil_tmp11 ;
512 int *mem_12 ;
513 void ***mem_13 ;
514
515 {
516#line 123
517 if (i > 0) {
518 {
519#line 123
520 __cil_tmp4 = (unsigned long )this;
521#line 123
522 __cil_tmp5 = __cil_tmp4 + 16;
523#line 123
524 mem_12 = (int *)__cil_tmp5;
525#line 123
526 __cil_tmp6 = *mem_12;
527#line 123
528 if (i <= __cil_tmp6) {
529
530 } else {
531 {
532#line 123
533 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
534 123U, "__utac__get_this_arg");
535 }
536 }
537 }
538 } else {
539 {
540#line 123
541 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
542 123U, "__utac__get_this_arg");
543 }
544 }
545#line 870 "libacc.c"
546 __cil_tmp7 = i - 1;
547#line 870
548 __cil_tmp8 = (unsigned long )this;
549#line 870
550 __cil_tmp9 = __cil_tmp8 + 8;
551#line 870
552 mem_13 = (void ***)__cil_tmp9;
553#line 870
554 __cil_tmp10 = *mem_13;
555#line 870
556 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
557#line 870
558 retValue_acc = *__cil_tmp11;
559#line 872
560 return (retValue_acc);
561#line 879
562 return (retValue_acc);
563}
564}
565#line 129 "libacc.c"
566char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
567{ char const *retValue_acc ;
568 unsigned long __cil_tmp4 ;
569 unsigned long __cil_tmp5 ;
570 int __cil_tmp6 ;
571 int __cil_tmp7 ;
572 unsigned long __cil_tmp8 ;
573 unsigned long __cil_tmp9 ;
574 char const **__cil_tmp10 ;
575 char const **__cil_tmp11 ;
576 int *mem_12 ;
577 char const ***mem_13 ;
578
579 {
580#line 131
581 if (i > 0) {
582 {
583#line 131
584 __cil_tmp4 = (unsigned long )this;
585#line 131
586 __cil_tmp5 = __cil_tmp4 + 16;
587#line 131
588 mem_12 = (int *)__cil_tmp5;
589#line 131
590 __cil_tmp6 = *mem_12;
591#line 131
592 if (i <= __cil_tmp6) {
593
594 } else {
595 {
596#line 131
597 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
598 131U, "__utac__get_this_argtype");
599 }
600 }
601 }
602 } else {
603 {
604#line 131
605 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
606 131U, "__utac__get_this_argtype");
607 }
608 }
609#line 903 "libacc.c"
610 __cil_tmp7 = i - 1;
611#line 903
612 __cil_tmp8 = (unsigned long )this;
613#line 903
614 __cil_tmp9 = __cil_tmp8 + 24;
615#line 903
616 mem_13 = (char const ***)__cil_tmp9;
617#line 903
618 __cil_tmp10 = *mem_13;
619#line 903
620 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
621#line 903
622 retValue_acc = *__cil_tmp11;
623#line 905
624 return (retValue_acc);
625#line 912
626 return (retValue_acc);
627}
628}
629#line 1 "MinePump.o"
630#pragma merger(0,"MinePump.i","")
631#line 4 "Environment.h"
632void lowerWaterLevel(void) ;
633#line 15
634void printEnvironment(void) ;
635#line 16
636int isHighWaterSensorDry(void) ;
637#line 4 "MinePump.h"
638void timeShift(void) ;
639#line 6
640void activatePump(void) ;
641#line 8
642void deactivatePump(void) ;
643#line 13
644void printPump(void) ;
645#line 7 "MinePump.c"
646int pumpRunning = 0;
647#line 9 "MinePump.c"
648int systemActive = 1;
649#line 16
650void processEnvironment(void) ;
651#line 12 "MinePump.c"
652void timeShift(void)
653{
654
655 {
656#line 15
657 if (pumpRunning) {
658 {
659#line 16
660 lowerWaterLevel();
661 }
662 } else {
663
664 }
665#line 15
666 if (systemActive) {
667 {
668#line 16
669 processEnvironment();
670 }
671 } else {
672
673 }
674 {
675#line 97 "MinePump.c"
676 __utac_acc__Specification2_spec__2();
677 }
678#line 103
679 return;
680}
681}
682#line 19 "MinePump.c"
683void processEnvironment__wrappee__base(void)
684{
685
686 {
687#line 121 "MinePump.c"
688 return;
689}
690}
691#line 28 "MinePump.c"
692int isHighWaterLevel(void) ;
693#line 23 "MinePump.c"
694void processEnvironment(void)
695{ int tmp ;
696
697 {
698#line 28
699 if (! pumpRunning) {
700 {
701#line 28
702 tmp = isHighWaterLevel();
703 }
704#line 28
705 if (tmp) {
706 {
707#line 25
708 activatePump();
709 }
710 } else {
711 {
712#line 27
713 processEnvironment__wrappee__base();
714 }
715 }
716 } else {
717 {
718#line 27
719 processEnvironment__wrappee__base();
720 }
721 }
722#line 147 "MinePump.c"
723 return;
724}
725}
726#line 32 "MinePump.c"
727void activatePump__wrappee__highWaterSensor(void)
728{
729
730 {
731#line 33
732 pumpRunning = 1;
733#line 167 "MinePump.c"
734 return;
735}
736}
737#line 40 "MinePump.c"
738int isMethaneAlarm(void) ;
739#line 35 "MinePump.c"
740void activatePump(void)
741{ int tmp ;
742
743 {
744 {
745#line 40
746 tmp = isMethaneAlarm();
747 }
748#line 40
749 if (tmp) {
750
751 } else {
752 {
753#line 37
754 activatePump__wrappee__highWaterSensor();
755 }
756 }
757#line 191 "MinePump.c"
758 return;
759}
760}
761#line 44 "MinePump.c"
762void deactivatePump(void)
763{
764
765 {
766#line 45
767 pumpRunning = 0;
768#line 211 "MinePump.c"
769 return;
770}
771}
772#line 49 "MinePump.c"
773int isMethaneAlarm(void)
774{ int retValue_acc ;
775
776 {
777 {
778#line 229 "MinePump.c"
779 retValue_acc = isMethaneLevelCritical();
780 }
781#line 231
782 return (retValue_acc);
783#line 238
784 return (retValue_acc);
785}
786}
787#line 54 "MinePump.c"
788int isPumpRunning(void)
789{ int retValue_acc ;
790
791 {
792#line 260 "MinePump.c"
793 retValue_acc = pumpRunning;
794#line 262
795 return (retValue_acc);
796#line 269
797 return (retValue_acc);
798}
799}
800#line 60 "MinePump.c"
801#line 59 "MinePump.c"
802void printPump(void)
803{
804
805 {
806 {
807#line 60
808 printf("Pump(System:");
809 }
810#line 61
811 if (systemActive) {
812 {
813#line 62
814 printf("On");
815 }
816 } else {
817 {
818#line 63
819 printf("Off");
820 }
821 }
822 {
823#line 65
824 printf(",Pump:");
825 }
826#line 66
827 if (pumpRunning) {
828 {
829#line 67
830 printf("On");
831 }
832 } else {
833 {
834#line 68
835 printf("Off");
836 }
837 }
838 {
839#line 70
840 printf(") ");
841#line 71
842 printEnvironment();
843#line 72
844 printf("\n");
845 }
846#line 309 "MinePump.c"
847 return;
848}
849}
850#line 74 "MinePump.c"
851int isHighWaterLevel(void)
852{ int retValue_acc ;
853 int tmp ;
854 int tmp___0 ;
855
856 {
857 {
858#line 327 "MinePump.c"
859 tmp = isHighWaterSensorDry();
860 }
861#line 327
862 if (tmp) {
863#line 327
864 tmp___0 = 0;
865 } else {
866#line 327
867 tmp___0 = 1;
868 }
869#line 327
870 retValue_acc = tmp___0;
871#line 329
872 return (retValue_acc);
873#line 336
874 return (retValue_acc);
875}
876}
877#line 1 "Environment.o"
878#pragma merger(0,"Environment.i","")
879#line 6 "Environment.h"
880void waterRise(void) ;
881#line 8
882void changeMethaneLevel(void) ;
883#line 12
884int getWaterLevel(void) ;
885#line 9 "Environment.c"
886int waterLevel = 1;
887#line 12 "Environment.c"
888int methaneLevelCritical = 0;
889#line 15 "Environment.c"
890void lowerWaterLevel(void)
891{
892
893 {
894#line 19
895 if (waterLevel > 0) {
896#line 17
897 waterLevel = waterLevel - 1;
898 } else {
899
900 }
901#line 83 "Environment.c"
902 return;
903}
904}
905#line 22 "Environment.c"
906void waterRise(void)
907{
908
909 {
910#line 26
911 if (waterLevel < 2) {
912#line 24
913 waterLevel = waterLevel + 1;
914 } else {
915
916 }
917#line 106 "Environment.c"
918 return;
919}
920}
921#line 29 "Environment.c"
922void changeMethaneLevel(void)
923{
924
925 {
926#line 34
927 if (methaneLevelCritical) {
928#line 31
929 methaneLevelCritical = 0;
930 } else {
931#line 33
932 methaneLevelCritical = 1;
933 }
934#line 132 "Environment.c"
935 return;
936}
937}
938#line 38 "Environment.c"
939int isMethaneLevelCritical(void)
940{ int retValue_acc ;
941
942 {
943#line 150 "Environment.c"
944 retValue_acc = methaneLevelCritical;
945#line 152
946 return (retValue_acc);
947#line 159
948 return (retValue_acc);
949}
950}
951#line 44 "Environment.c"
952void printEnvironment(void)
953{
954
955 {
956 {
957#line 45
958 printf("Env(Water:%i", waterLevel);
959#line 46
960 printf(",Meth:");
961 }
962#line 47
963 if (methaneLevelCritical) {
964 {
965#line 48
966 printf("CRIT");
967 }
968 } else {
969 {
970#line 49
971 printf("OK");
972 }
973 }
974 {
975#line 51
976 printf(")");
977 }
978#line 191 "Environment.c"
979 return;
980}
981}
982#line 55 "Environment.c"
983int getWaterLevel(void)
984{ int retValue_acc ;
985
986 {
987#line 209 "Environment.c"
988 retValue_acc = waterLevel;
989#line 211
990 return (retValue_acc);
991#line 218
992 return (retValue_acc);
993}
994}
995#line 58 "Environment.c"
996int isHighWaterSensorDry(void)
997{ int retValue_acc ;
998
999 {
1000#line 65 "Environment.c"
1001 if (waterLevel < 2) {
1002#line 243
1003 retValue_acc = 1;
1004#line 245
1005 return (retValue_acc);
1006 } else {
1007#line 251 "Environment.c"
1008 retValue_acc = 0;
1009#line 253
1010 return (retValue_acc);
1011 }
1012#line 260 "Environment.c"
1013 return (retValue_acc);
1014}
1015}
1016#line 1 "scenario.o"
1017#pragma merger(0,"scenario.i","")
1018#line 7 "scenario.c"
1019#line 15
1020void cleanup(void) ;
1021#line 1 "scenario.c"
1022void test(void)
1023{ int splverifierCounter ;
1024 int tmp ;
1025 int tmp___0 ;
1026 int tmp___1 ;
1027 int tmp___2 ;
1028
1029 {
1030#line 2
1031 splverifierCounter = 0;
1032 {
1033#line 3
1034 while (1) {
1035 while_3_continue: ;
1036#line 3
1037 if (splverifierCounter < 4) {
1038
1039 } else {
1040 goto while_3_break;
1041 }
1042 {
1043#line 7
1044 tmp = __VERIFIER_nondet_int();
1045 }
1046#line 7
1047 if (tmp) {
1048 {
1049#line 5
1050 waterRise();
1051 }
1052 } else {
1053
1054 }
1055 {
1056#line 7
1057 tmp___0 = __VERIFIER_nondet_int();
1058 }
1059#line 7
1060 if (tmp___0) {
1061 {
1062#line 8
1063 changeMethaneLevel();
1064 }
1065 } else {
1066
1067 }
1068 {
1069#line 10
1070 tmp___2 = __VERIFIER_nondet_int();
1071 }
1072#line 10
1073 if (tmp___2) {
1074
1075 } else {
1076 {
1077#line 12
1078 tmp___1 = __VERIFIER_nondet_int();
1079 }
1080#line 12
1081 if (tmp___1) {
1082
1083 } else {
1084
1085 }
1086 }
1087 {
1088#line 13
1089 timeShift();
1090 }
1091 }
1092 while_3_break: ;
1093 }
1094 {
1095#line 15
1096 cleanup();
1097 }
1098#line 74 "scenario.c"
1099 return;
1100}
1101}
1102#line 1 "featureselect.o"
1103#pragma merger(0,"featureselect.i","")
1104#line 8 "featureselect.h"
1105int select_one(void) ;
1106#line 10
1107void select_features(void) ;
1108#line 12
1109void select_helpers(void) ;
1110#line 14
1111int valid_product(void) ;
1112#line 8 "featureselect.c"
1113int select_one(void)
1114{ int retValue_acc ;
1115 int choice = __VERIFIER_nondet_int();
1116
1117 {
1118#line 62 "featureselect.c"
1119 retValue_acc = choice;
1120#line 64
1121 return (retValue_acc);
1122#line 71
1123 return (retValue_acc);
1124}
1125}
1126#line 14 "featureselect.c"
1127void select_features(void)
1128{
1129
1130 {
1131#line 93 "featureselect.c"
1132 return;
1133}
1134}
1135#line 20 "featureselect.c"
1136void select_helpers(void)
1137{
1138
1139 {
1140#line 111 "featureselect.c"
1141 return;
1142}
1143}
1144#line 25 "featureselect.c"
1145int valid_product(void)
1146{ int retValue_acc ;
1147
1148 {
1149#line 129 "featureselect.c"
1150 retValue_acc = 1;
1151#line 131
1152 return (retValue_acc);
1153#line 138
1154 return (retValue_acc);
1155}
1156}
1157#line 1 "wsllib_check.o"
1158#pragma merger(0,"wsllib_check.i","")
1159#line 3 "wsllib_check.c"
1160void __automaton_fail(void)
1161{
1162
1163 {
1164 goto ERROR;
1165 ERROR: ;
1166#line 53 "wsllib_check.c"
1167 return;
1168}
1169}
1170#line 1 "Test.o"
1171#pragma merger(0,"Test.i","")
1172#line 8 "Test.c"
1173int cleanupTimeShifts = 4;
1174#line 11 "Test.c"
1175#line 17 "Test.c"
1176void cleanup(void)
1177{ int i ;
1178 int __cil_tmp2 ;
1179
1180 {
1181 {
1182#line 20
1183 timeShift();
1184#line 22
1185 i = 0;
1186 }
1187 {
1188#line 22
1189 while (1) {
1190 while_4_continue: ;
1191 {
1192#line 22
1193 __cil_tmp2 = cleanupTimeShifts - 1;
1194#line 22
1195 if (i < __cil_tmp2) {
1196
1197 } else {
1198 goto while_4_break;
1199 }
1200 }
1201 {
1202#line 23
1203 timeShift();
1204#line 22
1205 i = i + 1;
1206 }
1207 }
1208 while_4_break: ;
1209 }
1210#line 1111 "Test.c"
1211 return;
1212}
1213}
1214#line 56 "Test.c"
1215void Specification2(void)
1216{
1217
1218 {
1219 {
1220#line 57
1221 timeShift();
1222#line 57
1223 printPump();
1224#line 58
1225 timeShift();
1226#line 58
1227 printPump();
1228#line 59
1229 timeShift();
1230#line 59
1231 printPump();
1232#line 60
1233 waterRise();
1234#line 60
1235 printPump();
1236#line 61
1237 timeShift();
1238#line 61
1239 printPump();
1240#line 62
1241 changeMethaneLevel();
1242#line 62
1243 printPump();
1244#line 63
1245 timeShift();
1246#line 63
1247 printPump();
1248#line 64
1249 cleanup();
1250 }
1251#line 1159 "Test.c"
1252 return;
1253}
1254}
1255#line 67 "Test.c"
1256void setup(void)
1257{
1258
1259 {
1260#line 1177 "Test.c"
1261 return;
1262}
1263}
1264#line 74 "Test.c"
1265void runTest(void)
1266{
1267
1268 {
1269 {
1270#line 1190 "Test.c"
1271 __utac_acc__Specification2_spec__1();
1272#line 77 "Test.c"
1273 test();
1274 }
1275#line 1205 "Test.c"
1276 return;
1277}
1278}
1279#line 82 "Test.c"
1280int main(void)
1281{ int retValue_acc ;
1282 int tmp ;
1283
1284 {
1285 {
1286#line 83
1287 select_helpers();
1288#line 84
1289 select_features();
1290#line 85
1291 tmp = valid_product();
1292 }
1293#line 85
1294 if (tmp) {
1295 {
1296#line 86
1297 setup();
1298#line 87
1299 runTest();
1300 }
1301 } else {
1302
1303 }
1304#line 1234 "Test.c"
1305 retValue_acc = 0;
1306#line 1236
1307 return (retValue_acc);
1308#line 1243
1309 return (retValue_acc);
1310}
1311}