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.n77.lus @ 43a2cae9

History | View | Annotate | Download (781 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
  V46_age_of_p: int;
15
  V53_age_of_p: int;
16
  V56_X: bool;
17
  V69_age_of_p: int;
18

    
19
let
20
  OK = (V16_env => (true -> ((V69_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 = (V56_X -> (V56_X and (pre V16_env)));
24
  V46_age_of_p = (0 -> (if (pre p) then (((pre V46_age_of_p) + 1) - 1) else 0))
25
  ;
26
  V53_age_of_p = (0 -> (if (pre q) then (((pre V53_age_of_p) + 1) - 1) else 0))
27
  ;
28
  V56_X = ((((V14_k >= 1) and (V15_m >= 2)) and ((V46_age_of_p >= V14_k) => q)) 
29
  and ((V53_age_of_p >= V15_m) => r));
30
  V69_age_of_p = (0 -> (if (pre p) then (((pre V69_age_of_p) + 1) - 1) else 0))
31
  ;
32
tel
33