Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / bench / distrib / misc / durationThm_1_e3_389_e4_294 / mutants / durationThm_1_e3_389_e4_294.mutant.n98.lus @ 43a2cae9

History | View | Annotate | Download (799 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 and (pre V16_env)));
24
  V45_age_of_p = (0 -> (if (pre (pre p)) then (((pre V45_age_of_p) + 1) - 1) 
25
  else 0));
26
  V52_age_of_p = (0 -> (if (pre (pre q)) then (((pre V52_age_of_p) + 1) - 1) 
27
  else 0));
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 (pre p)) then (((pre V68_age_of_p) + 1) - 1) 
31
  else 0));
32
tel
33