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