Use LAST instead of NEXT (only EDD implementation works at the moment)

8 files changed, 189 insertions, 173 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3db657..26b788b 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -2,17 +2,12 @@ open Ast
 open Ast_util
 open Formula
 open Typing
+open Cmdline
 
 open Util
 open Num_domain
 open Enum_domain
 
-type cmdline_opt = {
-    widen_delay       : int;
-    disjunct          : (id -> bool);
-    verbose_ci        : bool;
-    vverbose_ci       : bool;
-}
 
 
 module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..c1fb905 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -2,10 +2,10 @@ open Ast
 open Ast_util
 open Formula
 open Typing
+open Cmdline
 
 open Util
 open Num_domain
-open Abs_interp
 
 
 
@@ -592,9 +592,12 @@ end = struct
         rp            : rooted_prog;
         opt           : cmdline_opt;
 
+        last_vars     : (bool * id * typ) list;
+        all_vars      : (bool * id * typ) list;
         ve            : varenv;
 
         (* program expressions *)
+        init_f        : bool_expr;
         cl            : conslist;
         cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
@@ -602,7 +605,6 @@ end = struct
         (* abstract interpretation *)
         cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget        : (id * typ) list;          (* s'(x) not specified *)
-        mutable data  : edd_v;
     }
 
 
@@ -924,20 +926,33 @@ end = struct
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     let init_env opt rp =
+        let init_f, f = Transform.f_of_prog rp false in
+        let _, f_g = Transform.f_of_prog rp true in
+        Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f;
+        Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+
+        let cl = Formula.conslist_of_f f in
+        let cl_g = Formula.conslist_of_f f_g in
+        Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+
+        let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in
+        let last_vars = List.map
+          (fun id ->
+            let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+              in false, id, ty)
+          last_vars in
+        let all_vars = last_vars @ rp.all_vars in
+
         Format.printf "Vars: @[<hov>%a@]@.@."
             (print_list Ast_printer.print_typed_var ", ")
-            rp.all_vars;
+            all_vars;
 
         let num_vars, enum_vars = List.fold_left
             (fun (nv, ev) (_, id, t) -> match t with
                 | TEnum ch -> nv, (id, ch)::ev
                 | TInt -> (id, false)::nv, ev
                 | TReal -> (id, true)::nv, ev)
-            ([], []) rp.all_vars in
-
-        let init_f = Transform.init_f_of_prog rp in
-        Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-        let init_cl = conslist_of_f init_f in
+            ([], []) all_vars in
 
         let guarantees = Transform.guarantees_of_prog rp in
         Format.printf "Guarantees:@.";
@@ -946,19 +961,10 @@ end = struct
           guarantees;
         Format.printf "@.";
 
-        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;
-
-        let cl = Formula.conslist_of_f f in
-        let cl_g = Formula.conslist_of_f f_g in
-        Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
-
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
 
-        let lv = extract_linked_evars_root init_cl
-            @ extract_linked_evars_root cl_g in
+        let lv = extract_linked_evars_root cl_g in
         let lv = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv)) in
 
@@ -995,25 +1001,17 @@ end = struct
         (* 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, ty)::q
+              if id.[0] = 'L' then
+                (id, String.sub id 1 (String.length id - 1), ty)::q
               else q)
-          [] rp.all_vars
-        in
-        let forget = List.map (fun (_, id, ty) -> (id, ty))
-            (List.filter
-              (fun (_, id, _) ->
-                not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
-              rp.all_vars)
+          [] last_vars
         in
+        let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
-        (* calculate initial environment *)
-        let data = edd_apply_cl (edd_top ve) init_cl in
-        Format.printf "Init: @[<hov>%a@]@." edd_print data;
 
-        { rp; opt; ve;
-          cl; cl_g; guarantees;
-          cycle; forget; data }
+        { rp; opt; ve; last_vars; all_vars;
+          init_f; cl; cl_g; guarantees;
+          cycle; forget }
 
           
 
@@ -1094,7 +1092,8 @@ end = struct
             end
         in
 
-        let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+        let init_acc = edd_star_new (edd_bot e.ve)
+            (pass_cycle e (edd_apply_cl (edd_top e.ve) (conslist_of_f e.init_f))) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
@@ -1124,13 +1123,13 @@ end = struct
         end;
 
         (* Examine probes *)
-        if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+        if List.exists (fun (p, _, _) -> p) e.all_vars then begin
           let final_flat = edd_forget_vars final
             (List.fold_left
               (fun l (_, id, ty) -> match ty with
                 | TInt | TReal -> l
                 | TEnum _ -> id::l)
-              [] e.rp.all_vars) in
+              [] e.all_vars) in
           let final_flat = match final_flat.root with
             | DTop -> ND.top e.ve.nvars
             | DBot -> ND.bottom e.ve.nvars
