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