Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / bench / distrib / misc / durationThm_1_e7_217_e1_89 / mutants / durationThm_1_e7_217_e1_89.mutant.n31.lus @ 43a2cae9

History | View | Annotate | Download (780 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) + 1) else 1))
25
  ;
26
  V52_age_of_p = (0 -> (if (pre q) then (((pre V52_age_of_p) + 1) + 1) else 1))
27
  ;
28
  V55_X = ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) 
29
  and ((V52_age_of_p >= V15_m) => r));
30
  V68_age_of_p = (0 -> (if (pre p) then (((pre V68_age_of_p) + 1) + 1) else 1))
31
  ;
32
tel
33