summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-30 10:37:28 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-30 10:37:28 +0200
commit8bba764aaade1839b62be7c4f24292f8dc85ada8 (patch)
tree1aa5a4b52548de0537f7c621e488d52b63f6af1a
parent818c737eb01abe1a47894c1fbfc35c3a3af804ef (diff)
downloadscade-analyzer-8bba764aaade1839b62be7c4f24292f8dc85ada8.tar.gz
scade-analyzer-8bba764aaade1839b62be7c4f24292f8dc85ada8.zip
Implement selection of disjunction variables for EDDs.
Next (?) : leaves can store information on evars.
-rw-r--r--abstract/abs_interp_dynpart.ml2
-rw-r--r--abstract/abs_interp_edd.ml58
-rw-r--r--abstract/varenv.ml11
-rw-r--r--main.ml25
4 files changed, 66 insertions, 30 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 2ff950a..bbd8d19 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -221,7 +221,7 @@ end = struct
guarantees;
Format.printf "@.";
- let ve = mk_varenv rp f (conslist_of_f f) in
+ let ve = mk_varenv rp opt.disjunct f (conslist_of_f f) in
let env = {
rp; opt; ve; f; guarantees;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 722dc1a..cdf3c7e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -259,30 +259,37 @@ end = struct
*)
let edd_of_cons ve (op, vid, r) =
let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-
- let leaves = Hashtbl.create 1 in
-
- let root = match r with
- | EItem x ->
- DChoice(0, vid,
- List.map (fun v -> if op v x then v, DTop else v, DBot)
- (List.assoc vid ve.evars))
- | EIdent vid2 ->
- let a, b =
- if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
- then vid, vid2
- else vid2, vid
- in
- let nc = ref 0 in
- let nb x =
- incr nc;
- DChoice(!nc, b,
- List.map (fun v -> if op v x then v, DTop else v, DBot)
- (List.assoc b ve.evars))
+ if not (List.mem vid ve.d_vars)
+ then edd_top ve
+ else
+ let leaves = Hashtbl.create 1 in
+ let root = match r with
+ | EItem x ->
+ DChoice(0, vid,
+ List.map (fun v -> if op v x then v, DTop else v, DBot)
+ (List.assoc vid ve.evars))
+ | EIdent vid2 ->
+ if not (List.mem vid2 ve.d_vars)
+ then DTop
+ else
+ let a, b =
+ if Hashtbl.find ve.ev_order vid
+ < Hashtbl.find ve.ev_order vid2
+ then vid, vid2
+ else vid2, vid
+ in
+ let nc = ref 0 in
+ let nb x =
+ incr nc;
+ DChoice(!nc, b,
+ List.map (fun v -> if op v x then v, DTop else v, DBot)
+ (List.assoc b ve.evars))
+ in
+ DChoice(0, a, List.map
+ (fun x -> x, nb x)
+ (List.assoc a ve.evars))
in
- DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
- in
- { ve; root; leaves }
+ { ve; root; leaves }
(*
edd_join : edd_v -> edd_v -> edd_v
@@ -570,7 +577,8 @@ end = struct
all_vars = [];
cycle = [];
forget = [];
- forget_inv = []; } in
+ forget_inv = [];
+ d_vars = ["x"; "y"; "z"] } in
Hashtbl.add ve.ev_order "x" 0;
Hashtbl.add ve.ev_order "y" 1;
Hashtbl.add ve.ev_order "z" 2;
@@ -856,7 +864,7 @@ end = struct
guarantees;
Format.printf "@.";
- let ve = mk_varenv rp f cl in
+ let ve = mk_varenv rp opt.disjunct f cl in
{ rp; opt; ve; init_cl; cl; guarantees; }
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index cf29edf..bcfa77a 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -17,6 +17,7 @@ type varenv = {
last_vars : (bool * id * typ) list;
all_vars : (bool * id * typ) list;
+ d_vars : id list;
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
@@ -228,7 +229,7 @@ let force_ordering vars groups =
- cycle, forget
*)
-let mk_varenv (rp : rooted_prog) f cl =
+let mk_varenv (rp : rooted_prog) disj_fun f cl =
(* add variables from LASTs *)
let last_vars = uniq_sorted
(List.sort compare (extract_last_vars f)) in
@@ -311,6 +312,12 @@ let mk_varenv (rp : rooted_prog) f cl =
not (List.exists (fun (_, b, _) -> b = id) cycle))
all_vars) in
- { evars = enum_vars; nvars = num_vars; ev_order;
+ (* use specified disjunction variables *)
+ let d_vars = List.filter disj_fun
+ (List.map (fun (id, _) -> id) enum_vars) in
+ Format.printf "Disjunction variables: @[<hov>[%a]@]@."
+ (print_list Formula_printer.print_id ", ") d_vars;
+
+ { evars = enum_vars; nvars = num_vars; ev_order; d_vars;
last_vars; all_vars; cycle; forget; forget_inv }
diff --git a/main.ml b/main.ml
index c283328..f130b6c 100644
--- a/main.ml
+++ b/main.ml
@@ -54,7 +54,7 @@ let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
let ai_init_scopes = ref "all"
-let ai_disj_v = ref ""
+let ai_disj_v = ref "all"
let ai_max_dp_depth = ref 10
let ai_max_dp_width = ref 100
let ai_vci = ref false
@@ -187,6 +187,27 @@ let () =
|| !ai_edd_itv_dp || !ai_edd_rel_dp then
begin
let comma_split = Str.split (Str.regexp ",") in
+ let match_s s pat =
+ let n, m = String.length s, String.length pat in
+ let memo = Array.make_matrix (n+1) (m+1) None in
+ let rec aux i j =
+ match memo.(i).(j) with
+ | Some x -> x
+ | None ->
+ let x =
+ if i = n && j = m
+ then true
+ else if j = m && i < n
+ then false
+ else if i = n && j < m
+ then pat.[j] = '*' && aux i (j+1)
+ else
+ if pat.[j] = '*'
+ then aux (i+1) j || aux i (j+1)
+ else s.[i] = pat.[j] && aux (i+1) (j+1)
+ in memo.(i).(j) <- Some x; x
+ in aux 0 0
+ in
let select_f x =
if x = "all" then
(fun _ -> true)
@@ -195,7 +216,7 @@ let () =
else if String.length x > 5 && String.sub x 0 5 = "last+" then
let psl = comma_split
(String.sub x 5 (String.length x - 5)) in
- (fun i -> i.[0] = 'L' || List.mem i psl)
+ (fun i -> i.[0] = 'L' || List.exists (match_s i) psl)
else
(fun i -> List.mem i (comma_split x))
in