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