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