summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-19 18:11:35 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-19 18:11:35 +0200
commit2514cd8a0767804a254addc9ac0ad8da2ce97dda (patch)
tree9df94006ffdc35a52badd78fbecadd032be4d331
parent3c3b96e877dcb121d17da282dc4ca0caadda72b2 (diff)
downloadscade-analyzer-2514cd8a0767804a254addc9ac0ad8da2ce97dda.tar.gz
scade-analyzer-2514cd8a0767804a254addc9ac0ad8da2ce97dda.zip
Actually, it works.
-rw-r--r--abstract/abs_domain.ml21
-rw-r--r--abstract/abs_interp.ml8
-rw-r--r--tests/source/half.scade2
3 files changed, 22 insertions, 9 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index a30713a..64eefc7 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -223,8 +223,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let var_itv x id =
if List.mem_assoc id x.nvars
- then IN (VMap.map (fun v -> ND.var_itv v id) x.value)
- else not_implemented "var_itv for enum variable"
+ then
+ let x = List.fold_left
+ (fun x (v, _) ->
+ if v.[0] = 'N' || (String.length v > 3 && String.sub v 0 3 = "pre")
+ then forgetvar x v else x)
+ x x.evars in
+ IN (VMap.map (fun v -> ND.var_itv v id) x.value)
+ else
+ let all = List.fold_left (fun a b -> SSet.add b a) SSet.empty
+ (List.assoc id x.evars) in
+ IE
+ (VMap.fold
+ (fun enum _ s ->
+ try SSet.add (VarMap.find id enum) s
+ with Not_found -> all)
+ x.value
+ SSet.empty)
let set_disjunct x id p =
{ x with
@@ -356,7 +371,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
{ x with value = VMap.empty }
let print_all fmt x =
- Format.fprintf fmt "@[<v 0>";
+ Format.fprintf fmt "@[<v>";
VMap.iter
(fun enum num ->
Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ "
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 7a53134..e55f199 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -127,14 +127,12 @@ end = struct
let do_prog widen_delay rp =
let st = init_state widen_delay rp in
- let final, final_c = loop st st.env in
+ let final_nc, final = loop st st.env in
Format.printf "@[<hov>F %a@]@.@."
- E.print_all final;
- (*
+ E.print_all final_nc;
Format.printf "@[<hov>F' %a@]@.@."
- E.print_all final_c;
- *)
+ E.print_all final;
let check_guarantee (id, f) =
let cl = Formula.conslist_of_f f in
diff --git a/tests/source/half.scade b/tests/source/half.scade
index da90586..541e81c 100644
--- a/tests/source/half.scade
+++ b/tests/source/half.scade
@@ -1,4 +1,4 @@
-node test(i: int) returns (a, b, probe c: int; exit: bool)
+node test(i: int) returns (probe a, probe b, probe c: int; exit: bool)
var
la, lb: int;
half: bool;