@@ -1146,7 +1145,7 @@ end = struct
                 ND.print_itv (ND.project final_flat id)
             | TEnum _ -> Format.printf "%a : enum variable@."
                 Formula_printer.print_id id)
-            e.rp.all_vars;
+            e.all_vars;
           Format.printf "@]@."
         end
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 01f6655..9c0ff71 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -51,7 +51,8 @@ type bool_expr =
   | BNot of bool_expr
 
 let f_and a b = match a, b with
-  | BConst false, _ | _, BConst false -> BConst false
+  | BConst false, _ | _, BConst false
+  | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false
   | BConst true, b -> b
   | a, BConst true -> a
   | a, b -> BAnd(a, b)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index dcb4049..1cbc27d 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,14 @@ open Typing
 open Interpret  (* used for constant evaluation ! *)
 
 
-(* Transform SCADE program to logical formula. *)
+(* Transform SCADE program to logical formula.
+
+    Convention : to access the last value of a variable,
+    access the variable with the same name prefixed by "L".
+    A pre-processing pass will extract the variables that are
+    referenced in such a way so that they are taken into
+    account when calculating the memory.
+*)
 
 (* node * prefix * equations *)
 type scope = id * id * eqn ext list
@@ -72,7 +79,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
     let typ = type_expr td.rp node expr in
       where
         (List.mapi
-          (fun i t -> let x = id^"."^(string_of_int i) in
+          (fun i t -> let x = "L"^id^"."^(string_of_int i) in
               match t with
               | TInt -> NE(NIdent x, false)
               | TReal -> NE(NIdent x, true)
@@ -190,40 +197,56 @@ and f_of_expr td (node, prefix, clock_scope) expr =
     Translate program into one big formula
 *)
 
+let reset_cond rst_exprs =
+  List.fold_left f_or (BConst false) rst_exprs
+let no_reset_cond rst_exprs =
+  List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs
+
 let clock_scope_here (node, prefix, _) =
   node^"/"^prefix
 
-let gen_clock td (node, prefix, _) active =
+let gen_clock td (node, prefix, _) active rst_exprs =
   let clock_scope = node^"/"^prefix in
   let clock_eq =
-    if active then
-      f_and
-        (if not (td.rp.no_time_scope clock_scope)
-          then BRel(AST_EQ, NIdent("N"^clock_scope^"time"),
-              NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false),
-              false)
-          else BConst true)
-        (if td.rp.init_scope clock_scope
-          then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false)
-          else BConst true)
-    else
-      f_and
-        (if not (td.rp.no_time_scope clock_scope)
-          then BRel(AST_EQ,
-              NIdent("N"^clock_scope^"time"),
-              NIdent(clock_scope^"time"), false)
-          else BConst true)
-        (if td.rp.init_scope clock_scope
-          then f_e_eq (EIdent("N"^clock_scope^"init"))
-                (EIdent (clock_scope^"init"))
-          else BConst true)
+    f_or
+      (f_and (reset_cond rst_exprs)
+        (f_and
+          (if not (td.rp.no_time_scope clock_scope)
+            then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)
+            else BConst true)
+          (if td.rp.init_scope clock_scope
+            then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
+            else BConst true)))
+      (f_and (no_reset_cond rst_exprs)
+        (if active then
+          f_and
+            (if not (td.rp.no_time_scope clock_scope)
+              then BRel(AST_EQ, NIdent(clock_scope^"time"),
+                  NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
+                  false)
+              else BConst true)
+            (if td.rp.init_scope clock_scope
+              then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false)
+              else BConst true)
+        else
+          f_and
+            (if not (td.rp.no_time_scope clock_scope)
+              then BRel(AST_EQ,
+                  NIdent(clock_scope^"time"),
+                  NIdent("L"^clock_scope^"time"), false)
+              else BConst true)
+            (if td.rp.init_scope clock_scope
+              then f_e_eq (EIdent(clock_scope^"init"))
+                    (EIdent ("L"^clock_scope^"init"))
+              else BConst true)))
   in
