Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / bench / distrib / misc / durationThm_1_e7_217_e7_31 / mutants / durationThm_1_e7_217_e7_31.mutant.n22.lus @ 43a2cae9

History | View | Annotate | Download (751 Bytes)

1
node top
2
  (ik: int;
3
  im: int;
4
  p: bool;
5
  q: bool;
6
  r: bool)
7
returns
8
  (OK: bool);
9

    
10
var
11
  V14_k: int;
12
  V15_m: int;
13
  V16_env: bool;
14
  V45_age_of_p: int;
15
  V52_age_of_p: int;
16
  V55_X: bool;
17
  V68_age_of_p: int;
18

    
19
let
20
  OK = (V16_env => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => r)));
21
  V14_k = (ik -> (pre V14_k));
22
  V15_m = (im -> (pre V15_m));
23
  V16_env = (V55_X -> (V55_X or (pre V16_env)));
24
  V45_age_of_p = (0 -> (if (pre p) then ((pre V45_age_of_p) + 1) else 0));
25
  V52_age_of_p = (0 -> (if (pre q) then ((pre V52_age_of_p) + 1) else 0));
26
  V55_X = ((((V14_k >= 1) or (V15_m > 1)) and ((V45_age_of_p >= V14_k) => q)) 
27
  and ((V52_age_of_p >= V15_m) => r));
28
  V68_age_of_p = (0 -> (if (pre p) then ((pre V68_age_of_p) + 1) else 0));
29
tel
30