lustrec / bench / distrib / misc / ex8_e8_220 / mutants / ex8_e8_220.mutant.n79.lus @ 53aa0cb0
History | View | Annotate | Download (645 Bytes)
| 1 | 53aa0cb0 | ploc | node top |
|---|---|---|---|
| 2 | (beacon: bool; |
||
| 3 | second: bool) |
||
| 4 | returns |
||
| 5 | (OK: bool); |
||
| 6 | |||
| 7 | var |
||
| 8 | V19_late: bool; |
||
| 9 | V20_early: bool; |
||
| 10 | V63_diff: int; |
||
| 11 | V64_incr: int; |
||
| 12 | V65_PC: int; |
||
| 13 | |||
| 14 | let |
||
| 15 | OK = (true -> ((not V19_late) and (pre V20_early))); |
||
| 16 | V19_late = (false -> (if (pre V19_late) then (V63_diff < 0) else (V63_diff <= |
||
| 17 | -10))); |
||
| 18 | V20_early = (false -> (if (pre V20_early) then (V63_diff > 10) else (V63_diff |
||
| 19 | >= 10))); |
||
| 20 | V63_diff = (if false then 0 else (if (beacon and second) then (V65_PC + |
||
| 21 | V64_incr) else V65_PC)); |
||
| 22 | V64_incr = (if (beacon and (not second)) then 1 else (if (second and (not |
||
| 23 | beacon)) then 2 else 0)); |
||
| 24 | V65_PC = (0 -> (pre V63_diff)); |
||
| 25 | tel |