diff options
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 65255ca..5beffda 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -587,12 +587,26 @@ end = struct List.length (List.filter (fun (qo, c, a) -> not a && c = ci) out_tc) in - a * b + (if a + b > 0 then 1 else 0)) + a + b + a * b) cases in let a = List.fold_left max 0 cs_sc in - let b = 5 * a in - if a > 0 && b = 0 then 1 else b + let b = if a = 0 then 0 else + List.length @@ List.filter + (fun qi -> + let qos = List.flatten @@ List.map + (fun (cid, c) -> + if List.exists (fun (qi0, c0, a) -> a && qi0 = qi && c0 = cid) in_tc + then + List.map (fun (qo, _, _) -> qo) @@ + List.filter (fun (_, c1, a) -> a && cid = c1) out_tc + else []) + cases + in + List.exists (fun qo -> not (List.mem qo qos)) loc.out_t) + loc.in_t + in + 5 * a + 17 * b in if fa <> 0 then begin (* calculate which states become inaccessible *) @@ -627,7 +641,7 @@ end = struct in (* calculate in/out count, weighted by changing guarantees *) let fc = - 0 * (2 * List.length loc.out_t + List.length loc.in_t) + 1 * (2 * List.length loc.out_t + List.length loc.in_t) in (* calculate number of VOI (variables of interest) that are affected *) let fd = |