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