New example ; minor fixes.

2 files changed, 12 insertions, 5 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
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 17fd064..480705f 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -143,6 +143,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
 and f_of_bexpr td (node, prefix, clock_scope) where expr =
   let sub = f_of_bexpr td (node, prefix, clock_scope) in
   let sub_id = sub (fun x -> x) in
+  let le = loc_error (snd expr) in
   match fst expr with
   | AST_bool_const b -> where (BConst b)
   | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b))
@@ -159,7 +160,8 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
               | AST_NE -> E_NE
               | _ -> type_error "Invalid operator on enumerated values."
             in f_e_op eop x y
-          | _ -> invalid_arity "Binary operator")
+          | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator."
+          | _ -> le invalid_arity "Binary operator")
         (AST_tuple [a; b], snd expr))
   (* Temporal *)
   | AST_arrow(a, b) ->
@@ -187,7 +189,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
       | _ -> assert false
     in
     f_of_neexpr td (node, prefix, clock_scope) ff expr
-  | _ -> type_error "Expected boolean value."
+  | _ -> le type_error "Expected boolean value."
 
 and f_of_expr td (node, prefix, clock_scope) expr =
     f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr