diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-02 16:24:12 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-02 16:24:12 +0200 |
commit | bc679afc4ac59c256a1b5f200078e495c188d066 (patch) | |
tree | e428dd704832e52322367d644db41b7cb37c8d29 | |
parent | 08096254ecf8c2341320e255ad74a7d99fb46d47 (diff) | |
download | scade-analyzer-bc679afc4ac59c256a1b5f200078e495c188d066.tar.gz scade-analyzer-bc679afc4ac59c256a1b5f200078e495c188d066.zip |
Fix non-termination issue in EDDs
-rw-r--r-- | abstract/abs_interp.ml | 18 | ||||
-rw-r--r-- | abstract/abs_interp_edd.ml | 147 | ||||
-rw-r--r-- | tests/source/updown2.scade | 40 |
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 |