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