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