Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!

8 files changed, 475 insertions, 63 deletions

diff --git a/Makefile b/Makefile
index ffa531c..4a76187 100644
--- a/Makefile
+++ b/Makefile
@@ -27,6 +27,7 @@ SRC= 	main.ml \
 		abstract/varenv.ml \
 		abstract/abs_interp.ml \
 		abstract/abs_interp_edd.ml \
+		abstract/abs_interp_dynpart.ml \
 		interpret/interpret.ml \
 
 all: $(BIN)
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
new file mode 100644
index 0000000..28f9238
--- /dev/null
+++ b/abstract/abs_interp_dynpart.ml
@@ -0,0 +1,375 @@
+open Ast
+open Ast_util
+open Formula
+open Typing
+open Cmdline
+
+open Util
+open Num_domain
+open Enum_domain
+
+open Varenv
+
+module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+: sig
+
+    val do_prog : cmdline_opt -> rooted_prog -> unit
+
+end = struct
+
+    type abs_v = ED.t * ND.t
+
+    type location = {
+        id            : int;
+
+        def           : bool_expr list;   (* conjunction of formula *)
+        def_cl        : conslist;
+        is_init       : bool;
+
+        f             : bool_expr;
+        cl            : conslist;
+
+        (* For chaotic iteration fixpoint *)
+        mutable star  : bool;
+        mutable in_c  : int;
+        mutable v     : abs_v;
+
+        mutable out_t : int list;
+        mutable in_t  : int list;
+    }
+
+    type env = {
+        rp            : rooted_prog;
+        opt           : cmdline_opt;
+
+        ve            : varenv;
+
+        (* program expressions *)
+        f             : bool_expr;
+        guarantees    : (id * bool_expr) list;
+
+        (* data *)
+        loc           : (int, location) Hashtbl.t;
+        counter       : int ref;
+    }
+
+    (* **************************
+            ABSTRACT VALUES
+       ************************** *)
+
+    (*
+      top : env -> abs_v
+      bottom : env -> abs_v
+    *)
+    let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
+    let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
+    let is_bot (e, n) = ND.is_bot n
+
+    let print_v fmt (enum, num) =
+      if is_bot (enum, num) then
+        Format.fprintf fmt "⊥"
+      else
+        Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num
+
+    (*
+      join : abs_v -> abs_v -> abs_v
+      meet : abs_v -> abs_v -> abs_v
+    *)
+    let join (e1, n1) (e2, n2) =
+      if is_bot (e1, n1) then (e2, n2)
+      else if is_bot (e2, n2) then (e1, n1)
+      else (ED.join e1 e2, ND.join n1 n2)
+    let meet (e1, n1) (e2, n2) =
+      if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
+      else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
+      else
+        try (ED.meet e1 e2 , ND.meet n1 n2)
+        with Bot -> e1, ND.vbottom n1
+
+    (*
+      apply_cl : abs_v -> conslist -> abs_v
+    *)
+    let rec apply_cl (enum, num) (ec, nc, r) =
+        try
+          begin match r with
+          | CLTrue ->
+            (ED.apply_cl enum ec, ND.apply_cl num nc)
+          | CLFalse ->
+            (enum, ND.vbottom num)
+          | CLAnd(a, b) ->
+            let enum, num = apply_cl (enum, num) (ec, nc, a) in
+            let enum, num = apply_cl (enum, num) ([], nc, b) in
+            enum, num
+          | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+            let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in 
+            let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in 
+            join a b
+          end
+        with Bot -> ED.vtop enum, ND.vbottom num
+
+
+    (* ***************************
+              INTERPRET
+       *************************** *)
+
+
+
+    (*
+      init_env : cmdline_opt -> rooted_prog -> env
+    *)
+    let init_env opt rp =
+        let f = Transform.f_of_prog_incl_init rp false in
+
+        let f = simplify_k (get_root_true f) f in
+        Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
+
+        let facts = get_root_true f in
+        let f, rp, _ = List.fold_left
+          (fun (f, (rp : rooted_prog), repls) eq ->
+            match eq with
+            | BEnumCons(E_EQ, a, EIdent b)
+                when a.[0] <> 'L' && b.[0] <> 'L' ->
+
+              let a = try List.assoc a repls with Not_found -> a in
+              let b = try List.assoc b repls with Not_found -> b in
+
+              if a = b then
+                f, rp, repls
+              else begin
+                let keep, repl =
+                  if String.length a <= String.length b
+                    then a, b
+                    else b, a
+                in
+                Format.printf "Replacing %s with %s@." repl keep;
+                let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in
+                let rp =
+                  { rp with all_vars =
+                      List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
+                let repls = (repl, keep)::
+                  (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
+                f, rp, repls
+              end
+            | _ -> f, rp, repls)
+          (f, rp, []) facts in
+
+        let f = simplify_k (get_root_true f) f in
+
+        Format.printf "Complete formula after simpl:@.%a@.@."
+            Formula_printer.print_expr f;
+
+        let guarantees = Transform.guarantees_of_prog rp in
+        Format.printf "Guarantees:@.";
+        List.iter (fun (id, f) ->
+            Format.printf "  %s: %a@." id Formula_printer.print_expr f)
+          guarantees;
+        Format.printf "@.";
+        
+        let ve = mk_varenv rp f (conslist_of_f f) in
+
+        let env = {
+          rp; opt; ve; f; guarantees;
+          loc = Hashtbl.create 2; counter = ref 2; } in
+
+        (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
+        let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in
+        let rstf = simplify_k rstc f in
+        let rstf = simplify_k (get_root_true rstf) rstf in
+        let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in
+        let nrstf = simplify_k nrstc f in
+        let nrstf = simplify_k (get_root_true nrstf) nrstf in
+        Hashtbl.add env.loc 0
+          {
+            id = 0;
+            def = rstc;
+            def_cl = conslist_of_f (f_and_list rstc);
+            is_init = true;
+
+            f = rstf;
+            cl = conslist_of_f rstf;
+
+            star = false;
+            in_c = 0;
+            v = (ED.top ve.evars, ND.bottom ve.nvars);
+
+            out_t = [];
+            in_t = [];
+          };
+        Hashtbl.add env.loc 1
+          {
+            id = 1;
+            def = nrstc;
+            def_cl = conslist_of_f (f_and_list nrstc);
+            is_init = false;
+
+            f = nrstf;
+            cl = conslist_of_f nrstf;
+
+            star = false;
+            in_c = 0;
+            v = (ED.top ve.evars, ND.bottom ve.nvars);
+
+            out_t = [];
+            in_t = [];
+          };
+        env
+
+
+    (*
+      pass_cycle : env -> edd_v -> edd_v
+      unpass_cycle : env -> edd_v -> edd_v
+
+      set_target_case : env -> edd_v -> bool_expr -> edd_v
+      cycle : env -> edd_v -> conslist -> edd_v
+    *)
+    let pass_cycle env (enum, num) =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (a, b)::ae, an
+            | TInt | TReal -> ae, (a, NIdent b)::an)
+          ([], []) env.cycle in
+
+        let enum = ED.assign enum assign_e in
+        let num = ND.assign num assign_n in
+
+        let ef, nf = List.fold_left
+            (fun (ef, nf) (var, t) -> match t with
+              | TEnum _ -> var::ef, nf
+              | TReal | TInt -> ef, var::nf)
+            ([], []) env.forget in
+
+        (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+
+    let unpass_cycle env (enum, num) =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (b, a)::ae, an
+            | TInt | TReal -> ae, (b, NIdent a)::an)
+          ([], []) env.ve.cycle in
+
+        let enum = ED.assign enum assign_e in
+        let num = ND.assign num assign_n in
+
+        let ef, nf = List.fold_left
+            (fun (ef, nf) (var, t) -> match t with
+              | TEnum _ -> var::ef, nf
+              | TReal | TInt -> ef, var::nf)
+            ([], []) env.ve.forget_inv in
+
+        (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+
+    let set_target_case e v cl =
+        let tgt = (unpass_cycle e (apply_cl (top e) cl)) in
+        (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*)
+        meet v tgt
+
+    (*
+      chaotic_iter : env -> unit
+
+      Fills the values of loc[*].v, and updates out_t and in_t
+    *)
+    let chaotic_iter e =
+        let delta = ref [] in
+
+        (* Fill up initial states *)
+        Hashtbl.iter
+          (fun q loc ->
+            loc.out_t <- [];
+            loc.in_t <- [];
+            if loc.is_init then begin
+              loc.v <- apply_cl (top e) loc.cl;
+              delta := q::!delta
+            end else
+              loc.v <- bottom e)
+          e.loc;
+
+        (* Iterate *)
+        let it_counter = ref 0 in
+        while !delta <> [] do
+          let s = List.hd !delta in
+          let loc = Hashtbl.find e.loc s in
+
+          incr it_counter;
+          Format.printf "@.Iteration %d: q%d@." !it_counter s;
+
+          let start = loc.v in
+          let f i =
+            (*Format.printf "I: %a@." print_v i;*)
+            let i' = set_target_case e i loc.def_cl in
+            (*Format.printf "I': %a@." print_v i';*)
+            let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in
+            (*Format.printf "J: %a@." print_v j;*)
+            j
+          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 ND.is_bot fi_num then
+                i_enum, i_num
+              else
+                if n < e.opt.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
+          Format.printf "Fixpoint: %a@." print_v z;
+
+          loc.v <- z;
+
+          Hashtbl.iter
+            (fun t loc2 ->
+                let u = pass_cycle e.ve z in
+                let v = apply_cl u loc2.def_cl in
+                let w = apply_cl v loc2.cl in
+                (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
+                let r_enum, r_num = w in
+                if not (is_bot (r_enum, r_num)) then begin
+                  Format.printf "%d -> %d with:@.  %a@." s t print_v (r_enum, r_num);
+                  if not (List.mem s loc2.in_t)
+                    then loc2.in_t <- s::loc2.in_t;
+                  if not (List.mem t loc.out_t)
+                    then loc.out_t <- t::loc.out_t;
+                  let enum, num = loc2.v in
+                  let enum2, num2 = join (enum, num) (r_enum, r_num) in
+                  if not (ED.subset enum2 enum) || not (ND.subset num2 num) then
+                  begin
+                    loc2.v <- (enum2, num2);
+                    if not (List.mem t !delta)
+                      then delta := t::!delta
+                  end
+                end)
+            e.loc;
+
+          delta := List.filter ((<>) s) !delta;
+        done
+
+
+    let print_locs e =
+        Hashtbl.iter
+          (fun id loc ->
+            Format.printf "@.";
+            Format.printf "q%d: @[<hov 4>[ %a ]@]@." id
+              (print_list Formula_printer.print_expr " ∧ ") loc.def;
+            (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*)
+            Format.printf "    @[<hv 0>%a ∧@ %a@]@."
+              ED.print (fst loc.v) ND.print (snd loc.v);
+            Format.printf " -> @[<hov>[%a]@]@."
+              (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
+            )
+          e.loc
+
+    let do_prog opt rp =
+        let e = init_env opt rp in
+
+        Format.printf "@.Initializing.@.";
+        chaotic_iter e;
+        print_locs e
+
+end
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index a439995..23d4734 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -557,7 +557,8 @@ end = struct
             last_vars = [];
             all_vars = [];
             cycle = [];
-            forget = []; } in
+            forget = [];
+            forget_inv = []; } in
         Hashtbl.add ve.ev_order "x" 0;
         Hashtbl.add ve.ev_order "y" 1;
         Hashtbl.add ve.ev_order "z" 2;
@@ -755,13 +756,10 @@ end = struct
         let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
 
         let ef, nf = List.fold_left
-            (fun (ef, nf) (_, var, t) ->
-              if var.[0] <> 'N' then
-                match t with
-                | TEnum _ -> var::ef, nf
-                | TReal | TInt -> ef, var::nf
-              else ef, nf)
-            ([], []) env.rp.all_vars in
+            (fun (ef, nf) (var, t) -> match t with
+              | TEnum _ -> var::ef, nf
+              | TReal | TInt -> ef, var::nf)
+            ([], []) env.ve.forget_inv in
 
         let v = edd_forget_vars v ef in
         edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
@@ -779,8 +777,9 @@ end = struct
 
         (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
         (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
+        (* WHY THE **** AM I SHOUTING LIKE THAT ? *)
         let facts = get_root_true f in
-        let f, rp, _ = List.fold_left
+        let f, rp, repls = List.fold_left
           (fun (f, (rp : rooted_prog), repls) eq ->
             match eq with
             | BEnumCons(E_EQ, a, EIdent b)
@@ -802,8 +801,12 @@ end = struct
                 let rp =
                   { rp with all_vars =
                       List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
-                let repls = (repl, keep)::
-                  (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
+                let repls = (repl, keep; "L"^repl, "L"^keep)::
+                  (List.map
+                    (fun (r, k) -> r,
+                      if k = repl then keep else
+                      if k = "L"^repl then "L"^keep else k)
+                    repls) in
                 f, rp, repls
               end
             | _ -> f, rp, repls)
@@ -825,6 +828,9 @@ end = struct
         Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
 
         let guarantees = Transform.guarantees_of_prog rp in
+        let guarantees = List.map
+          (fun (id, f) -> id, formula_replace_evars repls f)
+          guarantees in
         Format.printf "Guarantees:@.";
         List.iter (fun (id, f) ->
             Format.printf "  %s: %a@." id Formula_printer.print_expr f)
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index ea2b053..4f6aacd 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -11,11 +11,15 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
 
     (* construction *)
     val top           : (id * item list) list -> t
+    val bottom        : (id * item list) list -> t
+    val vtop          : t -> t  (* top with same vars *)
+    val is_bot        : t -> bool
 
     (* variable management *)
     val vars          : t -> (id * item list) list
 
     val forgetvar     : t -> id -> t
+    val forgetvars    : t -> id list -> t
     val project       : t -> id -> item list
 
     (* set-theoretic operations *)
@@ -27,6 +31,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
 
     (* abstract operations *)
     val apply_cons    : t -> enum_cons -> t list (* may disjunct *)
+    val apply_cl      : t -> enum_cons list -> t (* join any disjunction ; may raise Bot *)
     val assign        : t -> (id * id) list -> t
 
     (* pretty-printing *)
@@ -47,11 +52,15 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
     }
 
     let top vars = { vars; value = VarMap.empty }
+    let vtop x = { x with value = VarMap.empty }
+    let bottom vars = raise Bot  (* we don't represent Bot *)
+    let is_bot x = false
 
     let vars x = x.vars
 
     let forgetvar x id =
         { x with value = VarMap.remove id x.value }
+    let forgetvars = List.fold_left forgetvar
     let project x id =
         try [VarMap.find id x.value]
         with Not_found -> List.assoc id x.vars
@@ -108,7 +117,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
               (List.filter (cc op s) (List.assoc id2 x.vars))
           | Some s, Some t ->
             if cc op s t then [x] else []
-    
+
+    let apply_cl x l =
+      List.fold_left
+        (fun k c -> match apply_cons k c with
+          | [] -> raise Bot
+          | p::q -> List.fold_left join p q )
+        x l
+   
     let assign x idl =
         let v = List.fold_left
             (fun v (id, id2) ->
@@ -163,11 +179,15 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
     let uniq x = uniq_sorted (sort x)
 
     let top vars = { vars; value = VarMap.empty }
+    let vtop x = { x with value = VarMap.empty }
+    let bottom vars = raise Bot  (* we don't represent Bot *)
+    let is_bot x = false
 
     let vars x = x.vars
 
     let forgetvar x id =
         { x with value = VarMap.remove id x.value }
+    let forgetvars = List.fold_left forgetvar
     let project x id =
         try VarMap.find id x.value
         with Not_found -> List.assoc id x.vars
@@ -220,6 +240,13 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
                 | [] -> l
                 | _ -> { x with value = VarMap.add id2 v2 x.value }::l)
             [] v1
+
+    let apply_cl x l =
+      List.fold_left
+        (fun k c -> match apply_cons k c with
+          | [] -> raise Bot
+          | p::q -> List.fold_left join p q )
+        x l
     
     let assign x idl =
         let v = List.fold_left
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 47515eb..ae71b09 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -1,41 +1,10 @@
 open Ast
 open Formula
 open Util
+open Enum_domain
 
-module type ENUM_ENVIRONMENT_DOMAIN2 = sig
-    type t
 
-    type item = string
-
-    (* construction *)
-    val top           : (id * item list) list -> t
-    val bottom        : (id * item list) list -> t
-    val is_bot        : t -> bool
-
-    (* variable management *)
-    val vars          : t -> (id * item list) list
-
-    val forgetvar     : t -> id -> t
-    val forgetvars    : t -> id list -> t
-    val project       : t -> id -> item list
-
-    (* set-theoretic operations *)
-    val join          : t -> t -> t   (* union *)
-    val meet          : t -> t -> t   (* intersection *)
-
-    val subset        : t -> t -> bool
-    val eq            : t -> t -> bool
-
-    (* abstract operations *)
-    val apply_cons    : t -> enum_cons -> t
-    val apply_cl      : t -> enum_cons list -> t
-    val assign        : t -> (id * id) list -> t
-
-    (* pretty-printing *)
-    val print         : Format.formatter -> t -> unit
-end
-
-module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
+module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
     exception Top
 
     type item = string
@@ -173,6 +142,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
 
     let bottom vars = let t = top vars in { t with root = DBot }
 
+    let vtop x = { x with root = DTop }
+
     (*
       is_bot : t -> bool
     *)
@@ -284,7 +255,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
       apply_cl : t -> enum_cons list -> t
     *)
     let apply_cons v x =
-      meet v (of_cons v x)
+      let v = meet v (of_cons v x) in
+      if v.root = DBot then [] else [v]
 
     let apply_cl v ec =
         let rec cl_k = function
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 8bd3971..450bef3 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -20,6 +20,7 @@ type varenv = {
 
     cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
     forget        : (id * typ) list;          (* s'(x) not specified *)
+    forget_inv    : (id * typ) list;
 }
 
 
@@ -267,7 +268,12 @@ let mk_varenv (rp : rooted_prog) f cl =
       [] last_vars
     in
     let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
+    let forget_inv = List.map (fun (_, id, ty) -> (id, ty))
+      (List.filter
+        (fun (_, id, _) ->
+          not (List.exists (fun (_, b, _) -> b = id) cycle))
+        all_vars) in
 
     { evars = enum_vars; nvars = num_vars; ev_order;
-      last_vars; all_vars; cycle; forget }
+      last_vars; all_vars; cycle; forget; forget_inv }
 
diff --git a/main.ml b/main.ml
index e114554..339a433 100644
--- a/main.ml
+++ b/main.ml
@@ -7,6 +7,7 @@ open Nonrelational
 open Apron_domain
 
 open Enum_domain_edd
+open Abs_interp_dynpart
 
 module Interpret = Interpret.I
 
@@ -18,6 +19,9 @@ module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
 module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
 
+module AI_S_Itv_DP = Abs_interp_dynpart.I
+      (Enum_domain.MultiValuation)(ItvND)
+
 (* command line options *)
 let times = ref false
 let dump = ref false
@@ -28,6 +32,7 @@ let ai_itv = ref false
 let ai_rel = ref false
 let ai_itv_edd = ref false
 let ai_rel_edd = ref false
+let ai_s_itv_dp = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
@@ -40,22 +45,35 @@ let ifile = ref ""
 let usage = "usage: analyzer [options] file.scade"
 
 let options = [
-    "--exec-times", Arg.Set times, "Show time spent in each function of the analyzer, for some functions";
+    "--exec-times", Arg.Set times,
+        "Show time spent in each function of the analyzer, for some functions";
     "--dump", Arg.Set dump, "Dump program source.";
     "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
     "--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
     "--test", Arg.Set test, "Simple testing (direct interpret).";
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
     "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
-    "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain.";
-    "--ai-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain.";
-    "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
-    "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)";
-    "--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.";
+    "--ai-itv-edd", Arg.Set ai_itv_edd,
+        "Do abstract analysis using intervals and EDD disjunction domain.";
+    "--ai-rel-edd", Arg.Set ai_rel_edd,
+        "Do abstract analysis using Apron and EDD disjunction domain.";
+    "--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
+        "Do abstract analysis using dynamic partitionning method, "^
+        "with intervals and valuation domain for enums.";
+    "--ai-vci", Arg.Set ai_vci,
+        "Verbose chaotic iterations (show state at each iteration)";
+    "--ai-vvci", Arg.Set ai_vvci,
+        "Very verbose chaotic iterations (show everything all the time)";
+    "--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 =
@@ -106,7 +124,10 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin
+      if !ai_itv || !ai_rel
+          || !ai_itv_edd || !ai_rel_edd
+          || !ai_s_itv_dp then
+      begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
               if x = "all" then
@@ -138,6 +159,8 @@ let () =
           
           if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
           if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;
+
+          if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
index 7970aab..6468523 100644
--- a/tests/source/two_counters.scade
+++ b/tests/source/two_counters.scade
@@ -1,5 +1,5 @@
-const n1: int = 10;
-const n2: int = 6;
+const n1: int = 100;
+const n2: int = 60;
 
 
 node top(a,b,c : bool) returns (ok, r1, r2 : bool)
@@ -7,12 +7,12 @@ var
   x, y, pre_x, pre_y: int;
   o1, o2: bool;
 
-  m: bool;
+  m, n, lb: bool;
 let
   x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
   y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
-  o1= x = n1;
-  o2= y = n2;
+  o1= x >= n1;
+  o2= y >= n2;
   ok= if o1 then o2 else true;
   r1 = 0<=x and x<=n1;
   r2 = 0<=y and y<=n2;
@@ -20,6 +20,8 @@ let
   pre_y = 0 -> pre(y);
 
   m = true -> pre o2;
+  n = true -> pre o1;
+  lb = true -> pre b;
 
   guarantee g1: ok;
   guarantee g2: r1;