Implementation of disjunction domain seems to work.

11 files changed, 619 insertions, 547 deletions

diff --git a/Makefile b/Makefile
index ee85664..93ae422 100644
--- a/Makefile
+++ b/Makefile
@@ -17,7 +17,7 @@ SRC= 	main.ml \
 		abstract/nonrelational.ml \
 		abstract/apron_domain.ml \
 		abstract/num_domain.ml \
-		abstract/abs_domain.ml \
+		abstract/enum_domain.ml \
 		\
 		abstract/formula.ml \
 		abstract/formula_printer.ml \
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)
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 0417d27..aca8d15 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -32,8 +32,8 @@ type scope = id * id * eqn ext list
 type rooted_prog = {
     p              : prog;
 
-    no_time_scope  : id list;    (* scopes in which not to introduce time variable *)
-    init_scope     : id list;    (* scopes in which to introduce init variable *)
+    no_time_scope  : id -> bool; (* scopes in which not to introduce time variable *)
+    init_scope     : id -> bool; (* scopes in which to introduce init variable *)
 
     root_node      : node_decl;
     root_scope     : scope;
@@ -179,13 +179,13 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
     let v =
-      if not (List.mem (node^"/") rp.no_time_scope)
+      if not (rp.no_time_scope (node^"/"))
       then
         (false, node^"/"^prefix^"time", TInt)::
         (false, "N"^node^"/"^prefix^"time", TInt)::v
       else v in
     let v =
-      if List.mem (node^"/") rp.init_scope
+      if rp.init_scope (node^"/")
         then
           (false, node^"/"^prefix^"init", bool_type)::
           (false, "N"^node^"/"^prefix^"init", bool_type)::v
@@ -197,7 +197,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
     root_prog : prog -> id -> string list -> string list -> rooted_prog
 *)
 let root_prog p root no_time_scope init_scope =
-    let (root_node, _) = find_node_decl p root in
+    let (root_node, _) =
+      try find_node_decl p root
+      with Not_found -> error ("No such root node: " ^ root) in
     let root_scope = ("", "", root_node.body) in
 
     let const_vars = List.map
diff --git a/main.ml b/main.ml
index 3cef6bd..1de08be 100644
--- a/main.ml
+++ b/main.ml
@@ -1,14 +1,15 @@
 open Ast
 
+open Num_domain
+open Nonrelational
+open Apron_domain
+
 module Interpret = Interpret.I
 
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
-module ItvD = Abs_domain.D(ItvND)
-
-module ApronD = Abs_domain.D(Apron_domain.ND)
 
-module AI_Itv = Abs_interp.I(ItvD)
-module AI_Rel = Abs_interp.I(ApronD)
+module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND)
+module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND)
 
 (* command line options *)
 let dump = ref false
@@ -21,6 +22,7 @@ let ai_root = ref "test"
 let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
 let ai_init_scopes = ref ""
+let ai_disj_v = ref ""
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -35,11 +37,13 @@ let options = [
     "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
     "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
     "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis.";
+    "--disj", Arg.Set_string ai_disj_v, "Variables for which to introduce a disjunction.";
     "--init", Arg.Set_string ai_init_scopes, "Scopes for which to introduce a 'init' variable in analysis.";
 ]
 
 let do_test_interpret prog verbose =
-    let s0 = Interpret.init_state (Typing.root_prog prog "test" [] []) in
+    let f0 _ = false in
+    let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in
     if verbose then begin
       Format.printf "Init state:@.";
       Interpret.print_state Format.std_formatter s0;
@@ -85,12 +89,19 @@ let () =
 
       if !ai_itv || !ai_rel then begin
           let comma_split = Str.split (Str.regexp ",") in
+          let select_f x =
+              if x = "all"
+                then (fun _ -> true)
+                else (fun i -> List.mem i (comma_split x))
+          in
           let rp = Typing.root_prog prog !ai_root
-              (comma_split !ai_no_time_scopes)
-              (comma_split !ai_init_scopes) in
+              (select_f !ai_no_time_scopes)
+              (select_f !ai_init_scopes) in
 
-          if !ai_itv then AI_Itv.do_prog !ai_widen_delay rp;
-          if !ai_rel then AI_Rel.do_prog !ai_widen_delay rp;
+          let disj = select_f !ai_disj_v in
+          
+          if !ai_itv then AI_Itv.do_prog !ai_widen_delay disj rp;
+          if !ai_rel then AI_Rel.do_prog !ai_widen_delay disj rp;
       end;
 
       if !vtest then do_test_interpret prog true