Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / bench / distrib / misc / durationThm_1_e7_217 / mutants / durationThm_1_e7_217.mutant.n53.lus @ 43a2cae9

History | View | Annotate | Download (805 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
  V60_Sofar: bool;
18
  V68_age_of_p: int;
19

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