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