summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abstract/abs_interp.ml18
-rw-r--r--abstract/abs_interp_edd.ml147
-rw-r--r--tests/source/updown2.scade40
3 files changed, 130 insertions, 75 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3b2d79..0db128f 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -174,9 +174,7 @@ end = struct
num_vars : (id * bool) list;
(* program expressions *)
- f : bool_expr;
cl : conslist;
- f_g : bool_expr;
cl_g : conslist;
guarantees : (id * bool_expr) list;
@@ -237,14 +235,12 @@ end = struct
(print_list Ast_printer.print_typed_var ", ")
rp.all_vars;
- let enum_vars = List.fold_left
- (fun v (_, id, t) -> match t with
- | TEnum ch -> (id, ch)::v | _ -> v)
- [] rp.all_vars in
- let num_vars = List.fold_left
- (fun v (_, id, t) -> match t with
- | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v)
- [] rp.all_vars in
+ let num_vars, enum_vars = List.fold_left
+ (fun (nv, ev) (_, id, t) -> match t with
+ | TEnum ch -> nv, (id, ch)::ev
+ | TInt -> (id, false)::nv, ev
+ | TReal -> (id, true)::nv, ev)
+ ([], []) rp.all_vars in
let init_f = Transform.init_f_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
@@ -317,7 +313,7 @@ end = struct
let st =
{ rp; opt; enum_vars; num_vars;
- f; cl; f_g; cl_g; guarantees;
+ cl; cl_g; guarantees;
cycle; forget; d_vars; top;
env; delta; widen } in
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6e45240..cdcdab2 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -125,6 +125,11 @@ end = struct
let leaves, get_leaf = get_leaf_fun_st () in
leaves, get_leaf (false, 0)
+ let rank ve = function
+ | DChoice(_, x, _) -> Hashtbl.find ve.ev_order x
+ | _ -> 10000000 (* HYPOTHESIS : program will never have more than
+ that number of variables *)
+
(*
edd_print : Format.formatter -> edd_v -> unit
*)
@@ -288,22 +293,14 @@ end = struct
la lb
in
dq va kl
- | DChoice(_, va, la), DChoice(_, vb, lb) ->
- let v, kl =
- if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f_rec ca nb) la
- else
- vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
- in
- dq v kl
| DTop, _ | _, DTop -> DTop
| DBot, DBot -> DBot
- | DChoice(_,va, la), _ ->
+ | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
- | _, DChoice(_, vb, lb) ->
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
@@ -314,6 +311,8 @@ end = struct
get_leaf (Hashtbl.find a.leaves u)
| DBot, DVal(v, _) ->
get_leaf (Hashtbl.find b.leaves v)
+
+ | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
in
{ leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
@@ -331,22 +330,14 @@ end = struct
la lb
in
dq va kl
- | DChoice(_, va, la), DChoice(_, vb, lb) ->
- let v, kl =
- if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f_rec ca nb) la
- else
- vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
- in
- dq v kl
| DBot, _ | _, DBot -> DBot
| DTop, DTop -> DTop
- | DChoice(_, va, la), _ ->
+ | DChoice(_, va, la), _ when rank ve na < rank ve nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
- | _, DChoice(_, vb, lb) ->
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
@@ -357,6 +348,8 @@ end = struct
get_leaf (Hashtbl.find a.leaves u)
| DTop, DVal(v, _) ->
get_leaf (Hashtbl.find b.leaves v)
+
+ | _ -> assert false (* see above *)
in
{ leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
@@ -456,6 +449,33 @@ end = struct
(*
+ edd_subset : edd_v -> edd_v -> bool
+ *)
+ let edd_subset a b =
+ let rank = rank a.ve in
+ let f f_rec na nb =
+ match na, nb with
+ | DBot, _ -> true
+ | _, DTop -> true
+ | DTop, DBot -> false
+
+ | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i)
+ | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i)
+
+ | DVal(i, _), DVal(j, _) ->
+ ND.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+ la lb
+ | DChoice(_, va, la), _ when rank na < rank nb ->
+ List.for_all (fun (c, n) -> f_rec n nb) la
+ | _, DChoice(_, vb, lb) when rank na > rank nb ->
+ List.for_all (fun (c, n) -> f_rec na n) lb
+ | _ -> assert false
+ in memo2 f a.root b.root
+
+ (*
edd_forget_vars : edd_v -> id list -> edd_v
*)
let edd_forget_vars v vars =
@@ -566,9 +586,7 @@ end = struct
ve : varenv;
(* program expressions *)
- f : bool_expr;
cl : conslist;
- f_g : bool_expr;
cl_g : conslist;
guarantees : (id * bool_expr) list;
@@ -604,7 +622,7 @@ end = struct
(*
edd_join_widen : edd_v -> edd_v -> edd_v
*)
- let edd_join_widen (a:edd_v) (b:edd_v) =
+ let edd_widen (a:edd_v) (b:edd_v) =
let ve = a.ve in
let leaves, get_leaf = get_leaf_fun () in
let dq = new_node_fun () in
@@ -621,14 +639,6 @@ end = struct
la lb
in
dq va kl
- | DChoice(_, va, la), DChoice(_, vb, lb) ->
- let v, kl =
- if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f_rec ca nb) la
- else
- vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
- in
- dq v kl
| DBot, DVal (i, _) ->
get_leaf (Hashtbl.find b.leaves i)
@@ -643,21 +653,23 @@ end = struct
(Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
- | DChoice(_,va, la), _ ->
+ | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
- | _, DChoice(_, vb, lb) ->
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
+
+ | _ -> assert false
in
{ leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
(*
- edd_join_star : edd_v -> edd_v -> edd_v
+ edd_accumulate : edd_v -> edd_v -> edd_v
- Star in A all things that are in B and not in A.
+ Sometimes do global widening.
*)
- let edd_join_star_widen env (a:edd_v) (b:edd_v) =
+ let edd_accumulate env (a:edd_v) (b:edd_v) =
let ve = a.ve in
let leaves, get_leaf = get_leaf_fun_st () in
let dq = new_node_fun () in
@@ -674,14 +686,6 @@ end = struct
la lb
in
dq va kl
- | DChoice(_, va, la), DChoice(_, vb, lb) ->
- let v, kl =
- if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f_rec ca nb) la
- else
- vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
- in
- dq v kl
| DBot, DVal (i, _) ->
get_leaf (true, 0) (Hashtbl.find b.leaves i)
@@ -690,23 +694,39 @@ end = struct
| DVal (u, (s1, i1)), DVal (v, _) ->
let p1, p2 = edd_extract_path a u, edd_extract_path b v in
let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in
- let star =
- s1 || not (edd_eq p1 p2) || not (ND.subset d2 d1)
- in
let widen = edd_eq p1 p2 && i1 >= env.opt.widen_delay in
let x = (if widen then ND.widen else ND.join) d1 d2 in
- get_leaf (star, i1 + 1) x
+ get_leaf (s1, i1 + 1) x
- | DChoice(_,va, la), _ ->
+ | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
- | _, DChoice(_, vb, lb) ->
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
+
+ | _ -> assert false
in
{ leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
(*
+ edd_star_new : edd_v -> edd_v -> edd_v
+
+ Star in s leaves that were not present in s0
+ *)
+ let edd_star_new s0 s =
+ let f f_rec = function
+ | DChoice(n, x, l) ->
+ DChoice(n, x, List.map (fun (c, x) -> c, f_rec x) l)
+ | DVal(i, (false, n)) when
+ not (edd_subset (edd_meet (edd_extract_path s i) s) s0)
+ ->
+ DVal(i, (true, n))
+ | x -> x
+ in
+ { s with root = memo f s.root }
+
+ (*
pass_cycle : env -> edd_v -> edd_v
unpass_cycle : env -> edd_v -> edd_v
*)
@@ -842,14 +862,12 @@ end = struct
(print_list Ast_printer.print_typed_var ", ")
rp.all_vars;
- let enum_vars = List.fold_left
- (fun v (_, id, t) -> match t with
- | TEnum ch -> (id, ch)::v | _ -> v)
- [] rp.all_vars in
- let num_vars = List.fold_left
- (fun v (_, id, t) -> match t with
- | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v)
- [] rp.all_vars in
+ let num_vars, enum_vars = List.fold_left
+ (fun (nv, ev) (_, id, t) -> match t with
+ | TEnum ch -> nv, (id, ch)::ev
+ | TInt -> (id, false)::nv, ev
+ | TReal -> (id, true)::nv, ev)
+ ([], []) rp.all_vars in
let init_f = Transform.init_f_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
@@ -868,6 +886,7 @@ end = struct
let cl = Formula.conslist_of_f f in
let cl_g = Formula.conslist_of_f f_g in
+ Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
(* calculate order for enumerated variables *)
let evars = List.map fst enum_vars in
@@ -909,7 +928,7 @@ end = struct
Format.printf "Init: @[<hov>%a@]@." edd_print data;
{ rp; opt; ve;
- f; cl; f_g; cl_g; guarantees;
+ cl; cl_g; guarantees;
cycle; forget; data }
@@ -927,7 +946,7 @@ end = struct
let d2 = edd_apply_cl x e.cl in
let dc = pass_cycle e d2 in
- let y = edd_join_star_widen e x dc in
+ let y = edd_star_new x (edd_accumulate e x dc) in
if e.opt.vverbose_ci then
Format.printf "d2 %a@. dc %a@. y %a@."
@@ -965,7 +984,7 @@ end = struct
if n < e.opt.widen_delay then
edd_join i fi
else
- edd_join_widen i fi
+ edd_widen i fi
in
if edd_eq i j then j else iter (n+1) j
in
@@ -973,8 +992,8 @@ end = struct
let z = fix edd_eq f y in
- let j = pass_cycle e (edd_apply_cl z e.cl) in
- let r = edd_join_star_widen e x j in
+ let fj = pass_cycle e (edd_apply_cl z e.cl) in
+ let r = edd_star_new x (edd_accumulate e x fj) in
if e.opt.verbose_ci then
Format.printf " -> %a@." edd_print r;
@@ -982,7 +1001,7 @@ end = struct
ch_it (n+1) r
in
- let init_acc = edd_join_star_widen e (edd_bot e.data.ve) e.data in
+ let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
(* Dump final state *)
let acc = ch_it 0 init_acc in
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
new file mode 100644
index 0000000..73d111a
--- /dev/null
+++ b/tests/source/updown2.scade
@@ -0,0 +1,40 @@
+const bound: int = 7;
+
+node updown() returns(probe x, probe y, probe z: int)
+var last_x, last_y: int;
+let
+ last_x = 0 -> pre x;
+ automaton
+ initial state UP
+ let x = last_x + 1; tel
+ until if x >= bound resume DOWN;
+
+ state DOWN
+ let x = last_x - 1; tel
+ until if x <= -bound resume UP;
+
+ returns x;
+ guarantee x_bounded: x >= -bound and x <= bound;
+
+ last_y = 0 -> pre y;
+ automaton
+ initial state DOWN
+ let y = last_y - 1; tel
+ until if y <= -bound resume UP;
+
+ state UP
+ let y = last_y + 1; tel
+ until if y >= bound resume DOWN;
+
+ returns y;
+ guarantee y_bounded: y >= -bound and y <= bound;
+
+ z = x + y;
+ guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+ exit = i >= 30;
+ a, b, c = updown2();
+tel
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 17:01:42 +0000