-  clock_scope, clock_eq
+  (clock_scope, rst_exprs), clock_eq
 
-let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
+let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
-      let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
+      let eq = f_of_scope active td (node^"/"^id, "", eqs)
+          cs assume_guarantees in
       if active then
         let arg_eq ((_,argname,ty), expr) =
             f_of_neexpr td (node, prefix, clock_scope) (function
@@ -247,7 +270,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
         f_of_neexpr td (node, prefix, clock_scope) (fun elist ->
             list_fold_op f_and
               (List.mapi
-                (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
+                (fun i v -> let x = (id^"."^(string_of_int i)) in
                   match v with
                   | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r)
                   | EE v -> f_e_eq (EIdent x) v)
@@ -257,11 +280,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
         let typ = type_expr td.rp node expr in
         list_fold_op f_and
           (List.mapi
-            (fun i t -> let x = string_of_int i in
+            (fun i t -> let id_x = id ^ "." ^ string_of_int i in
               match t with
-              | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false)
-              | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true)
-              | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
+              | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false)
+              | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true)
+              | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x)))
             typ)
     in
     let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
@@ -323,8 +346,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
       let rec do_tree_act = function
         | AST_activate_body b ->
             let b_scope = node, b.act_id^".", b.body in
-            let clock_scope, clock_eq = gen_clock td b_scope true in
-            f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees)
+            let cs2, clock_eq = gen_clock td b_scope true rst_exprs in
+            f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees)
         | AST_activate_if(c, a, b) ->
           f_or
             (f_and (f_of_expr td (node, prefix, clock_scope) c)
@@ -334,29 +357,37 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
       and do_tree_inact = function
         | AST_activate_body b ->
             let b_scope = node, b.act_id^".", b.body in
-            let clock_scope, clock_eq = gen_clock td b_scope false in
-            f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees)
+            let cs2, clock_eq = gen_clock td b_scope false rst_exprs in
+            f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees)
         | AST_activate_if(_, a, b) ->
           f_and (do_tree_inact a) (do_tree_inact b)
       in
         f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
     | AST_automaton (aid, states, _) ->
+      let (init_st, _) = List.find (fun (st, _) -> st.initial) states in
+      let lnstv = "L"^node^"/"^aid^".next_state" in
+      let nstv = node^"/"^aid^".next_state" in
       let stv = node^"/"^aid^".state" in
-      let nstv = "N"^node^"/"^aid^".state" in
+      let st_choice_eq =
+        f_or
+          (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name)))
+          (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
+      in
+
       let st_eq_inact (st, _) =
         let st_scope = node, aid^"."^st.st_name^".", st.body in
-        let clock_scope, clock_eq = gen_clock td st_scope false in
+        let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in
         f_and clock_eq
           (f_and
-            (f_of_scope false td st_scope clock_scope assume_guarantees)
+            (f_of_scope false td st_scope cs assume_guarantees)
             (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until)))
       in
       if active then
         let st_eq_act (st, l) =
           let act_eq =
             let st_scope = node, aid^"."^st.st_name^".", st.body in
-            let clock_scope, clock_eq = gen_clock td st_scope true in
-            let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in
+            let cs2, clock_eq = gen_clock td st_scope true rst_exprs in
+            let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in
             let rec aux = function
               | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
               | (c, (target, l), rst)::q ->
@@ -372,9 +403,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
             (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
               (st_eq_inact (st, l)))
         in
-        f_and_list (List.map st_eq_act states)
+        f_and st_choice_eq
+          (f_and_list (List.map st_eq_act states))
       else
-        f_and_list (List.map st_eq_inact states)
+        f_and st_choice_eq
+          (f_and_list (List.map st_eq_inact states))
   in
   f_and_list (List.map do_eq eqs)
 
