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