summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_dynpart.ml
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 09:09:12 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 09:09:12 +0200
commit7205927e18ea355a619e95b1036aac9b94a22667 (patch)
tree5398582cd50ceefd7680fcf55dbd3a225fee6cc1 /abstract/abs_interp_dynpart.ml
parent29e7daea2d613f1a3b375934446f7f9b6c489021 (diff)
downloadscade-analyzer-7205927e18ea355a619e95b1036aac9b94a22667.tar.gz
scade-analyzer-7205927e18ea355a619e95b1036aac9b94a22667.zip
Try (and fail) to make heuristic any good.
Diffstat (limited to 'abstract/abs_interp_dynpart.ml')
-rw-r--r--abstract/abs_interp_dynpart.ml22
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 =