summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-24 17:12:04 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-24 17:12:04 +0200
commit99cf7409d4eaacd7f8b86ff4de8b92c86a10dd5f (patch)
tree4fddba970a4a5db064d48859c9525baff4d4ae6f /abstract
parent6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4 (diff)
downloadscade-analyzer-99cf7409d4eaacd7f8b86ff4de8b92c86a10dd5f.tar.gz
scade-analyzer-99cf7409d4eaacd7f8b86ff4de8b92c86a10dd5f.zip
Implementation of disjunction domain seems to work.
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_domain.ml401
-rw-r--r--abstract/abs_interp.ml468
-rw-r--r--abstract/apron_domain.ml38
-rw-r--r--abstract/enum_domain.ml144
-rw-r--r--abstract/intervals_domain.ml8
-rw-r--r--abstract/nonrelational.ml33
-rw-r--r--abstract/num_domain.ml15
-rw-r--r--abstract/transform.ml14
8 files changed, 590 insertions, 531 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
deleted file mode 100644
index d6ff489..0000000
--- a/abstract/abs_domain.ml
+++ /dev/null
@@ -1,401 +0,0 @@
-open Ast
-open Formula
-open Num_domain
-open Typing
-open Util
-
-type disjunct_policy =
- | DAlways
- | DNever
- | DSometimes
-
-module type ENVIRONMENT_DOMAIN = sig
- type t
- type itv
-
- (* construction *)
- val init : t
- val bottom : t
- val vbottom : t -> t (* bottom value with same environment *)
- val is_bot : t -> bool
-
- (* variable management *)
- val addvar : t -> id -> Typing.typ -> t
- val rmvar : t -> id -> t
- val vars : t -> (id * Typing.typ) list
-
- val forgetvar : t -> id -> t
- val var_itv : t -> id -> itv
- val set_disjunct : t -> id -> disjunct_policy -> t
-
- (* set_theoretic operations *)
- val join : t -> t -> t (* union *)
- val meet : t -> t -> t (* intersection *)
- val widen : t -> t -> t
-
- val subset : t -> t -> bool
- val eq : t -> t -> bool
-
- (* abstract operations *)
- val apply_f : t -> bool_expr -> t
- val apply_cl : t -> conslist -> t
- val assign : t -> (id * id) list -> t
-
- (* pretty-printing *)
- val print_vars : Format.formatter -> t -> id list -> unit
- val print_all : Format.formatter -> t -> unit
- val print_itv : Format.formatter -> itv -> unit
-
-end
-
-
-module D_ignore_enum (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
-struct
- type t = ND.t
- type itv = ND.itv
-
-
- let init = ND.init
- let bottom = ND.bottom
- let vbottom = ND.vbottom
- let is_bot = ND.is_bot
-
- let addvar x id ty = ND.addvar x id (ty = TReal)
- let rmvar = ND.rmvar
- let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x)
-
- let forgetvar = ND.forgetvar
- let var_itv = ND.var_itv
- let set_disjunct x _ _ = x
-
- let join = ND.join
- let meet = ND.meet
- let widen = ND.widen
-
- let subset = ND.subset
- let eq = ND.eq
-
- let rec apply_cl x (econs, cons, rest) = match rest with
- | CLTrue ->
- ND.apply_ncl x cons
- | CLFalse -> vbottom x
- | CLAnd(a, b) ->
- let y = apply_cl x (econs, cons, a) in
- apply_cl y (econs, cons, b)
- | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
- let y = apply_cl x (econs@eca, cons@ca, ra) in
- let z = apply_cl x (econs@ecb, cons@cb, rb) in
- join y z
-
- let apply_f x f = apply_cl x (conslist_of_f f)
-
- let assign x v = ND.assign x (List.map (fun (id, id2) -> id, NIdent id2) v)
-
- let print_vars = ND.print_vars
- let print_all = ND.print_all
- let print_itv = ND.print_itv
-end
-
-module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
-
- module Valuation = struct
- type t = string VarMap.t
- let compare = VarMap.compare Pervasives.compare
-
- let subset a b =
- VarMap.for_all
- (fun id v ->
- try v = VarMap.find id b
- with Not_found -> true)
- a
-
- let print fmt x =
- let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x) in
- let s = List.sort Pervasives.compare b in
- let rec bl = function
- | [] -> []
- | (v, id)::q ->
- begin match bl q with
- | (vv, ids)::q when vv = v -> (v, id::ids)::q
- | r -> (v, [id])::r
- end
- 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;
- Format.fprintf fmt " ≡ %s@]" v)
- sbl;
- Format.fprintf fmt " }@]"
-
- end
- module VMap = Mapext.Make(Valuation)
-
- type t = {
- nvars : (id * bool) list;
- evars : (id * string list) list;
- nd_init : ND.t;
- nd_bottom : ND.t;
- value : ND.t VMap.t;
- disj_v : id list;
- nodisj_v : id list;
- }
- type itv =
- | IN of ND.itv VMap.t
- | IE of SSet.t
-
-
- let init = {
- nvars = []; evars = []; disj_v = []; nodisj_v = [];
- nd_init = ND.init;
- nd_bottom = ND.bottom;
- value = VMap.singleton VarMap.empty ND.init;
- }
- let bottom = {
- nvars = []; evars = []; disj_v = []; nodisj_v = [];
- nd_init = ND.init;
- nd_bottom = ND.bottom;
- value = VMap.empty;
- }
- let vbottom x = { x with value = VMap.empty }
-
- let is_bot x = VMap.is_empty x.value || VMap.for_all (fun _ v -> ND.is_bot v) x.value
-
- let strict value =
- VMap.filter (fun _ v -> not (ND.is_bot v)) value
-
- let add_case_w widen x (enum, num) =
- let value = x.value in
- let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in
- let v =
- if VMap.exists
- (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0)
- value
- || ND.is_bot num
- then
- value
- else
- try VMap.add enum
- ((if widen then ND.widen else ND.join) (VMap.find enum value) num)
- value
- with Not_found -> VMap.add enum num value
- in { x with value = v }
- let add_case = add_case_w false
-
- let addvar x id ty = match ty with
- | TInt | TReal ->
- let is_real = (ty = TReal) in
- { x with
- nvars = (id, is_real)::(x.nvars);
- nd_init = ND.addvar x.nd_init id is_real;
- nd_bottom = ND.addvar x.nd_bottom id is_real;
- value = VMap.map (fun v -> ND.addvar v id is_real) x.value
- }
- | TEnum options ->
- { x with
- evars = (id, options)::x.evars
- }
-
- let vars x =
- List.map (fun (id, r) -> id, if r then TReal else TInt) x.nvars @
- List.map (fun (id, o) -> id, TEnum o) x.evars
-
- let forgetvar x id =
- if List.mem_assoc id x.evars then
- VMap.fold
- (fun enum num value ->
- let enum' = VarMap.remove id enum in
- add_case value (enum', num))
- x.value
- { x with value = VMap.empty }
- else
- { x with value = strict @@ VMap.map (fun v -> ND.forgetvar v id) x.value }
-
- let rmvar x id =
- if List.mem_assoc id x.evars then
- let y = forgetvar x id in
- { y with
- evars = List.remove_assoc id x.evars }
- else
- { x with
- nvars = List.remove_assoc id x.nvars;
- value = strict @@ VMap.map (fun v -> ND.rmvar v id) x.value }
-
- let var_itv x id =
- if List.mem_assoc id x.nvars
- 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
- disj_v = (if p = DAlways then id::x.disj_v
- else List.filter ((<>) id) x.disj_v);
- nodisj_v = (if p = DNever then id::x.nodisj_v
- else List.filter ((<>) id) x.nodisj_v);
- }
-
- let join x y =
- VMap.fold
- (fun enum num value -> add_case value (enum, num))
- y.value
- x
- let meet x y = not_implemented "meet for enum+num domain"
- let widen x y =
- let value = VMap.merge
- (fun _ a b -> match a, b with
- | Some x, None -> Some x
- | None, Some y -> Some y
- | Some x, Some y -> Some (ND.widen x y)
- | _ -> None)
- x.value y.value
- in { x with value = value }
-
- (* Some cases of subset/equality not detected *)
- let subset a b =
- VMap.for_all
- (fun enum num ->
- VMap.exists
- (fun enum_b num_b ->
- Valuation.subset enum enum_b && ND.subset num num_b)
- b.value)
- a.value
- let eq a b = subset a b && subset b a
-
- (* Constraints ! *)
- let apply_ec x (op, a, b) =
- VMap.fold
- (fun enum num value ->
- match a, b with
- | i, EItem u ->
- begin try let v = VarMap.find i enum in
- if (if op = E_EQ then u = v else u <> v)
- then add_case value (enum, num)
- else value
- with Not_found ->
- if op = E_EQ
- then add_case value (VarMap.add i u enum, num)
- else (* MAKE A DISJUNCTION *)
- List.fold_left
- (fun value item ->
- add_case value (VarMap.add i item enum, num))
- value
- (List.filter ((<>) u) (List.assoc i x.evars))
- end
- | i, EIdent j ->
- begin
- try let x = VarMap.find i enum in
- try let y = VarMap.find j enum in
- if (if op = E_EQ then x = y else x <> y)
- then add_case value (enum, num)
- else value
- with Not_found (* J not found *) ->
- add_case value (VarMap.add j x enum, num)
- with Not_found (* I not found *) ->
- try let y = VarMap.find j enum in
- add_case value (VarMap.add i y enum, num)
- with Not_found (* J not found *) ->
- if op = E_EQ
- then (* MAKE A DISJUNCTION ! *)
- List.fold_left
- (fun value item ->
- let enum = VarMap.add i item enum in
- let enum = VarMap.add j item enum in
- add_case value (enum, num))
- value
- (List.assoc i x.evars)
- else
- add_case value (enum, num)
- end)
- x.value
- { x with value = VMap.empty }
-
- let apply_ecl x cons =
- let f x = List.fold_left apply_ec x cons in
- fix eq f x
-
-
- let apply_ncl x econs =
- { x with value = strict @@ VMap.map (fun x -> ND.apply_ncl x econs) x.value }
-
- let rec apply_cl x (econs, ncons, rest) = match rest with
- | CLTrue ->
- let y = apply_ecl x econs in
- let z = apply_ncl y ncons in
- z
- | CLFalse -> vbottom x
- | CLAnd(a, b) ->
- let y = apply_cl x (econs, ncons, a) in
- apply_cl y (econs, ncons, b)
- | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
- let y = apply_cl x (econs@eca, ncons@ca, ra) in
- let z = apply_cl x (econs@ecb, ncons@cb, rb) in
- join y z
-
- let apply_f x f = apply_cl x (conslist_of_f f)
-
- let assign x e =
- let ee, ne = List.partition (fun (id, id2) -> List.mem_assoc id x.evars) e in
- let ne_e = List.map (fun (id, id2) -> id, NIdent id2) ne in
-
- VMap.fold
- (fun enum0 num value ->
- let enum = List.fold_left
- (fun enum (id, id2) ->
- try let y = VarMap.find id2 enum0 in
- VarMap.add id y enum
- with Not_found ->
- VarMap.remove id enum)
- enum0 ee
- in
- add_case value (enum, ND.assign num ne_e))
- x.value
- { x with value = VMap.empty }
-
- let print_all fmt x =
- Format.fprintf fmt "@[<v>";
- VMap.iter
- (fun enum num ->
- Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ "
- Valuation.print enum ND.print_all num)
- x.value;
- Format.fprintf fmt "@]"
-
- let print_vars fmt x idl = print_all fmt x (* TODO *)
-
- let print_itv fmt = function
- | IN x ->
- Format.fprintf fmt "@[<v 0>";
- VMap.iter
- (fun enum i ->
- Format.fprintf fmt "%a when %a@ "
- ND.print_itv i Valuation.print enum)
- x;
- Format.fprintf fmt "@]"
- | IE x ->
- Format.fprintf fmt "@[<hov 2>{ ";
- SSet.iter (fun x -> Format.fprintf fmt "%s@ " x) x;
- Format.fprintf fmt "}@]"
-
-end
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index a610843..8d5f1c9 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -4,42 +4,244 @@ open Formula
open Typing
open Util
-open Abs_domain
open Num_domain
+open Enum_domain
-module I (E : ENVIRONMENT_DOMAIN) : sig
+
+module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
type st
- val do_prog : int -> rooted_prog -> unit
+ val do_prog : int -> (id -> bool) -> rooted_prog -> unit
end = struct
+ (* **************************
+ Disjunction domain
+ ************************** *)
+
+ type case_v = ED.t * ND.t
+ type case = ED.item list
+
+ type dd_v = {
+ d_vars : id list;
+ data : (case, case_v) Hashtbl.t;
+ }
+
+ (*
+ print_dd : Formatter.t -> dd_v -> unit
+ *)
+ let print_aux fmt d_vars env =
+ let print_it q (enum, num) =
+ Format.fprintf fmt "@[<hov 4>";
+ List.iter2
+ (fun id v -> Format.fprintf fmt "%a ≡ %s,@ "
+ Formula_printer.print_id id v)
+ d_vars q;
+ Format.fprintf fmt "@ %a,@ %a@]@."
+ ED.print enum ND.print num;
+ in
+ Hashtbl.iter print_it env
+ let print_dd fmt dd = print_aux fmt dd.d_vars dd.data
+
+
+ (*
+ dd_bot : id list -> dd_v
+ *)
+ let dd_bot d_vars = { d_vars; data = Hashtbl.create 12 }
+
+ (*
+ dd_add_case : dd_v -> case_v -> unit
+ *)
+ let dd_add_case env (enum, num) =
+ let rec aux enum vals = function
+ | [] ->
+ let case = List.rev vals in
+ begin try let e0, n0 = Hashtbl.find env.data case in
+ Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0);
+ with Not_found ->
+ Hashtbl.add env.data case (enum, num);
+ end
+ | p::q ->
+ List.iter
+ (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
+ | [en] -> aux en (v::vals) q
+ | _ -> assert false)
+ (ED.project enum p)
+ in aux enum [] env.d_vars
+
+ (*
+ dd_singleton : id list -> case_v -> dd_v
+ *)
+ let dd_singleton d_vars d =
+ let v = { d_vars; data = Hashtbl.create 1 } in
+ dd_add_case v d;
+ v
+
+ (*
+ dd_extract_case : dd_v -> case -> dd_v
+ *)
+ let dd_extract_case v case =
+ try dd_singleton v.d_vars (Hashtbl.find v.data case)
+ with Not_found -> dd_bot v.d_vars
+
+
+ (*
+ dd_apply_ncons : dd_v -> num_cons list -> dd_v
+ *)
+ let dd_apply_ncl v ncl =
+ let vv = dd_bot v.d_vars in
+ Hashtbl.iter (fun case (enum, num) ->
+ let num = ND.apply_cl num ncl in
+ if not (ND.is_bot num) then
+ Hashtbl.add vv.data case (enum, num))
+ v.data;
+ vv
+
+ (*
+ dd_apply_econs : dd_v -> enum_cons -> dd_v
+ *)
+ let dd_apply_econs v cons =
+ let vv = dd_bot v.d_vars in
+ Hashtbl.iter (fun case (enum, num) ->
+ List.iter
+ (fun enum -> dd_add_case vv (enum, num))
+ (ED.apply_cons enum cons))
+ v.data;
+ vv
+
+ (*
+ dd_join : dd_v -> dd_v -> dd_v
+ *)
+ let dd_join a b =
+ let vv = { d_vars = a.d_vars; data = Hashtbl.copy a.data } in
+ Hashtbl.iter (fun case (enum, num) ->
+ try let e2, n2 = Hashtbl.find vv.data case in
+ Hashtbl.replace vv.data case (ED.join e2 enum, ND.join n2 num)
+ with Not_found -> Hashtbl.replace vv.data case (enum, num))
+ b.data;
+ vv
+
+ (*
+ dd_meet : dd_v -> dd_v -> dd_v
+ *)
+ let dd_meet a b =
+ let vv = dd_bot a.d_vars in
+ Hashtbl.iter (fun case (enum, num) ->
+ try let e2, n2 = Hashtbl.find b.data case in
+ let en, nn = ED.meet enum e2, ND.meet n2 num in
+ if not (ND.is_bot nn) then Hashtbl.add vv.data case (en, nn)
+ with _ -> ())
+ a.data;
+ vv
+
+ (*
+ dd_apply_cl : dd_v -> conslist -> dd_v
+ *)
+ let rec apply_cl env (ec, nc, r) =
+ match r with
+ | CLTrue ->
+ let env_ec = List.fold_left dd_apply_econs env ec in
+ let env_nc = dd_apply_ncl env_ec nc in
+ (* Format.printf "[[ %a -> %a ]]@."
+ print_dd env print_dd env_nc; *)
+ env_nc
+ | CLFalse -> dd_bot env.d_vars
+ | CLAnd(a, b) ->
+ let env = apply_cl env (ec, nc, a) in
+ apply_cl env (ec, nc, b)
+ | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+ dd_join (apply_cl env (ec@eca, nc@nca, ra))
+ (apply_cl env (ec@ecb, nc@ncb, rb))
+
+
+ (* ***************************
+ Abstract interpretation
+ *************************** *)
+
type st = {
rp : rooted_prog;
widen_delay : int;
- env : E.t;
+
+ enum_vars : (id * ED.item list) list;
+ num_vars : (id * bool) list;
+
+ (* program expressions *)
f : bool_expr;
cl : conslist;
f_g : bool_expr;
cl_g : conslist;
guarantees : (id * bool_expr) list;
+
+ (* abstract interpretation *)
+ cycle : (id * id * typ) list; (* s'(x) = s(y) *)
+ forget : (id * typ) list; (* s'(x) not specified *)
+ d_vars : id list; (* disjunction variables *)
+ top : case_v;
+ env : (case, case_v) Hashtbl.t;
+ mutable delta : case list;
+ widen : (case, int) Hashtbl.t;
}
+ (*
+ print_st : Formatter.t -> st -> unit
+ *)
+ let print_st fmt st = print_aux fmt st.d_vars st.env
- (* init state *)
- let init_state widen_delay rp =
- let env = List.fold_left
- (fun env (_, id, ty) -> E.addvar env id ty)
- E.init
- rp.all_vars
- in
+ (*
+ add_case : st -> case_v -> unit
+ *)
+ let add_case st (enum, num) =
+ let rec aux enum vals = function
+ | [] ->
+ let case = List.rev vals in
+ begin try let e0, n0 = Hashtbl.find st.env case in
+ if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
+ begin try
+ let n = Hashtbl.find st.widen case in
+ let jw = if n < st.widen_delay then ND.join else ND.widen in
+ Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
+ Hashtbl.replace st.widen case (n+1);
+ with Not_found ->
+ Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0);
+ Hashtbl.add st.widen case 0;
+ end;
+ if not (List.mem case st.delta) then st.delta <- case::st.delta
+ end
+ with Not_found ->
+ Hashtbl.add st.env case (enum, num);
+ if not (List.mem case st.delta) then st.delta <- case::st.delta
+ end
+ | p::q ->
+ List.iter
+ (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
+ | [en] -> aux en (v::vals) q
+ | _ -> assert false)
+ (ED.project enum p)
+ in aux enum [] st.d_vars
+
+
+
+ (*
+ init_state : int -> rooted_prog -> st
+ *)
+ let init_state widen_delay disj rp =
Format.printf "Vars: @[<hov>%a@]@.@."
(Ast_printer.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 init_f = Transform.init_f_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
+ let init_cl = conslist_of_f init_f in
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
@@ -51,96 +253,192 @@ end = struct
let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
- Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
-
- let env = E.set_disjunct env "/exit" DNever in
- let env = E.apply_f env init_f in
+ Format.printf "Cycle formula with guarantees:@.%a@.@."
+ Formula_printer.print_expr f_g;
let cl = Formula.conslist_of_f f in
let cl_g = Formula.conslist_of_f f_g in
- { rp; widen_delay;
- f; cl; f_g; cl_g;
- guarantees; env }
-
- (*
- pass_cycle : var_def list -> E.t -> E.t
-
- Does :
- - x <- Nx, for all x
- - ignore x for all x such that Nx does not exist
- *)
- let pass_cycle vars e =
- let tr_assigns = List.fold_left
- (fun q (_, id, _) ->
+ (* calculate cycle variables and forget variables *)
+ let cycle = List.fold_left
+ (fun q (_, id, ty) ->
if id.[0] = 'N' then
- (String.sub id 1 (String.length id - 1), id)::q
- else
- q)
- [] vars
+ (String.sub id 1 (String.length id - 1), id, ty)::q
+ else q)
+ [] rp.all_vars
in
- let e = E.assign e tr_assigns in
-
- let forget_vars = List.map (fun (_, id, _) -> id)
+ let forget = List.map (fun (_, id, ty) -> (id, ty))
(List.filter
- (fun (_, id, _) ->
- not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
- vars) in
- let e = List.fold_left E.forgetvar e forget_vars in
- e
+ (fun (_, id, _) ->
+ not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
+ rp.all_vars)
+ in
+
+ (* calculate disjunction variables *)
+ (* first approximation : use all enum variables appearing in init formula *)
+ let rec calculate_dvars (ec, _, r) =
+ let a = List.map (fun (_, id, _) -> id) ec in
+ let rec aux = function
+ | CLTrue | CLFalse -> []
+ | CLAnd(u, v) ->
+ aux u @ aux v
+ | CLOr(u, v) ->
+ calculate_dvars u @ calculate_dvars v
+ in a @ aux r
+ in
+ let d_vars_0 = calculate_dvars init_cl in
+ let d_vars_1 = List.filter
+ (fun id -> disj id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+ (List.map (fun (id, _) -> id) enum_vars) in
+ let d_vars = d_vars_0 @ d_vars_1 in
+
+ (* setup abstract data *)
+ let top = ED.top enum_vars, ND.top num_vars in
+ let delta = [] in
+ let widen = Hashtbl.create 12 in
+ (* calculate initial state and environment *)
+ let init_s = dd_bot d_vars in
+
+ let init_ec, _, _ = init_cl in
+ let init_ed = List.fold_left
+ (fun ed cons ->
+ List.flatten (List.map (fun x -> ED.apply_cons x cons) ed))
+ [ED.top enum_vars] (init_ec) in
+ List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed;
+ let env_dd = apply_cl init_s init_cl in
+ let env = env_dd.data in
+
+ let st =
+ { rp; widen_delay; enum_vars; num_vars;
+ f; cl; f_g; cl_g; guarantees;
+ cycle; forget; d_vars; top;
+ env; delta; widen } in
+
+ Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
+
+ st
- (* cycle : st -> cl -> env -> env *)
- let cycle st cl i =
- (pass_cycle st.rp.all_vars (E.apply_cl i cl))
(*
- loop : st -> env -> env -> env
+ pass_cycle : st -> case_v -> case_v
*)
- let loop st acc0 =
+ let pass_cycle st (enum, num) =
+ let assign_e =
+ List.map (fun (a, b, _) -> a, b)
+ (List.filter
+ (fun (_, _, t) -> match t with TEnum _ -> true | _ -> false)
+ st.cycle) in
+ let assign_n =
+ List.map (fun (a, b, _) -> a, NIdent b)
+ (List.filter
+ (fun (_, _, t) -> match t with TInt | TReal -> true | _ -> false)
+ st.cycle) in
- Format.printf "Loop @[<hv>%a@]@.@."
- Formula_printer.print_conslist st.cl;
+ let enum = ED.assign enum assign_e in
+ let num = ND.assign num assign_n in
- let fsharp cl i =
- Format.printf "Acc @[<hv>%a@]@." E.print_all i;
- let j = cycle st cl i in
- E.join acc0 j
- in
+ List.fold_left
+ (fun (enum, num) (var, t) -> match t with
+ | TEnum _ -> ED.forgetvar enum var, num
+ | TReal | TInt -> enum, ND.forgetvar num var)
+ (enum, num) st.forget
- let rec iter n i =
- let i' =
- if n < st.widen_delay
- then E.join i (fsharp st.cl i)
- else E.widen i (fsharp st.cl_g i)
- in
- if E.eq i i' then i else iter (n+1) i'
- in
+ let dd_pass_cycle st (v : dd_v) =
+ let vv = dd_bot v.d_vars in
+ Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
+ vv
+
+ (*
+ cycle : st -> cl -> dd_v -> dd_v
+ *)
+ let cycle st cl env =
+ let env_f = apply_cl env cl in
+ (* Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f; *)
+ dd_pass_cycle st env_f
- let x = iter 0 acc0 in
- let y = fix E.eq (fsharp st.cl) x in (* decreasing iteration *)
- let z = E.apply_cl y st.cl in (* no more guarantee *)
- y, z
+
+ (*
+ set_target_case : st -> dd_v -> case -> dd_v
+ *)
+ let set_target_case st env case =
+ List.fold_left2
+ (fun env id v ->
+ if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
+ dd_apply_econs env (E_EQ, "N"^id, EItem v)
+ else env)
+ env st.d_vars case
(*
do_prog : rooted_prog -> unit
*)
- let do_prog widen_delay rp =
- let st = init_state widen_delay rp in
+ let do_prog widen_delay disj rp =
+ let st = init_state widen_delay disj rp in
+
+ Format.printf "Init: %a@." print_st st;
+
+ let n_ch_iter = ref 0 in
- let final_nc, final = loop st st.env in
+ (* chaotic iteration loop *)
+ while st.delta <> [] do
+ let case = List.hd st.delta in
+
+ incr n_ch_iter;
+ Format.printf "Chaotic iteration %d: @[<hov>[%a]@]@."
+ !n_ch_iter
+ (Ast_printer.print_list Formula_printer.print_id ", ") case;
+
+ let start = try Hashtbl.find st.env case with Not_found -> assert false in
+ let start_dd = dd_singleton st.d_vars start in
+ let f i =
+ let i = dd_singleton st.d_vars i in
+ let i' = set_target_case st i case in
+ let q = dd_join start_dd (cycle st st.cl i') in
+ try Hashtbl.find q.data case with Not_found -> assert false
+ in
+
+ let rec iter n (i_enum, i_num) =
+ let fi_enum, fi_num = f (i_enum, i_num) in
+ let j_enum, j_num =
+ if n < st.widen_delay then
+ ED.join i_enum fi_enum, ND.join i_num fi_num
+ else
+ ED.join i_enum fi_enum, ND.widen i_num fi_num
+ in
+ if ED.eq j_enum i_enum && ND.eq j_num i_num
+ then (i_enum, i_num)
+ else iter (n+1) (j_enum, j_num)
+ in
+ let y = iter 0 start in
+ let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in
+
+ let i = dd_singleton st.d_vars z in
+ let j = cycle st st.cl i in
+ let cases = ref [] in
+ Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
+ List.iter
+ (fun case ->
+ let i' = set_target_case st i case in
+ let j = cycle st st.cl i' in
+ Hashtbl.iter (fun _ q -> add_case st q) j.data)
+ !cases;
+
+ st.delta <- List.filter ((<>) case) st.delta;
+
+ (* Format.printf "Final: %a@." print_st st; *)
+
+ done;
+
+ let final = apply_cl { d_vars = st.d_vars; data = st.env } st.cl in
+ Format.printf "Accessible: %a@." print_dd final;
- Format.printf "@[<hov>F %a@]@.@."
- E.print_all final_nc;
- Format.printf "@[<hov>F' %a@]@.@."
- E.print_all final;
let check_guarantee (id, f) =
let cl = Formula.conslist_of_f f in
Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
id Formula_printer.print_conslist cl;
- let z = E.apply_cl final cl in
- if E.is_bot z then
+ let z = apply_cl final cl in
+ if Hashtbl.length z.data = 0 then
Format.printf "OK@]@ "
else
Format.printf "FAIL@]@ "
@@ -153,12 +451,26 @@ end = struct
if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
Format.printf "Probes: @[<v 0>";
- List.iter (fun (p, id, _) ->
- if p then Format.printf "%a ∊ %a@ "
- Formula_printer.print_id id
- E.print_itv (E.var_itv final id))
+ List.iter (fun (p, id, ty) ->
+ if p then begin
+ Format.printf "%a ∊ @[<v>" Formula_printer.print_id id;
+ Hashtbl.iter (fun case (enum, num) ->
+ begin match ty with
+ | TInt | TReal ->
+ Format.printf "%a" ND.print_itv (ND.project num id)
+ | TEnum _ ->
+ Format.printf "@[<hov>{ %a }@]"
+ (Ast_printer.print_list Formula_printer.print_id ", ")
+ (ED.project enum id)
+ end;
+ Format.printf " when @[<hov>[%a]@]@ "
+ (Ast_printer.print_list Formula_printer.print_id ", ") case)
+ final.data;
+ Format.printf "@]@ "
+ end)
st.rp.all_vars;
Format.printf "@]@."
end
end
+
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 369f4b7..7a823db 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -58,27 +58,23 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
(* implementation *)
- let init = Abstract1.top manager (Environment.make [||] [||])
- let bottom = Abstract1.bottom manager (Environment.make [||] [||])
+ let v_env vars =
+ let intv = List.map
+ (fun (s, _) -> Var.of_string s)
+ (List.filter (fun (_, n) -> not n) vars) in
+ let realv = List.map
+ (fun (s, _) -> Var.of_string s)
+ (List.filter (fun (_, n) -> n) vars) in
+ (Environment.make (Array.of_list intv) (Array.of_list realv))
+
+ let top vars =
+ Abstract1.top manager (v_env vars)
+ let bottom vars = Abstract1.bottom manager (v_env vars)
let is_bot = Abstract1.is_bottom manager
- let addvar x id isfloat =
- let env = Abstract1.env x in
- let env2 = if isfloat then
- Environment.add env [||] [| Var.of_string id |]
- else
- Environment.add env [| Var.of_string id |] [||]
- in
- Abstract1.change_environment manager x env2 false
let forgetvar x id =
let v = [| Var.of_string id |] in
Abstract1.forget_array manager x v false
- let rmvar x id =
- let v = [| Var.of_string id |] in
- let env = Abstract1.env x in
- let env2 = Environment.remove env v in
- let y = Abstract1.forget_array manager x v false in
- Abstract1.change_environment manager y env2 false
let vars x =
let (ivt, fvt) = Environment.vars (Abstract1.env x) in
@@ -89,17 +85,19 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
let vbottom x =
Abstract1.bottom manager (Abstract1.env x)
- let var_itv x id =
+ let project x id =
Abstract1.bound_variable manager x (Var.of_string id)
(* Apply some formula to the environment *)
- let rec apply_ncl x cons =
+ let apply_cl x cons =
let env = Abstract1.env x in
let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
let ar = Tcons1.array_make env (Array.length tca) in
Array.iteri (Tcons1.array_set ar) tca;
Abstract1.meet_tcons_array manager x ar
+ let apply_cons x cons = apply_cl x [cons]
+
let assign x eqs =
let env = Abstract1.env x in
@@ -119,7 +117,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
let eq = Abstract1.is_eq manager
(* Pretty-printing *)
- let print_all fmt x =
+ let print fmt x =
Abstract1.minimize manager x;
Abstract1.print fmt x;
Format.fprintf fmt "@?"
@@ -130,7 +128,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
let rm_vars = Array.of_list
(List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in
let xx = Abstract1.forget_array manager x rm_vars false in
- print_all fmt xx
+ print fmt xx
let print_itv = Interval.print
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
new file mode 100644
index 0000000..c8b4ec5
--- /dev/null
+++ b/abstract/enum_domain.ml
@@ -0,0 +1,144 @@
+open Ast
+open Formula
+open Util
+
+exception Bot
+
+module type ENUM_ENVIRONMENT_DOMAIN = sig
+ type t
+
+ type item = string
+
+ (* construction *)
+ val top : (id * item list) list -> t
+
+ (* variable management *)
+ val vars : t -> (id * item list) list
+
+ val forgetvar : t -> id -> t
+ val project : t -> id -> item list
+
+ (* set-theoretic operations *)
+ val join : t -> t -> t (* union *)
+ val meet : t -> t -> t (* intersection, may raise Bot *)
+
+ val subset : t -> t -> bool
+ val eq : t -> t -> bool
+
+ (* abstract operations *)
+ val apply_cons : t -> enum_cons -> t list (* may disjunct *)
+ val assign : t -> (id * id) list -> t
+
+ (* pretty-printing *)
+ val print : Format.formatter -> t -> unit
+end
+
+
+
+module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
+ type item = string
+
+ type t = {
+ vars : (id * item list) list;
+ value : item VarMap.t;
+ }
+
+ 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 when a = b -> Some a
+ | _ -> 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 -> if a = b then Some a else raise Bot
+ | _ -> None)
+ x1.value x2.value in
+ { x1 with value = v }
+
+ let subset a b =
+ VarMap.for_all
+ (fun id v ->
+ try v = VarMap.find id b.value
+ with Not_found -> true)
+ a.value
+ let eq a b =
+ VarMap.equal (=) a.value b.value
+
+ let cc op = match op with
+ | E_EQ -> (=)
+ | E_NE -> (<>)
+
+ let apply_cons x (op, id, e) =
+ match e with
+ | EItem s ->
+ begin try let t = VarMap.find id x.value in
+ if cc op s t then [x] else []
+ with Not_found ->
+ List.map (fun v -> { x with value = VarMap.add id v x.value })
+ (List.filter (cc op s) (List.assoc id x.vars))
+ end
+ | EIdent id2 ->
+ match
+ (try Some (VarMap.find id x.value) with _ -> None),
+ (try Some (VarMap.find id2 x.value) with _ -> None)
+ with
+ | None, None -> [x]
+ | None, Some s ->
+ List.map (fun v -> { x with value = VarMap.add id v x.value})
+ (List.filter (cc op s) (List.assoc id x.vars))
+ | Some s, None ->
+ List.map (fun v -> { x with value = VarMap.add id2 v x.value})
+ (List.filter (cc op s) (List.assoc id2 x.vars))
+ | Some s, Some t ->
+ if cc op s t then [x] else []
+
+ 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 ->
+ begin match bl q with
+ | (vv, ids)::q when vv = v -> (v, id::ids)::q
+ | r -> (v, [id])::r
+ end
+ 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;
+ Format.fprintf fmt " ≡ %s@]" v)
+ sbl;
+ Format.fprintf fmt " }@]"
+
+end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 92d00a2..084e397 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -10,6 +10,8 @@ module VD : VALUE_DOMAIN = struct
| Int a, Int b -> a <= b
| x, y -> x = y
+ let bound_lt a b = not (bound_leq b a) (* a < b *)
+
let bound_add a b =
match a, b with
| MInf, Int a | Int a, MInf -> MInf
@@ -77,7 +79,7 @@ module VD : VALUE_DOMAIN = struct
let subset a b = match a, b with
| Bot, _ -> true
| _, Bot -> false
- | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+ | Itv(a, b), Itv(c, d) -> bound_leq c a && bound_leq b d
let join a b = match a, b with
| Bot, x | x, Bot -> x
@@ -96,12 +98,12 @@ module VD : VALUE_DOMAIN = struct
| x, Bot | Bot, x -> x
| Itv(a, b), Itv(c, d) ->
let lb =
- if not (bound_leq a c) then
+ if bound_lt c a then
(if bound_leq (Int 0) c then Int 0 else MInf)
else a
in
let ub =
- if not (bound_leq d b) then
+ if bound_lt b d then
(if bound_leq d (Int 0) then Int 0 else PInf)
else b
in
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 6497760..3e978ce 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -15,8 +15,11 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type t = Env of env | Bot
type itv = Value_domain.itv
- let init = Env VarMap.empty
- let bottom = Bot
+ let top vars = Env
+ (List.fold_left
+ (fun e (v, _) -> VarMap.add v V.top e)
+ VarMap.empty vars)
+ let bottom _ = Bot
let get_var env id =
try VarMap.find id env
@@ -55,16 +58,14 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
| Bot -> true
| Env env -> strict env = Bot
- let addvar x id _ = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
- let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
let vars env = match env with
| Bot -> []
| Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env)
- let vbottom _ = bottom
+ let vbottom _ = Bot
- let var_itv x id = match x with
+ let project x id = match x with
| Bot -> Value_domain.Bot
| Env env -> V.to_itv (get_var env id)
@@ -95,16 +96,20 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
| Bot, x -> true
| Env _, Bot -> false
| Env m, Env n ->
- VarMap.for_all2o
- (fun _ _ -> true)
- (fun _ v -> v = V.top)
- (fun _ a b -> V.subset a b)
- m n
+ VarMap.for_all
+ (fun id vn ->
+ try let vm = VarMap.find id m in V.subset vm vn
+ with Not_found -> vn = V.top)
+ n
let eq a b = match a, b with
| Bot, Bot -> true
| Env m, Env n ->
- VarMap.equal (=) m n
+ VarMap.for_all2o
+ (fun _ v -> v = V.top)
+ (fun _ v -> v = V.top)
+ (fun _ a b -> a = b)
+ m n
| _ -> false
(* Apply some formula to the environment *)
@@ -163,7 +168,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
List.fold_left restrict_var env
(extract_var (expr, zop, NIntConst 0))
- let apply_ncl x cl =
+ let apply_cl x cl =
let f x = List.fold_left apply_cons x cl in
fix eq f x
@@ -212,7 +217,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
sbl;
Format.fprintf fmt " }@]"
- let print_all fmt x =
+ let print fmt x =
print_vars fmt x (List.map fst (vars x))
let print_itv fmt x =
diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
index 59ed1a0..96de8bc 100644
--- a/abstract/num_domain.ml
+++ b/abstract/num_domain.ml
@@ -6,18 +6,16 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
type itv
(* construction *)
- val init : t
- val bottom : t
- val vbottom : t -> t (* bottom value with same environment *)
+ val top : (id * bool) list -> t
+ val bottom : (id * bool) list -> t
+ val vbottom : t -> t (* bottom value with same variables *)
val is_bot : t -> bool
(* variable management *)
- val addvar : t -> id -> bool -> t (* integer or real variable ? *)
- val rmvar : t -> id -> t
val vars : t -> (id * bool) list
val forgetvar : t -> id -> t (* remove var from constraints *)
- val var_itv : t -> id -> itv
+ val project : t -> id -> itv
(* set-theoretic operations *)
val join : t -> t -> t (* union *)
@@ -29,12 +27,13 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
val eq : t -> t -> bool
(* abstract operation *)
- val apply_ncl : t -> num_cons list -> t
+ val apply_cons : t -> num_cons -> t
+ val apply_cl : t -> num_cons list -> t
val assign : t -> (id * num_expr) list -> t
(* pretty-printing *)
+ val print : Format.formatter -> t -> unit
val print_vars : Format.formatter -> t -> id list -> unit
- val print_all : Format.formatter -> t -> unit
val print_itv : Format.formatter -> itv -> unit
end
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b6781a8..82b6731 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -70,7 +70,7 @@ let rec f_of_neexpr td (node, prefix) where expr =
| TEnum _ -> EE(EIdent x))
typ)
| AST_arrow(a, b) ->
- if List.mem (node^"/") td.rp.init_scope
+ if td.rp.init_scope (node^"/")
then
f_or
(f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true))
@@ -306,21 +306,21 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
let time_incr_eq =
if active then
f_and
- (if not (List.mem (node^"/") td.rp.no_time_scope)
+ (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 List.mem (node^"/") td.rp.init_scope
+ (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 (List.mem (node^"/") td.rp.no_time_scope)
+ (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 List.mem (node^"/") td.rp.init_scope
+ (if td.rp.init_scope (node^"/")
then f_e_eq (EIdent("N"^node^"/"^prefix^"init"))
(EIdent (node^"/"^prefix^"init"))
else BConst true)
@@ -373,13 +373,13 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
in
let time_eq =
f_and
- (if not (List.mem (node^"/") rp.no_time_scope)
+ (if not (rp.no_time_scope (node^"/"))
then
BRel(AST_EQ,
NIdent(node^"/"^prefix^"time"),
NIntConst 0)
else BConst true)
- (if List.mem (node^"/") rp.init_scope
+ (if rp.init_scope (node^"/")
then
f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true)
else BConst true)