@@ -384,77 +417,32 @@ and f_of_prog rp assume_guarantees =
       consts = I.consts rp;
     } in
 
-    let clock_scope, clock_eq = gen_clock td rp.root_scope true in
-
-    let scope_f = 
-      f_of_scope
-        true
-        td td.rp.root_scope
-        clock_scope
-        assume_guarantees in
-    f_and clock_eq scope_f
-      
+    let prog_normal =
+      let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in
 
-(*
-    Translate init state into a formula
-*)
-let gen_clock_init rp (node, prefix, _) =
-  let clock_scope = node^"/"^prefix in
-  let time_eq =
-    f_and
-      (if not (rp.no_time_scope clock_scope)
-        then
-          BRel(AST_EQ,
-            NIdent(clock_scope^"time"),
-            NIntConst 0, false)
-        else BConst true)
-      (if rp.init_scope clock_scope
-        then
-          f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
-        else BConst true)
-  in
-  clock_scope, time_eq
+      let scope_f = 
+        f_of_scope
+          true
+          td td.rp.root_scope
+          clock_scope
+          assume_guarantees in
+      f_and clock_eq scope_f
+    in
+    let prog_init =
+      let clock_scope, clock_eq =
+        gen_clock td rp.root_scope true [BConst true] in
 
-let rec init_f_of_scope rp (node, prefix, eqs) clock_scope =
-  let expr_eq e =
-    let instance_eq (_, id, eqs, args) =
-     init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope
+      let scope_f = 
+        f_of_scope
+          true
+          td td.rp.root_scope
+          clock_scope
+          assume_guarantees in
+      f_and clock_eq scope_f
     in
-    List.fold_left (fun x i -> f_and (instance_eq i) x)
-      (BConst true) (extract_instances rp.p e)
-  in
-  let do_eq eq = match fst eq with
-    | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
-        expr_eq e
-    | AST_activate (b, _) ->
-      let rec cond_eq = function
-        | AST_activate_body b ->
-          let bscope = (node, b.act_id^".", b.body) in
-          let clock_scope, clock_eq = gen_clock_init rp bscope in
-          f_and clock_eq (init_f_of_scope rp bscope clock_scope)
-        | AST_activate_if(c, a, b) ->
-          f_and (expr_eq c)
-            (f_and (cond_eq a) (cond_eq b))
-      in
-      cond_eq b
-    | AST_automaton (aid, states, _) ->
-      let (st, _) = List.find (fun (st, _) -> st.initial) states in
-      let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
-      let state_eq (st, _) =
-        let sc_f =
-          let st_scope = (node, aid^"."^st.st_name^".", st.body) in
-          let clock_scope, clock_eq = gen_clock_init rp st_scope in
-          f_and clock_eq (init_f_of_scope rp st_scope clock_scope)
-        in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until
-      in
-      List.fold_left f_and init_eq
-        (List.map state_eq states)
-  in
-  f_and_list (List.map do_eq eqs)
+      prog_init, prog_normal
+      
 
-and init_f_of_prog rp =
-    let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in
-    f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope)
 
 (*
     Get expressions for guarantee violation
@@ -502,3 +490,30 @@ and guarantees_of_prog rp =
 
     g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true)
 
