diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 186 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 343 | ||||
| -rw-r--r-- | abstract/transform.ml | 229 |
3 files changed, 579 insertions, 179 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 3ff91a6..4f2ad81 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -11,8 +11,6 @@ module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig val do_prog : cmdline_opt -> rooted_prog -> unit - val test : unit -> unit - end = struct @@ -31,10 +29,11 @@ end = struct ev_order : (id, int) Hashtbl.t; } - type edd = + type edd_node = | DBot | DVal of int | DChoice of id * (item * edd) list + and edd = int * edd_node type edd_v = { ve : varenv; @@ -43,40 +42,66 @@ end = struct (* add here eventual annotations *) } + (* + Utility functions for memoization + + memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b) + memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c) + *) + let memo f = + let n = ref 0 in + let memo = Hashtbl.create 12 in + let rec ff (id, v) = + try Hashtbl.find memo id + with Not_found -> + let r = f ff v in + incr n; + Hashtbl.add memo id (n, r); + n, r + in ff + let memo2 f = + let n = ref 0 in + let memo = Hashtbl.create 12 in + let rec ff (id1, v1) (id2, v2) = + try Hashtbl.find memo (id1, id2) + with Not_found -> + let r = f ff v1 v2 in + incr n; + Hashtbl.add memo (id1, id2) (n, r); + n, r + in ff (* edd_print : Format.formatter -> edd_v -> unit *) let edd_print fmt v = - let ids = Hashtbl.create 12 in - let n = ref 0 in - let rec mkid = function - | DChoice(_, l) as x -> - if not (Hashtbl.mem ids x) then begin - incr n; Hashtbl.add ids x !n; - List.iter (fun (_, x) -> mkid x) l + let c_nodes = Hashtbl.create 12 in + let rec add = function + | n, (DChoice(_, l) as x) -> + if not (Hashtbl.mem c_nodes n) then begin + Hashtbl.add c_nodes n x; + List.iter (fun (_, y) -> add y) l end | _ -> () - in mkid v.root; + in add v.root; + let print_n fmt = function - | DBot -> Format.fprintf fmt "⊥"; - | DVal i -> Format.fprintf fmt "v%d" i; - | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x) + | (_, DBot) -> Format.fprintf fmt "⊥"; + | (_, DVal i) -> Format.fprintf fmt "v%d" i; + | (n, DChoice _) -> Format.fprintf fmt "n%d" n in Format.fprintf fmt "Root: %a@." print_n v.root; - for id = 1 to !n do - let c = ref None in - Hashtbl.iter (fun u i -> if i = id then c := Some u) ids; - let x = match !c with | Some x -> x | None -> assert false in - match x with + + Hashtbl.iter + (fun id x -> match x with | DChoice (var, l) -> let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@." id Formula_printer.print_id var (print_list p ", ") l - | _ -> assert false - done; + | _ -> assert false) + c_nodes; Hashtbl.iter (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v) v.leaves @@ -86,7 +111,7 @@ end = struct (* edd_bot : varenv -> edd_v *) - let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 } + let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 } (* edd_top : evar list -> nvar list -> edd_v @@ -94,7 +119,7 @@ end = struct let edd_top ve = let leaves = Hashtbl.create 1 in Hashtbl.add leaves 0 (ND.top ve.nvars); - { ve; root = DVal 0; leaves } + { ve; root = (1, DVal 0); leaves } (* edd_of_cons : varenv -> enum_cons -> edd_v @@ -105,23 +130,27 @@ end = struct let leaves = Hashtbl.create 1 in Hashtbl.add leaves 0 (ND.top ve.nvars); + let bot, top = (0, DBot), (1, DVal 0) in + let root = match r with | EItem x -> - DChoice(vid, - List.map (fun v -> if op v x then v, DVal 0 else v, DBot) - (List.assoc vid ve.evars)) + 2, DChoice(vid, + List.map (fun v -> if op v x then v, bot else v, top) + (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 n = ref 2 in let nb x = - DChoice(b, - List.map (fun v -> if op v x then v, DVal 0 else v, DBot) - (List.assoc b ve.evars)) + incr n; + !n, DChoice(b, + List.map (fun v -> if op v x then v, top else v, bot) + (List.assoc b ve.evars)) in - DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) + 2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) in { ve; root; leaves } @@ -131,10 +160,9 @@ end = struct let edd_join a b = let ve = a.ve in - let leaves = Hashtbl.copy a.leaves in - let n = ref 0 in - Hashtbl.iter (fun i _ -> if i > !n then n := i) leaves; + let leaves = Hashtbl.create 12 in + let n = ref 0 in let get_leaf x = let id = ref None in Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; @@ -147,61 +175,47 @@ end = struct end in - let memo_bcopy = Hashtbl.create 12 in - let rec bcopy nb = - try Hashtbl.find memo_bcopy nb - with Not_found -> let r = - match nb with - | DBot -> DBot - | DVal i -> get_leaf (Hashtbl.find b.leaves i) - | DChoice (v, x) -> - DChoice(v, List.map (fun (c, n) -> c, bcopy n) x) - in Hashtbl.add memo_bcopy nb r; r - in - let memo = Hashtbl.create 12 in - let rec f (na, nb) = - try Hashtbl.find memo (na, nb) - with Not_found -> let r = - let dq v l = - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> x <> x0) l - then DChoice(v, l) - else x0 + let f f_rec na nb = + let dq v l = + let _, (i, x0) = List.hd l in + if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l + then DChoice(v, l) + else x0 + in + match na, nb with + | DBot, DBot -> DBot + | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i) + | x, DBot -> x + + | DChoice(va, la), DChoice(vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f (ba, bb)) + la lb in - match na, nb with - | DBot, x -> bcopy x - | x, DBot -> x - - | DChoice(va, la), DChoice(vb, lb) when va = vb -> - let kl = List.map2 - (fun (ta, ba) (tb, bb) -> assert (ta = tb); - ta, f (ba, bb)) - 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 (ca, nb)) la - else - vb, List.map (fun (k, cb) -> k, f (na, cb)) lb - in - dq v kl - - | DChoice(va, la), _ -> - let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in - dq va kl - | _, DChoice(vb, lb) -> - let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in - dq vb kl - - | DVal u, DVal v -> - let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x - in Hashtbl.add memo (na, nb) r; r + 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 (ca, nb)) la + else + vb, List.map (fun (k, cb) -> k, f (na, cb)) lb + in + dq v kl + + | DChoice(va, la), _ -> + let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in + dq va kl + | _, DChoice(vb, lb) -> + let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in + dq vb kl + + | DVal u, DVal v -> + let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x in - { leaves; ve; root = f (a.root, b.root) } + { leaves; ve; root = memo2 f a.root b.root } (* edd_meet : edd_v -> edd_v -> edd_v @@ -342,6 +356,7 @@ end = struct in f (a.root, b.root) + (* let test () = let ve = { evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]]; @@ -358,6 +373,7 @@ end = struct Format.printf "x = y && y != z : @[%a@]@." edd_print w; let t = edd_join u v in Format.printf "x = y || y != z : @[%a@]@." edd_print t + *) (* ****************************** diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index c8b4ec5..2353049 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -34,6 +34,9 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig end +(* + Simple domain : one valuation for each variable, or T +*) module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct type item = string @@ -142,3 +145,343 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct Format.fprintf fmt " }@]" end + + +(* + Less simple domain : a set of possible values for each variable, or T +*) + +module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct + type item = string + + type t = { + vars : (id * item list) list; + value : item list VarMap.t; + } + + let sort = List.sort Pervasives.compare + let uniq x = uniq_sorted (sort x) + + let top vars = { vars; value = VarMap.empty } + + let vars x = x.vars + + let forgetvar x id = + { x with value = VarMap.remove id x.value } + let project x id = + try VarMap.find id x.value + with Not_found -> List.assoc id x.vars + + let join x1 x2 = + let v = VarMap.merge + (fun _ a b -> match a, b with + | Some a, Some b -> Some (uniq (a@b)) + | _ -> None) + x1.value x2.value in + { x1 with value = v } + let meet x1 x2 = + let v = VarMap.merge + (fun _ a b -> match a, b with + | Some a, None | None, Some a -> Some a + | Some a, Some b -> + begin match List.filter (fun x -> List.mem x b) a with + | [] -> raise Bot | l -> Some l end + | _ -> None) + x1.value x2.value in + { x1 with value = v } + + let subset a b = + VarMap.for_all + (fun id v -> + try let v2 = VarMap.find id b.value in + List.for_all (fun x -> List.mem x v2) v + with Not_found -> true) + a.value + let eq a b = subset a b && subset b a + + let apply_cons x (op, id, e) = + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in + + match e with + | EItem s -> + let pv = project x id in + begin match List.filter (op s) pv with + | [] -> [] + | vals -> [{ x with value = VarMap.add id vals x.value }] + end + | EIdent id2 -> + let v1 = project x id in + let v2 = project x id2 in + List.fold_left + (fun l v1 -> + let v2 = List.filter (op v1) v2 in + let x = { x with value = VarMap.add id [v1] x.value } in + match v2 with + | [] -> l + | _ -> { x with value = VarMap.add id2 v2 x.value }::l) + [] v1 + + let assign x idl = + let v = List.fold_left + (fun v (id, id2) -> + try VarMap.add id (VarMap.find id2 x.value) v + with Not_found -> VarMap.remove id v ) + x.value idl + in { x with value = v } + + + let print fmt x = + let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in + let s = List.sort Pervasives.compare b in + let rec bl = function + | [] -> [] + | (v, id)::q -> + let v = sort v in + if v <> sort (List.assoc id x.vars) then + match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + else + bl q + in + let sbl = bl s in + Format.fprintf fmt "@[<v 2>{ "; + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + Format.fprintf fmt "@[<hov 4>"; + List.iteri + (fun i id -> + if i > 0 then Format.fprintf fmt ",@ "; + Format.fprintf fmt "%a" Formula_printer.print_id id) + ids; + match v with + | [v0] -> Format.fprintf fmt " ≡ %s@]" v0 + | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l) + sbl; + Format.fprintf fmt " }@]" + +end + + +(* + Complicated domain : a set of values for each variables, plus some + constraints on couples of variables + (eg. (x, y) in [ tt, tt ; ff, ff ] +*) + +module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct + + module VarC = struct + type t = id * id + let compare = Pervasives.compare + end + module VarCMap = Mapext.Make(VarC) + + type item = string + + type t = { + vars : (id * item list) list; + value : item list VarMap.t; + + (* in ccond (x, y) -> l, must have x < y (textual order on identifiers) -> unicity *) + ccons : (item * item) list VarCMap.t; + } + + let sort = List.sort Pervasives.compare + let uniq x = uniq_sorted (sort x) + let list_inter x y = List.filter (fun k -> List.mem k y) x + + let all_couples l1 l2 = + List.flatten + (List.map (fun x -> List.map (fun y -> x, y) l2) l1) + + let top vars = { vars; value = VarMap.empty; ccons = VarCMap.empty } + + let vars x = x.vars + + let forgetvar x id = + (* TODO : try to find a substitution variable so that some contraints can be propagated. + this is important so that cycle passing can be done correctly ! *) + { x with + value = VarMap.remove id x.value; + ccons = VarCMap.filter (fun (a, b) _ -> a <> id && b <> id) x.ccons } + + let project x id = + try VarMap.find id x.value + with Not_found -> List.assoc id x.vars + + let project2 x id1 id2 = + try + let id1', id2' = ord_couple (id1, id2) in + if id1' = id1 then + VarCMap.find (id1, id2) x.ccons + else + List.map (fun (a, b) -> b, a) (VarCMap.find (id1', id2') x.ccons) + with _ -> + let v1, v2 = project x id1, project x id2 in + all_couples v1 v2 + + let strict x = + let rec f x = + (* + - if (x, y) in [ a, b1 ; a, b2 ; ... ; a, bn ], + replace this by x = a and y in { b1, ..., bn } + - filter (x, y) in [ ... ] with x in specified itv, y in specified itv + *) + let usefull, vv, cc = + VarCMap.fold + (fun (x, y) l (usefull, vv, cc) -> + let p1, p2 = uniq (List.map fst l), uniq (List.map snd l) in + let p1 = try list_inter p1 (VarMap.find x vv) with _ -> p1 in + let p2 = try list_inter p2 (VarMap.find y vv) with _ -> p2 in + + if p1 = [] || p2 = [] then raise Bot; + let vv = VarMap.add x p1 (VarMap.add y p2 vv) in + + if List.length p1 = 1 || List.length p2 = 1 + then + true, vv, cc + else + match List.filter (fun (u, v) -> List.mem u p1 && List.mem v p2) l with + | [] -> raise Bot + | l2 -> List.length l2 < List.length l, vv, VarCMap.add (x, y) l2 cc) + x.ccons (false, x.value, VarCMap.empty) in + + let x = { x with value = vv; ccons = cc } in + if usefull then f x else x + in + f x + + let join x1 x2 = + let v = VarMap.merge + (fun _ a b -> match a, b with + | Some a, Some b -> Some (uniq (a@b)) + | _ -> None) + x1.value x2.value in + let x = { x1 with value = v } in + + let cc = VarCMap.merge + (fun (id1, id2) l1 l2 -> + let v1, v2 = project x1 id1, project x id2 in + let ac = all_couples v1 v2 in + let c = List.filter + (fun q -> + (match l1 with Some l -> List.mem q l | _ -> true) || + (match l2 with Some l -> List.mem q l | _ -> true)) + ac in + if List.length c < List.length ac then Some c else None) + x1.ccons x2.ccons in + + strict { x with ccons = cc } + + let meet x1 x2 = + let v = VarMap.merge + (fun _ a b -> match a, b with + | Some a, None | None, Some a -> Some a + | Some a, Some b -> + begin match list_inter a b with + | [] -> raise Bot | l -> Some l end + | _ -> None) + x1.value x2.value in + let x = { x1 with value = v } in + + let cc = VarCMap.merge + (fun (id1, id2) l1 l2 -> + let v1, v2 = project x id1, project x id2 in + let ac = all_couples v1 v2 in + let c1 = match l1 with Some l -> list_inter l ac | None -> ac in + let c2 = match l2 with Some l -> list_inter l ac | None -> ac in + match list_inter c1 c2 with + | [] -> raise Bot + | l -> if List.length l < List.length ac then Some l else None) + x1.ccons x2.ccons in + + strict { x with ccons = cc } + + let subset a b = + VarMap.for_all + (fun id v -> + let vs = project a id in + List.for_all (fun c -> List.mem c vs) v) + b.value + && + VarCMap.for_all + (fun (id1, id2) l -> + let l2 = project2 a id1 id2 in + List.for_all (fun c -> List.mem c l) l2) + b.ccons + let eq a b = + subset a b && subset b a + + let apply_cons x (op, id, e) = + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in + + match e with + | EItem s -> + let pv = project x id in + begin match List.filter (op s) pv with + | [] -> [] + | vals -> try [strict { x with value = VarMap.add id vals x.value }] with Bot -> [] + end + | EIdent id2 -> + let id, id2 = ord_couple (id, id2) in + let c = project2 x id id2 in + let ok_c = List.filter (fun (a, b) -> op a b) c in + try + [match uniq (List.map fst ok_c), uniq (List.map snd ok_c) with + | [], _ | _, [] -> raise Bot + | [a], q -> strict { x with value = VarMap.add id [a] (VarMap.add id2 q x.value) } + | q, [b] -> strict { x with value = VarMap.add id q (VarMap.add id2 [b] x.value) } + | _ -> strict { x with ccons = VarCMap.add (id, id2) ok_c x.ccons} + ] + with Bot -> [] + + let assign x idl = + let x2 = List.fold_left (fun x (v, _) -> forgetvar x v) x idl in + let v = List.fold_left + (fun v (id, id2) -> + try VarMap.add id (VarMap.find id2 x.value) v + with Not_found -> v) + x2.value idl in + let c = VarCMap.fold + (fun (v1, v2) l c -> + let v1' = try List.assoc v1 idl with _ -> v1 in + let v2' = try List.assoc v2 idl with _ -> v2 in + VarCMap.add (v1', v2') l c) + x.ccons x2.ccons in + strict { x with value = v; ccons = c } + + + let print fmt x = + let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in + let s = List.sort Pervasives.compare b in + let rec bl = function + | [] -> [] + | (v, id)::q -> + let v = sort v in + if v <> sort (List.assoc id x.vars) then + match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + else + bl q + in + let sbl = bl s in + Format.fprintf fmt "@[<v 2>{ "; + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + Format.fprintf fmt "@[<hov 4>"; + List.iteri + (fun i id -> + if i > 0 then Format.fprintf fmt ",@ "; + Format.fprintf fmt "%a" Formula_printer.print_id id) + ids; + match v with + | [v0] -> Format.fprintf fmt " ≡ %s@]" v0 + | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l) + sbl; + Format.fprintf fmt " }@]" + +end diff --git a/abstract/transform.ml b/abstract/transform.ml index b9c173d..4a13e18 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -26,8 +26,8 @@ type ne_expr = (* f_of_neexpr : transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr *) -let rec f_of_neexpr td (node, prefix) where expr = - let sub = f_of_neexpr td (node, prefix) in +let rec f_of_neexpr td (node, prefix, clock_scope) where expr = + let sub = f_of_neexpr td (node, prefix, clock_scope) in let le = loc_error (snd expr) in match fst expr with (* ident *) @@ -71,24 +71,27 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - if td.rp.init_scope (node^"/") + if td.rp.init_scope clock_scope then f_or - (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) + (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) (sub where a)) - (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false)) + (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) (sub where b)) - else + else if not (td.rp.no_time_scope clock_scope) + then f_or - (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0)) (sub where a)) - (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1)) (sub where b)) + else + f_or (sub where a) (sub where b) (* other *) | AST_if(c, a, b) -> f_or - (f_and (f_of_expr td (node, prefix) c) (sub where a)) - (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b)) + (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a)) + (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b)) | AST_instance ((f, _), args, nid) -> let (n, _) = find_node_decl td.rp.p f in where @@ -107,8 +110,9 @@ let rec f_of_neexpr td (node, prefix) where expr = (* boolean values treated as enumerated types *) | _ when type_expr td.rp node expr = [bool_type] -> f_or - (f_and (f_of_expr td (node, prefix) expr) (where [EE (EItem bool_true)])) - (f_and (f_of_expr td (node, prefix) (AST_not(expr), snd expr)) + (f_and (f_of_expr td (node, prefix, clock_scope) expr) + (where [EE (EItem bool_true)])) + (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr)) (where [EE (EItem bool_false)])) | _ -> le type_error "Expected numerical/enumerated value" @@ -120,8 +124,8 @@ let rec f_of_neexpr td (node, prefix) where expr = f_of_bexpr : transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr *) -and f_of_bexpr td (node, prefix) where expr = - let sub = f_of_bexpr td (node, prefix) in +and f_of_bexpr td (node, prefix, clock_scope) where expr = + let sub = f_of_bexpr td (node, prefix, clock_scope) in match fst expr with | AST_bool_const b -> where (BConst b) | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b) @@ -129,7 +133,7 @@ and f_of_bexpr td (node, prefix) where expr = | AST_not(a) -> BNot(sub where a) | AST_binary_rel(rel, a, b) -> where - (f_of_neexpr td (node, prefix) + (f_of_neexpr td (node, prefix, clock_scope) (function | [NE x; NE y] -> BRel(rel, x, y) | [EE x; EE y] -> @@ -142,11 +146,22 @@ and f_of_bexpr td (node, prefix) where expr = (AST_tuple [a; b], snd expr)) (* Temporal *) | AST_arrow(a, b) -> + if td.rp.init_scope clock_scope + then f_or - (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) (sub where a)) - (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) (sub where b)) + else if not (td.rp.no_time_scope clock_scope) + then + f_or + (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1)) + (sub where b)) + else + f_or (sub where a) (sub where b) (* Enumerations... *) | _ when type_expr td.rp node expr = [bool_type] -> let ff = function @@ -156,23 +171,53 @@ and f_of_bexpr td (node, prefix) where expr = (f_and (f_e_eq x (EItem bool_false)) (where (BConst false))) | _ -> assert false in - f_of_neexpr td (node, prefix) ff expr + f_of_neexpr td (node, prefix, clock_scope) ff expr | _ -> type_error "Expected boolean value." -and f_of_expr td (node, prefix) expr = - f_of_bexpr td (node, prefix) (fun x -> x) expr +and f_of_expr td (node, prefix, clock_scope) expr = + f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr (* Translate program into one big formula *) -let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = + +let clock_scope_here (node, prefix, _) = + node^"/"^prefix + +let gen_clock td (node, prefix, _) active = + let clock_scope = node^"/"^prefix in + let clock_eq = + if active then + f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, NIdent("N"^clock_scope^"time"), + NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"))) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false) + else BConst true) + else + f_and + (if not (td.rp.no_time_scope clock_scope) + then BRel(AST_EQ, + NIdent("N"^clock_scope^"time"), + NIdent(clock_scope^"time")) + else BConst true) + (if td.rp.init_scope clock_scope + then f_e_eq (EIdent("N"^clock_scope^"init")) + (EIdent (clock_scope^"init")) + else BConst true) + in + clock_scope, clock_eq + +let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = let expr_eq e = let instance_eq (_, id, eqs, args) = - let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in + let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in if active then let arg_eq ((_,argname,_), expr) = - f_of_neexpr td (node, prefix) (function + f_of_neexpr td (node, prefix, clock_scope) (function | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v) | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v | _ -> invalid_arity "in argument") @@ -186,7 +231,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let pre_expr (id, expr) = let id = node^"/"^id in if active then - f_of_neexpr td (node, prefix) (fun elist -> + f_of_neexpr td (node, prefix, clock_scope) (fun elist -> list_fold_op f_and (List.mapi (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in @@ -222,7 +267,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in f_and_list rels in - f_of_neexpr td (node, prefix) apply_f e + f_of_neexpr td (node, prefix, clock_scope) apply_f e else BConst true in @@ -230,7 +275,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = | AST_assume (_, e) -> let assume_eq = if active then - f_of_expr td (node, prefix) e + f_of_expr td (node, prefix, clock_scope) e else BConst true in @@ -239,13 +284,13 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let gn = node^"/g_"^id in let guarantee_eq = if active && assume_guarantees then - f_and (f_of_expr td (node, prefix) e) + f_and (f_of_expr td (node, prefix, clock_scope) e) (BEnumCons(E_EQ, gn, EItem bool_true)) else f_or - (f_and (f_of_expr td (node, prefix) e) + (f_and (f_of_expr td (node, prefix, clock_scope) e) (BEnumCons(E_EQ, gn, EItem bool_true))) - (f_and (BNot (f_of_expr td (node, prefix) e)) + (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e)) (BEnumCons(E_EQ, gn, EItem bool_false))) in f_and (expr_eq e) guarantee_eq @@ -258,16 +303,20 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in let rec do_tree_act = function | AST_activate_body b -> - f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees + let b_scope = node, b.act_id^".", b.body in + let clock_scope, clock_eq = gen_clock td b_scope true in + f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees) | AST_activate_if(c, a, b) -> f_or - (f_and (f_of_expr td (node, prefix) c) + (f_and (f_of_expr td (node, prefix, clock_scope) c) (f_and (do_tree_act a) (do_tree_inact b))) - (f_and (BNot(f_of_expr td (node, prefix) c)) + (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (f_and (do_tree_act b) (do_tree_inact a))) and do_tree_inact = function | AST_activate_body b -> - f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees + let b_scope = node, b.act_id^".", b.body in + let clock_scope, clock_eq = gen_clock td b_scope false in + f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees) | AST_activate_if(_, a, b) -> f_and (do_tree_inact a) (do_tree_inact b) in @@ -276,24 +325,27 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let stv = node^"/"^aid^".state" in let nstv = "N"^node^"/"^aid^".state" in let st_eq_inact (st, _) = - f_and - (f_of_scope false td - (node, aid^"."^st.st_name^".", st.body) assume_guarantees) - (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until)) + let st_scope = node, aid^"."^st.st_name^".", st.body in + let clock_scope, clock_eq = gen_clock td st_scope false in + f_and clock_eq + (f_and + (f_of_scope false td st_scope clock_scope assume_guarantees) + (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until))) in if active then let st_eq_act (st, l) = let act_eq = - let st_eq = f_of_scope true td - (node, aid^"."^st.st_name^".", st.body) assume_guarantees in + let st_scope = node, aid^"."^st.st_name^".", st.body in + let clock_scope, clock_eq = gen_clock td st_scope true in + let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in let rec aux = function | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name) | (c, (target, l), rst)::q -> if rst then loc_error l error "Resetting transitions not supported."; f_or - (f_and (f_of_expr td (node, prefix) c) + (f_and (f_of_expr td (node, prefix, clock_scope) c) (BEnumCons(E_EQ, nstv, EItem target))) - (f_and (BNot (f_of_expr td (node, prefix) c)) (aux q)) + (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q)) in f_and st_eq (aux st.until) in f_or @@ -305,31 +357,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = else f_and_list (List.map st_eq_inact states) in - let time_incr_eq = - if active then - f_and - (if not (td.rp.no_time_scope (node^"/")) - then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) - else BConst true) - (if td.rp.init_scope (node^"/") - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) - else BConst true) - else - f_and - (if not (td.rp.no_time_scope (node^"/")) - then BRel(AST_EQ, - NIdent("N"^node^"/"^prefix^"time"), - NIdent(node^"/"^prefix^"time")) - else BConst true) - (if td.rp.init_scope (node^"/") - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) - (EIdent (node^"/"^prefix^"init")) - else BConst true) - in - List.fold_left f_and - time_incr_eq - (List.map do_eq eqs) + f_and_list (List.map do_eq eqs) and f_of_prog rp assume_guarantees = let td = { @@ -337,15 +365,34 @@ and f_of_prog rp assume_guarantees = consts = I.consts rp; } in - f_of_scope true td td.rp.root_scope assume_guarantees + let clock_scope, clock_eq = gen_clock td rp.root_scope true in + + f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees) (* Translate init state into a formula *) -let rec init_f_of_scope rp (node, prefix, eqs) = +let gen_clock_init rp (node, prefix, _) = + let clock_scope = node^"/"^prefix in + let time_eq = + f_and + (if not (rp.no_time_scope clock_scope) + then + BRel(AST_EQ, + NIdent(clock_scope^"time"), + NIntConst 0) + else BConst true) + (if rp.init_scope clock_scope + then + f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true) + else BConst true) + in + clock_scope, time_eq + +let rec init_f_of_scope rp (node, prefix, eqs) clock_scope = let expr_eq e = let instance_eq (_, id, eqs, args) = - init_f_of_scope rp (node^"/"^id, "", eqs) + init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope in List.fold_left (fun x i -> f_and (instance_eq i) x) (BConst true) (extract_instances rp.p e) @@ -356,7 +403,9 @@ let rec init_f_of_scope rp (node, prefix, eqs) = | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> - init_f_of_scope rp (node, b.act_id^".", b.body) + let bscope = (node, b.act_id^".", b.body) in + let clock_scope, clock_eq = gen_clock_init rp bscope in + f_and clock_eq (init_f_of_scope rp bscope clock_scope) | AST_activate_if(c, a, b) -> f_and (expr_eq c) (f_and (cond_eq a) (cond_eq b)) @@ -367,37 +416,27 @@ let rec init_f_of_scope rp (node, prefix, eqs) = let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in let state_eq (st, _) = let sc_f = - init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body) + let st_scope = (node, aid^"."^st.st_name^".", st.body) in + let clock_scope, clock_eq = gen_clock_init rp st_scope in + f_and clock_eq (init_f_of_scope rp st_scope clock_scope) in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until in List.fold_left f_and init_eq (List.map state_eq states) in - let time_eq = - f_and - (if not (rp.no_time_scope (node^"/")) - then - BRel(AST_EQ, - NIdent(node^"/"^prefix^"time"), - NIntConst 0) - else BConst true) - (if rp.init_scope (node^"/") - then - f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) - else BConst true) - in - List.fold_left f_and time_eq (List.map do_eq eqs) + f_and_list (List.map do_eq eqs) and init_f_of_prog rp = - init_f_of_scope rp rp.root_scope + let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in + f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope) (* Get expressions for guarantee violation *) -let rec g_of_scope td (node, prefix, eqs) cond = +let rec g_of_scope td (node, prefix, eqs) clock_scope cond = let expr_g e = let instance_g (_, id, eqs, args) = - g_of_scope td (node^"/"^id, "", eqs) cond + g_of_scope td (node^"/"^id, "", eqs) clock_scope cond in List.fold_left (fun x i -> (instance_g i) @ x) [] (extract_instances td.rp.p e) @@ -406,21 +445,23 @@ let rec g_of_scope td (node, prefix, eqs) cond = | AST_assign(_, e) | AST_assume(_, e) -> expr_g e | AST_guarantee((id, _), e) -> - (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e))) + (id, f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e))) :: (expr_g e) | AST_activate (b, _) -> let rec cond_g cond = function | AST_activate_body b -> - g_of_scope td (node, b.act_id^".", b.body) cond + let bscope = node, b.act_id^".", b.body in + g_of_scope td bscope (clock_scope_here bscope) cond | AST_activate_if(c, a, b) -> - (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @ - (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @ + (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) c)) a) @ + (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(c), snd c))) b) @ (expr_g c) in cond_g cond b | AST_automaton (aid, states, _) -> let st_g (st, _) = - g_of_scope td (node, aid^"."^st.st_name^".", st.body) + let stscope = (node, aid^"."^st.st_name^".", st.body) in + g_of_scope td stscope (clock_scope_here stscope) (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name))) in List.flatten (List.map st_g states) @@ -433,4 +474,4 @@ and guarantees_of_prog rp = consts = I.consts rp; } in - g_of_scope td rp.root_scope (BConst true) + g_of_scope td rp.root_scope "" (BConst true) |