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