+
+
+(*
+    Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+  | BRel(_, a, b, _) ->
+      elv_ne a @ elv_ne b
+  | BEnumCons c ->
+      elv_ec c
+  | BAnd(a, b) | BOr (a, b) ->
+    extract_last_vars a @ extract_last_vars b
+  | BNot(e) -> extract_last_vars e
+  | _ -> []
+
+and elv_ne = function
+  | NIdent i when i.[0] = 'L' -> [i]
+  | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+  | NUnary (_, a, _) -> elv_ne a
+  | _ -> []
+
+and elv_ec (_, v, q) =
+  (if v.[0] = 'L' then [v] else []) @
+  (match q with
+    | EIdent i when i.[0] = 'L' -> [i]
+    | _ -> [])
diff --git a/cmdline.ml b/cmdline.ml
new file mode 100644
index 0000000..b8f8ea8
--- /dev/null
+++ b/cmdline.ml
@@ -0,0 +1,8 @@
+open Ast
+
+type cmdline_opt = {
+    widen_delay       : int;
+    disjunct          : (id -> bool);
+    verbose_ci        : bool;
+    vverbose_ci       : bool;
+}
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 2859230..d814bbe 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -129,15 +129,12 @@ let clock_vars rp (node, prefix, _) =
     let v =
       if not (rp.no_time_scope (node^"/"^prefix))
       then
-        [
-          false, node^"/"^prefix^"time", TInt;
-          false, "N"^node^"/"^prefix^"time", TInt]
+        [false, node^"/"^prefix^"time", TInt]
       else [] in
     let v =
       if rp.init_scope (node^"/"^prefix)
         then
-          (false, node^"/"^prefix^"init", bool_type)::
-          (false, "N"^node^"/"^prefix^"init", bool_type)::v
+          (false, node^"/"^prefix^"init", bool_type)::v
         else v in
     v
 
@@ -145,9 +142,7 @@ let clock_vars rp (node, prefix, _) =
     extract_all_vars : rooted_prog -> scope -> var list
 
     Extracts all variables with names given according to
-    naming convention used here and in transform.ml :
-    - pre variables are not prefixed by scope
-    - next values for variables are prefixed by capital N
+    naming convention used here and in transform.ml
 *)
 let rec extract_all_vars rp (node, prefix, eqs) n_vars =
     let vars_of_expr e =
@@ -162,12 +157,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
         (List.map
           (fun (id, expr) ->
               let id = node^"/"^id in
-              let vd =
-                List.mapi
-                  (fun i t -> false, id^"."^(string_of_int i), t)
-                  (type_expr_vl rp.p n_vars rp.const_vars node expr)
-              in
-              vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+              List.mapi
+                (fun i t -> false, id^"."^(string_of_int i), t)
+                (type_expr_vl rp.p n_vars rp.const_vars node expr))
           (extract_pre e))
     in
     let vars_of_eq e = match fst e with
@@ -206,14 +198,14 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
           let st_scope = (node, aid^"."^st.st_name^".", st.body) in
           let svars = vars_in_node node st.st_locals in
           (if st.i_rst || st.o_rst then
-            [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type]
+            [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
           else [])
           @ svars @ tvars @ clock_vars rp st_scope @
             extract_all_vars rp st_scope (tvars@n_vars)
         in
         let st_ids = List.map (fun (st, _) -> st.st_name) states in
         (false, node^"/"^aid^".state", TEnum st_ids)::
-        (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+        (false, node^"/"^aid^".next_state", TEnum st_ids)::
         (List.flatten (List.map do_state states))
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
@@ -247,6 +239,7 @@ let root_prog p root no_time_scope init_scope =
     let root_vars = vars_in_node "" (decls_of_node root_node) in
     let root_clock_vars = clock_vars rp root_scope in
 
-    { rp with all_vars = root_clock_vars @ root_vars @ extract_all_vars rp root_scope root_vars }
+    { rp with all_vars = root_clock_vars @
+            root_vars @ extract_all_vars rp root_scope root_vars }
 
 
diff --git a/libs/util.ml b/libs/util.ml
index 940fe3e..6e8dc59 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -13,7 +13,7 @@ let rec uniq_sorted = function
 
 (* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *)
 let rec list_fold_op op = function
-  | [] -> invalid_arg "list_fold_opt on empty list"
+  | [] -> invalid_arg "list_fold_op on empty list"
   | [a] -> a
   | x::q -> op x (list_fold_op op q)
 
diff --git a/main.ml b/main.ml
index 5e9f087..a02820c 100644
--- a/main.ml
+++ b/main.ml
@@ -1,16 +1,19 @@
+open Cmdline
+
 open Ast
 
 open Num_domain
 open Nonrelational
 open Apron_domain
-open Abs_interp
 
 module Interpret = Interpret.I
 
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
 
+(*
 module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
 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)
@@ -123,8 +126,10 @@ let () =
               vverbose_ci = !ai_vvci;
           } in
           
+          (*
           if !ai_itv then AI_Itv.do_prog opt rp;
           if !ai_rel then AI_Rel.do_prog opt rp;
+          *)
           
           if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
           if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;