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