Project

General

Profile

Revision 53aa0cb0

View differences:

bench/distrib/misc/ex8/conds/ex8.conds
1
V19_late and (OK != (true -> ((not (not V19_late)) and pre V20_early))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
2
(not V19_late) and (OK != (true -> ((not (not V19_late)) and pre V20_early))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
3
pre V20_early and (OK != (true -> ((not V19_late) and pre (not V20_early)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
4
(not pre V20_early) and (OK != (true -> ((not V19_late) and pre (not V20_early)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
5
pre V19_late and (V19_late != (false -> (if pre (not V19_late) then (V63_diff < 0) else (V63_diff <= (- 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
6
(not pre V19_late) and (V19_late != (false -> (if pre (not V19_late) then (V63_diff < 0) else (V63_diff <= (- 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
7
(V63_diff < 0) and (V19_late != (false -> (if pre V19_late then (not (V63_diff < 0)) else (V63_diff <= (- 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
8
(not (V63_diff < 0)) and (V19_late != (false -> (if pre V19_late then (not (V63_diff < 0)) else (V63_diff <= (- 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
9
(V63_diff <= (- 10)) and (V19_late != (false -> (if pre V19_late then (V63_diff < 0) else (not (V63_diff <= (- 10)))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
10
(not (V63_diff <= (- 10))) and (V19_late != (false -> (if pre V19_late then (V63_diff < 0) else (not (V63_diff <= (- 10)))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
11
pre V20_early and (V20_early != (false -> (if pre (not V20_early) then (V63_diff > 0) else (V63_diff >= 10)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
12
(not pre V20_early) and (V20_early != (false -> (if pre (not V20_early) then (V63_diff > 0) else (V63_diff >= 10)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
13
(V63_diff > 0) and (V20_early != (false -> (if pre V20_early then (not (V63_diff > 0)) else (V63_diff >= 10)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
14
(not (V63_diff > 0)) and (V20_early != (false -> (if pre V20_early then (not (V63_diff > 0)) else (V63_diff >= 10)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
15
(V63_diff >= 10) and (V20_early != (false -> (if pre V20_early then (V63_diff > 0) else (not (V63_diff >= 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
16
(not (V63_diff >= 10)) and (V20_early != (false -> (if pre V20_early then (V63_diff > 0) else (not (V63_diff >= 10))))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
17
beacon and ((beacon or second) != ((not beacon) or second)) and (beacon or not beacon) and (second or not second) and (OK or not OK)
18
(not beacon) and ((beacon or second) != ((not beacon) or second)) and (beacon or not beacon) and (second or not second) and (OK or not OK)
19
second and ((beacon or second) != (beacon or (not second))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
20
(not second) and ((beacon or second) != (beacon or (not second))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
21
beacon and ((beacon and (not second)) != ((not beacon) and (not second))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
22
(not beacon) and ((beacon and (not second)) != ((not beacon) and (not second))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
23
second and ((beacon and (not second)) != (beacon and (not (not second)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
24
(not second) and ((beacon and (not second)) != (beacon and (not (not second)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
25
second and ((second and (not beacon)) != ((not second) and (not beacon))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
26
(not second) and ((second and (not beacon)) != ((not second) and (not beacon))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
27
beacon and ((second and (not beacon)) != (second and (not (not beacon)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
28
(not beacon) and ((second and (not beacon)) != (second and (not (not beacon)))) and (beacon or not beacon) and (second or not second) and (OK or not OK)
bench/distrib/misc/ex8/conds/ex8.ec
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/ex8.lus
1
node COUNTER(init,incr:int;X,reset:bool) returns (C:int);
2
var PC: int;
3
let
4
  PC = init -> pre C;
5
  C = if reset then init
6
      else if X then (PC+incr)
7
      else PC;
8
tel
9

  
10
node speed(beacon,second:bool) returns (late,early:bool);
11
var
12
  diff,incr:int;
13
let
14
  incr = if (beacon and not second) then 1
15
         else if (second and not beacon) then 2
16
         else 0;
17
  diff = COUNTER(0,incr,(beacon or second),false);
18
  early = false -> if pre early then (diff > 0)
19
                   else (diff >= 10);
20
  late = false -> if pre late then (diff < 0)
21
                  else (diff <= -10);
22
tel
23

  
24
--@ ensures OK;
25
node top(beacon,second:bool) returns (OK:bool);
26
var late,early: bool;
27
let
28
  (late,early) = speed(beacon,second);
29

  
30
  OK = true -> not late and pre early;
31

  
32
  --cannot go directly from early to late (valid)
33

  
34
  -- always was early and is not late; incorrect
35
  --%PROPERTY OK=true;
36

  
37
tel
bench/distrib/misc/ex8/ex8.lus_top_flatten.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n1.lus
1
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 < 10) else (V63_diff 
17
  <= -10)));
18
  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n10.lus
1
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 >= 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n11.lus
1
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 <= 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n12.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n13.lus
1
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 < 2) else (V63_diff <= 
17
  -10)));
18
  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n14.lus
1
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 < 1) else (V63_diff <= 
17
  -10)));
18
  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n15.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n16.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n17.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n18.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 1 else (if (beacon or 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 = (1 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n19.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if (not false) then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n2.lus
1
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 > 0) 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n20.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (not (beacon and (not second))) then 1 else (if (second and 
23
  (not beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n21.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not (not second))) then 1 else (if (second and 
23
  (not beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n22.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n23.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not (not second))) then 1 else (if (second and 
23
  (not beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n24.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not second)) then 1 else (if (not (second and 
23
  (not beacon))) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n25.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not second)) then 1 else (if ((not second) and 
23
  (not beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n26.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n27.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (not (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n28.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if ((not beacon) or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n29.lus
1
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 = (not (false -> (if (pre V20_early) then (V63_diff > 0) else (
19
  V63_diff >= 10))));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n3.lus
1
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 > 0) else (V63_diff 
19
  = 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n30.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
  (not beacon))) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n31.lus
1
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 -> (not (if (pre V20_early) then (V63_diff > 0) else (
19
  V63_diff >= 10))));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n32.lus
1
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 (not (pre V20_early)) then (V63_diff > 0) else (
19
  V63_diff >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n33.lus
1
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 (not V20_early)) then (V63_diff > 0) else (
19
  V63_diff >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n34.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n35.lus
1
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 < 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n36.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n37.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n38.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n39.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon xor (not second)) then 1 else (if (second and (not 
23
  beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n4.lus
1
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 > 0) else (V63_diff 
19
  <> 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n40.lus
1
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 (not (V63_diff > 0)) else (
19
  V63_diff >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n41.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not second)) then 1 else (if (second => (not 
23
  beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n42.lus
1
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
  V62_diff: int;
11
  V63_incr: int;
12
  V64_PC: int;
13

  
14
let
15
  OK = (true -> ((not V19_late) and (pre V20_early)));
16
  V19_late = (false -> (if (pre V19_late) then (V62_diff < 0) else (V62_diff <= 
17
  -10)));
18
  V20_early = (false -> (if (pre V20_early) then (V62_diff > 0) else (V62_diff 
19
  >= 1)));
20
  V62_diff = (if false then 0 else (if (beacon or second) then (V64_PC + 
21
  V63_incr) else V64_PC));
22
  V63_incr = (if (beacon and (not second)) then 1 else (if (second and (not 
23
  beacon)) then 2 else 0));
24
  V64_PC = (0 -> (pre V62_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n43.lus
1
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 > 0) else (not (
19
  V63_diff >= 10))));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n44.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or second) then (V65_PC + 
21
  V64_incr) else V65_PC));
22
  V64_incr = (if (beacon and (not second)) then 1 else (if (second xor (not 
23
  beacon)) then 2 else 0));
24
  V65_PC = (0 -> (pre V63_diff));
25
tel
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n45.lus
1
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 (not V19_late)) then (V63_diff < 0) else (
17
  V63_diff <= -10)));
18
  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n46.lus
1
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 (not (
17
  V63_diff <= -10))));
18
  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n47.lus
1
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 > 0) else (V63_diff 
19
  >= 10)));
20
  V63_diff = (if false then 0 else (if (beacon or 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
26

  
bench/distrib/misc/ex8/mutants/ex8.mutant.n48.lus
1
node top
2
  (beacon: bool;
3
  second: bool)
4
returns
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff