New example ; minor fixes.

1 files changed, 8 insertions, 3 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index c1fb905..35bdbfb 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -597,7 +597,7 @@ end = struct
         ve            : varenv;
 
         (* program expressions *)
-        init_f        : bool_expr;
+        init_cl       : conslist;
         cl            : conslist;
         cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
@@ -933,6 +933,7 @@ end = struct
 
         let cl = Formula.conslist_of_f f in
         let cl_g = Formula.conslist_of_f f_g in
+        let init_cl = Formula.conslist_of_f init_f 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
@@ -975,6 +976,9 @@ end = struct
           (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)
@@ -1010,7 +1014,7 @@ end = struct
 
 
         { rp; opt; ve; last_vars; all_vars;
-          init_f; cl; cl_g; guarantees;
+          init_cl; cl; cl_g; guarantees;
           cycle; forget }
 
           
@@ -1092,8 +1096,9 @@ end = struct
             end
         in
 
+        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) (conslist_of_f e.init_f))) in
+            (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in