Cleanup.

4 files changed, 292 insertions, 241 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 1b3bb39..b80ca14 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -7,6 +7,7 @@ open Cmdline
 open Util
 open Num_domain
 
+open Varenv
 
 
 exception Top
@@ -25,18 +26,6 @@ end = struct
     (*  **********************
               EDD Domain  
         **********************  *)
-
-    type item = string
-
-    type evar = id * item list
-    type nvar = id * bool
-
-    type varenv = {
-        evars         : evar list;
-        nvars         : nvar list;
-        ev_order      : (id, int) Hashtbl.t;
-    }
-
     type edd =
         | DBot
         | DTop
@@ -564,7 +553,11 @@ end = struct
         let ve = {
             evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
             nvars = [];
-            ev_order = Hashtbl.create 2 } in
+            ev_order = Hashtbl.create 2;
+            last_vars = [];
+            all_vars = [];
+            cycle = [];
+            forget = []; } in
         Hashtbl.add ve.ev_order "x" 0;
         Hashtbl.add ve.ev_order "y" 1;
         Hashtbl.add ve.ev_order "z" 2;
@@ -590,8 +583,6 @@ end = struct
         rp            : rooted_prog;
         opt           : cmdline_opt;
 
-        last_vars     : (bool * id * typ) list;
-        all_vars      : (bool * id * typ) list;
         ve            : varenv;
 
         (* program expressions *)
@@ -599,10 +590,6 @@ end = struct
         cl            : conslist;
         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 *)
     }
 
 
@@ -736,7 +723,7 @@ end = struct
         { s with root = memo f s.root }
 
     (*
-      pass_cycle : env -> edd_v -> edd_v
+      pass_cycle : varenv -> edd_v -> edd_v
       unpass_cycle : env -> edd_v -> edd_v
     *)
     let pass_cycle env v =
@@ -763,7 +750,7 @@ end = struct
           (fun (ae, an) (a, b, t) -> match t with
             | TEnum _ -> (b, a)::ae, an
             | TInt | TReal -> ae, (b, NIdent a)::an)
-          ([], []) env.cycle in
+          ([], []) env.ve.cycle in
 
         let v = edd_eassign v assign_e in
         let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
@@ -780,145 +767,7 @@ end = struct
         let v = edd_forget_vars v ef in
         edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
 
-    (*
-      extract_linked_evars : conslist -> (id * id) list
-
-      Extract all pairs of enum-type variable (x, y) appearing in an
-      equation like x = y or x != y
-
-      A couple may appear several times in the result.
-    *)
-    let rec extract_linked_evars_root (ecl, _, r) =
-        let v_ecl = List.fold_left
-            (fun c (_, x, v) -> match v with
-                | EIdent y -> (x, y)::c
-                | _ -> c)
-            [] ecl
-        in
-        v_ecl
-
-    let rec extract_const_vars_root (ecl, _, _) =
-        List.fold_left
-          (fun l (_, x, v) -> match v with 
-                | EItem _ -> x::l
-                | _ -> l)
-          [] ecl
-
-    (*
-      scope_constrict : id list -> (id * id) list -> id list
-
-      Orders the variable in the first argument such as to minimize the
-      sum of the distance between the position of two variables appearing in
-      a couple of the second list. (minimisation is approximate, this is
-      an heuristic so that the EDD will not explode in size when expressing
-      equations such as x = y && u = v && a != b)
-    *)
-    let scope_constrict vars cp_id =
-        let var_i = Array.of_list vars in
-        let n = Array.length var_i in
-
-        let i_var = Hashtbl.create n in
-        Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
-
-        let cp_i = List.map
-          (fun (x, y) -> Hashtbl.find i_var x, Hashtbl.find i_var y)
-          cp_id in
-
-        let eval i =
-          let r = Array.make n (-1) in
-          Array.iteri (fun pos var -> r.(var) <- pos) i;
-          Array.iteri (fun _ x -> assert (x <> (-1))) r;
-          List.fold_left
-            (fun s (x, y) -> s + abs (r.(x) - r.(y)))
-            0 cp_i
-        in
-
-        let best = Array.init n (fun i -> i) in
-
-        let usefull = ref true in
-        Format.printf "SCA";
-        while !usefull do
-          Format.printf ".@?";
-
-          usefull := false;
-          let try_s x =
-            if eval x < eval best then begin
-              Array.blit x 0 best 0 n;
-              usefull := true
-            end
-          in
-
-          for i = 0 to n-1 do
-            let tt = Array.copy best in
-            (* move item i at beginning *)
-            let temp = tt.(i) in
-            for j = i downto 1 do tt.(j) <- tt.(j-1) done;
-            tt.(0) <- temp;
-            (* try all positions *)
-            try_s tt;
-            for j = 1 to n-1 do
-              let temp = tt.(j-1) in
-              tt.(j-1) <- tt.(j);
-              tt.(j) <- temp;
-              try_s tt
-            done
-          done
-        done;
-        Format.printf "@.";
-
-        Array.to_list (Array.map (Array.get var_i) best)
-
-    (*
-      force_ordering : id list -> (float * id list) list -> id list
-
-      Determine a good ordering for enumerate variables based on the FORCE algorithm
-    *)
-    let force_ordering vars groups =
-        let var_i = Array.of_list vars in
-        let n = Array.length var_i in
-
-        let i_var = Hashtbl.create n in
-        Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
-        Hashtbl.add i_var "#BEGIN" (-1);
-
-        let ngroups = List.map
-          (fun (w, l) -> w, List.map (Hashtbl.find i_var) l)
-          groups in
-
-        let ord = Array.init n (fun i -> i) in
-
-        for iter = 0 to 500 do
-            let rev = Array.make n (-1) in
-            for i = 0 to n-1 do rev.(ord.(i)) <- i done;
-
-            let bw = Array.make n 0. in
-            let w = Array.make n 0. in
 
-            let gfun (gw, l) =
-              let sp = List.fold_left (+.) 0.
-                (List.map
-                  (fun i -> if i = -1 then -.gw else float_of_int (rev.(i))) l)
-              in
-              let b = sp /. float_of_int (List.length l) in
-              List.iter (fun i -> if i >= 0 then begin
-                          bw.(i) <- bw.(i) +. (gw *. b);
-                          w.(i) <- w.(i) +. gw end)
-                  l 
-            in
-            List.iter gfun ngroups;
-
-            let b = Array.init n
-              (fun i ->
-                if w.(i) = 0. then
-                    float_of_int i
-                else bw.(i) /. w.(i)) in
-                    
-            let ol = List.sort
-              (fun i j -> Pervasives.compare b.(i) b.(j))
-              (Array.to_list ord) in
-            Array.blit (Array.of_list ol) 0 ord 0 n
-        done;
-        List.map (Array.get var_i) (Array.to_list ord)
 
     (*
       init_env : cmdline_opt -> rooted_prog -> env
@@ -941,81 +790,10 @@ end = struct
           guarantees;
         Format.printf "@.";
         
-        (* add variables from LASTs *)
-        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 ", ")
-            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)
-            ([], []) all_vars in
-
-
-        (* calculate order for enumerated variables *)
-        let evars = List.map fst enum_vars in
-
-        let lv = extract_linked_evars_root cl_g in
-        let lv = uniq_sorted
-             (List.sort Pervasives.compare (List.map ord_couple lv)) in
-
-        let lv_f = List.map (fun (a, b) -> (1.0, [a; b])) lv in
-        let lv_f = lv_f @ (List.map (fun v -> (10.0, ["#BEGIN"; v]))
-          (extract_const_vars_root cl)) in
-        let lv_f = lv_f @ (List.map (fun v -> (5.0, ["#BEGIN"; v]))
-          (List.filter (fun n -> is_suffix n "init") evars)) in
-        let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v]))
-          (List.filter (fun n -> is_suffix n "state") evars)) in
-        let lv_f = lv_f @
-          (List.map (fun v -> (0.7, [v; "L"^v]))
-            (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in
-        let evars_ord =
-          if true then
-            time "FORCE" (fun () -> force_ordering evars lv_f)
-          else
-            time "SCA" (fun () -> scope_constrict evars lv)
-        in
-
-        let evars_ord =
-          if false then
-            let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in
-            let vb, vc = List.partition (fun n -> is_suffix n "state") vb in
-            (List.rev va) @ vb @ vc
-          else
-            evars_ord
-        in
-
-        let ev_order = Hashtbl.create (List.length evars) in
-        List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
-        let ve = { evars = enum_vars; nvars = num_vars; ev_order } in
-
-        Format.printf "Order for variables: @[<hov>[%a]@]@."
-          (print_list Formula_printer.print_id ", ") evars_ord;
-
-        (* calculate cycle variables and forget variables *)
-        let cycle = List.fold_left
-          (fun q (_, id, ty) ->
-              if id.[0] = 'L' then
-                (id, String.sub id 1 (String.length id - 1), ty)::q
-              else q)
-          [] last_vars
-        in
-        let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
+        let ve = mk_varenv rp f_g cl_g in
 
 
-        { rp; opt; ve; last_vars; all_vars;
-          init_cl; cl; cl_g; guarantees;
-          cycle; forget }
+        { rp; opt; ve; init_cl; cl; cl_g; guarantees; }
 
           
 
@@ -1031,7 +809,7 @@ end = struct
             Format.printf "It. %d : full iteration.@." n;
 
             let d2 = edd_apply_cl x e.cl in
-            let dc = pass_cycle e d2 in
+            let dc = pass_cycle e.ve d2 in
             if dc.root = DBot then begin
               Format.printf "@.WARNING: contradictory hypotheses!@.@.";
               x
@@ -1064,7 +842,7 @@ end = struct
                 Format.printf "i %a@.i' %a@.j %a@."
                   edd_print i edd_print i' edd_print j;
 
-              let q = edd_join start (pass_cycle e j) in
+              let q = edd_join start (pass_cycle e.ve j) in
               edd_meet path q
             in
 
@@ -1082,7 +860,7 @@ end = struct
             let z = fix edd_eq f y in
 
 
-            let fj = pass_cycle e (edd_apply_cl z e.cl) in
+            let fj = pass_cycle e.ve (edd_apply_cl z e.cl) in
             if fj.root = DBot then begin
               Format.printf "@.WARNING: contradictory hypotheses!@.@.";
               x
@@ -1098,7 +876,7 @@ end = struct
 
         Format.printf "Calculating initial state...@.";
         let init_acc = edd_star_new (edd_bot e.ve)
-            (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in
+            (pass_cycle e.ve (edd_apply_cl (edd_top e.ve) e.init_cl)) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
@@ -1128,13 +906,13 @@ end = struct
         end;
 
         (* Examine probes *)
-        if List.exists (fun (p, _, _) -> p) e.all_vars then begin
+        if List.exists (fun (p, _, _) -> p) e.ve.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.all_vars) in
+              [] e.ve.all_vars) in
           let final_flat = match final_flat.root with
             | DTop -> ND.top e.ve.nvars
             | DBot -> ND.bottom e.ve.nvars
@@ -1150,7 +928,7 @@ end = struct
                 ND.print_itv (ND.project final_flat id)
             | TEnum _ -> Format.printf "%a : enum variable@."
                 Formula_printer.print_id id)
-            e.all_vars;
+            e.ve.all_vars;
           Format.printf "@]@."
         end
 
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index a372772..47515eb 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -9,7 +9,7 @@ module type ENUM_ENVIRONMENT_DOMAIN2 = sig
 
     (* construction *)
     val top           : (id * item list) list -> t
-    val bot           : (id * item list) list -> t
+    val bottom        : (id * item list) list -> t
     val is_bot        : t -> bool
 
     (* variable management *)
@@ -170,7 +170,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
         let order = Hashtbl.create 12 in
         List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
         { vars; order; root = DTop }
-    let bot vars = let t = top vars in { t with root = DBot }
+
+    let bottom vars = let t = top vars in { t with root = DBot }
 
     (*
       is_bot : t -> bool
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 480705f..e0f32c2 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -490,6 +490,26 @@ and f_of_prog rp assume_guarantees =
       f_and clock_eq scope_f
     in
       prog_init, prog_normal
+
+let f_of_prog_incl_init rp assume_guarantees =
+    let td = {
+      rp = rp;
+      consts = I.consts rp;
+    } in
+
+    let init_cond = BEnumCons(E_EQ, "L/must_reset", bool_true) in
+    let no_next_init_cond = BEnumCons(E_EQ, "/must_reset", bool_false) in
+
+    let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in
+
+    let scope_f = 
+      f_of_scope
+        true
+        td td.rp.root_scope
+        clock_scope
+        assume_guarantees in
+    f_and clock_eq (f_and no_next_init_cond scope_f)
+
       
 
 
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
new file mode 100644
index 0000000..1aa17b4
--- /dev/null
+++ b/abstract/varenv.ml
@@ -0,0 +1,252 @@
+open Ast
+open Util
+open Typing
+open Formula
+
+
+
+type item = string
+
+type evar = id * item list
+type nvar = id * bool
+
+type varenv = {
+    evars         : evar list;
+    nvars         : nvar list;
+    ev_order      : (id, int) Hashtbl.t;
+
+    last_vars     : (bool * id * typ) list;
+    all_vars      : (bool * id * typ) list;
+
+    cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
+    forget        : (id * typ) list;          (* s'(x) not specified *)
+}
+
+
+
+(*
+  extract_linked_evars : conslist -> (id * id) list
+
+  Extract all pairs of enum-type variable (x, y) appearing in an
+  equation like x = y or x != y
+
+  A couple may appear several times in the result.
+*)
+let rec extract_linked_evars_root (ecl, _, r) =
+    let v_ecl = List.fold_left
+        (fun c (_, x, v) -> match v with
+            | EIdent y -> (x, y)::c
+            | _ -> c)
+        [] ecl
+    in
+    v_ecl
+
+let rec extract_const_vars_root (ecl, _, _) =
+    List.fold_left
+      (fun l (_, x, v) -> match v with 
+            | EItem _ -> x::l
+            | _ -> l)
+      [] ecl
+
+
+
+(*
+  scope_constrict : id list -> (id * id) list -> id list
+
+  Orders the variable in the first argument such as to minimize the
+  sum of the distance between the position of two variables appearing in
+  a couple of the second list. (minimisation is approximate, this is
+  an heuristic so that the EDD will not explode in size when expressing
+  equations such as x = y && u = v && a != b)
+*)
+let scope_constrict vars cp_id =
+    let var_i = Array.of_list vars in
+    let n = Array.length var_i in
+
+    let i_var = Hashtbl.create n in
+    Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
+
+    let cp_i = List.map
+      (fun (x, y) -> Hashtbl.find i_var x, Hashtbl.find i_var y)
+      cp_id in
+
+    let eval i =
+      let r = Array.make n (-1) in
+      Array.iteri (fun pos var -> r.(var) <- pos) i;
+      Array.iteri (fun _ x -> assert (x <> (-1))) r;
+      List.fold_left
+        (fun s (x, y) -> s + abs (r.(x) - r.(y)))
+        0 cp_i
+    in
+
+    let best = Array.init n (fun i -> i) in
+
+    let usefull = ref true in
+    Format.printf "SCA";
+    while !usefull do
+      Format.printf ".@?";
+
+      usefull := false;
+      let try_s x =
+        if eval x < eval best then begin
+          Array.blit x 0 best 0 n;
+          usefull := true
+        end
+      in
+
+      for i = 0 to n-1 do
+        let tt = Array.copy best in
+        (* move item i at beginning *)
+        let temp = tt.(i) in
+        for j = i downto 1 do tt.(j) <- tt.(j-1) done;
+        tt.(0) <- temp;
+        (* try all positions *)
+        try_s tt;
+        for j = 1 to n-1 do
+          let temp = tt.(j-1) in
+          tt.(j-1) <- tt.(j);
+          tt.(j) <- temp;
+          try_s tt
+        done
+      done
+    done;
+    Format.printf "@.";
+
+    Array.to_list (Array.map (Array.get var_i) best)
+
+
+(*
+  force_ordering : id list -> (float * id list) list -> id list
+
+  Determine a good ordering for enumerate variables based on the FORCE algorithm
+*)
+let force_ordering vars groups =
+    let var_i = Array.of_list vars in
+    let n = Array.length var_i in
+
+    let i_var = Hashtbl.create n in
+    Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
+    Hashtbl.add i_var "#BEGIN" (-1);
+
+    let ngroups = List.map
+      (fun (w, l) -> w, List.map (Hashtbl.find i_var) l)
+      groups in
+
+    let ord = Array.init n (fun i -> i) in
+
+    for iter = 0 to 500 do
+        let rev = Array.make n (-1) in
+        for i = 0 to n-1 do rev.(ord.(i)) <- i done;
+
+        let bw = Array.make n 0. in
+        let w = Array.make n 0. in
+
+        let gfun (gw, l) =
+          let sp = List.fold_left (+.) 0.
+            (List.map
+              (fun i -> if i = -1 then -.gw else float_of_int (rev.(i))) l)
+          in
+          let b = sp /. float_of_int (List.length l) in
+          List.iter (fun i -> if i >= 0 then begin
+                      bw.(i) <- bw.(i) +. (gw *. b);
+                      w.(i) <- w.(i) +. gw end)
+              l 
+        in
+        List.iter gfun ngroups;
+
+        let b = Array.init n
+          (fun i ->
+            if w.(i) = 0. then
+                float_of_int i
+            else bw.(i) /. w.(i)) in
+                
+        let ol = List.sort
+          (fun i j -> Pervasives.compare b.(i) b.(j))
+          (Array.to_list ord) in
+        Array.blit (Array.of_list ol) 0 ord 0 n
+    done;
+    List.map (Array.get var_i) (Array.to_list ord)
+
+
+(*
+  Make varenv : takes a program, and extracts
+  - list of enum variables
+  - list of num variables
+  - good order for enum variables
+  - cycle, forget
+*)
+
+let mk_varenv (rp : rooted_prog) f cl =
+    (* add variables from LASTs *)
+    let last_vars = uniq_sorted 
+      (List.sort compare (Transform.extract_last_vars f)) 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 ", ")
+        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)
+        ([], []) all_vars in
+
+    (* calculate order for enumerated variables *)
+    let evars = List.map fst enum_vars in
+
+    let lv = extract_linked_evars_root cl in
+    let lv = uniq_sorted
+         (List.sort Pervasives.compare (List.map ord_couple lv)) in
+
+    let lv_f = List.map (fun (a, b) -> (1.0, [a; b])) lv in
+    let lv_f = lv_f @ (List.map (fun v -> (10.0, ["#BEGIN"; v]))
+      (extract_const_vars_root cl)) in
+    let lv_f = lv_f @ (List.map (fun v -> (5.0, ["#BEGIN"; v]))
+      (List.filter (fun n -> is_suffix n "init") evars)) in
+    let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v]))
+      (List.filter (fun n -> is_suffix n "state") evars)) in
+    let lv_f = lv_f @
+      (List.map (fun v -> (0.7, [v; "L"^v]))
+        (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in
+    let evars_ord =
+      if true then
+        time "FORCE" (fun () -> force_ordering evars lv_f)
+      else
+        time "SCA" (fun () -> scope_constrict evars lv)
+    in
+
+    let evars_ord =
+      if false then
+        let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in
+        let vb, vc = List.partition (fun n -> is_suffix n "state") vb in
+        (List.rev va) @ vb @ vc
+      else
+        evars_ord
+    in
+
+    let ev_order = Hashtbl.create (List.length evars) in
+    List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
+
+    Format.printf "Order for variables: @[<hov>[%a]@]@."
+      (print_list Formula_printer.print_id ", ") evars_ord;
+
+    (* calculate cycle variables and forget variables *)
+    let cycle = List.fold_left
+      (fun q (_, id, ty) ->
+          if id.[0] = 'L' then
+            (id, String.sub id 1 (String.length id - 1), ty)::q
+          else q)
+      [] last_vars
+    in
+    let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
+
+    { evars = enum_vars; nvars = num_vars; ev_order;
+      last_vars; all_vars; cycle; forget }
+