Merge branch 'e-last'

Conflicts:
	abstract/abs_interp.ml
	tests/source/counters.scade

1 files changed, 98 insertions, 96 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index f6ce0ab..cb5ae9c 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
@@ -170,6 +165,7 @@ end = struct
         rp          : rooted_prog;
         opt         : cmdline_opt;
 
+        all_vars    : (bool * id * typ) list;
         enum_vars   : (id * ED.item list) list;
         num_vars    : (id * bool) list;
 
@@ -181,7 +177,8 @@ end = struct
         (* abstract interpretation *)
         cycle       : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget      : (id * typ) list;          (* s'(x) not specified *)
-        d_vars      : id list;                  (* disjunction variables *)
+        d_vars      : id list;                  (* disjunction variables when calculating *)
+        acc_d_vars  : id list;                  (* disjunction variables in accumulator *)
         top         : case_v;
         env         : (case, case_v) Hashtbl.t;
         mutable delta : case list;
@@ -191,7 +188,7 @@ end = struct
     (*
       print_st : Formatter.t -> st -> unit
     *)
-    let print_st fmt st = print_aux fmt st.d_vars st.env
+    let print_st fmt st = print_aux fmt st.acc_d_vars st.env
 
     (*
       add_case : st -> case_v -> unit
@@ -223,29 +220,70 @@ end = struct
               | [en] -> aux en (v::vals) q
               | _ -> assert false)
             (ED.project enum p)
-      in aux enum [] st.d_vars
+      in aux enum [] st.acc_d_vars
 
+  
+    (*
+      dd_apply_cl : dd_v -> conslist -> dd_v
+    *)
+    let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) =
+        match r with
+        | CLTrue ->
+          let enums = List.fold_left
+            (fun enums ec -> List.flatten
+              (List.map (fun e -> ED.apply_cons e ec) enums))
+            [enum] ec in
+          let num = ND.apply_cl num nc in
+          List.map (fun ec -> ec, num) enums
+        | CLFalse -> []
+        | CLAnd(a, b) ->
+          let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in
+          List.flatten
+            (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs)
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @
+          apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb)
+
+    (*
+      pass_cycle : st -> case_v -> case_v
+    *)
+    let pass_cycle st (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)
+          ([], []) st.cycle in
+
+        let enum = ED.assign enum assign_e in
+        let num = ND.assign num assign_n in
+
+        List.fold_left
+            (fun (enum, num) (var, t) ->
+              let e, n = match t with
+              | TEnum _ -> ED.forgetvar enum var, num
+              | TReal | TInt -> enum, ND.forgetvar num var
+              in e, n)
+            (enum, num) st.forget
 
+    let dd_pass_cycle st (v : dd_v) =
+      let vv = dd_bot st.acc_d_vars in
+      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
+      vv
 
     (*
       init_state : int -> rooted_prog -> st
     *)
     let init_state opt rp =
-      Format.printf "Vars: @[<hov>%a@]@.@."
-          (print_list Ast_printer.print_typed_var ", ")
-          rp.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
+      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;
-      let init_cl = conslist_of_f init_f in
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
+      let init_cl = conslist_of_f init_f in
+      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 guarantees = Transform.guarantees_of_prog rp in
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
@@ -253,69 +291,58 @@ 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;
+      (* 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 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)
+        [] all_vars
       in
+      let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
       (* calculate disjunction variables *)
-      (* first approximation : use all enum variables appearing in init formula *)
-      let rec calculate_dvars (ec, _, r) =
-          let a = List.map (fun (_, id, _) -> id) ec in
-          let rec aux = function
-          | CLTrue | CLFalse -> []
-          | CLAnd(u, v) ->
-              aux u @ aux v
-          | CLOr(u, v) ->
-              calculate_dvars u @ calculate_dvars v
-          in a @ aux r
-      in
-      let d_vars_0 = calculate_dvars init_cl in
-      let d_vars_1 = List.filter
-          (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+      (* actually, don't calculate them, rely on user input *)
+      let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
           (List.map (fun (id, _) -> id) enum_vars) in
-      let d_vars = d_vars_0 @ d_vars_1 in
+      let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in 
 
       (* setup abstract data *)
       let top = ED.top enum_vars, ND.top num_vars in
       let delta = [] in
       let widen = Hashtbl.create 12 in
 
-      (* calculate initial state and environment *)
-      let init_s = dd_bot d_vars in
-
-      let init_ec, _, _ = init_cl in
-      let init_ed = List.fold_left
-          (fun ed cons ->
-            List.flatten (List.map (fun x -> ED.apply_cons x cons) ed))
-          [ED.top enum_vars] (init_ec) in
-      List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed;
-      let env_dd = apply_cl init_s init_cl in
-      let env = env_dd.data in
-      
       let st = 
-      { rp; opt; enum_vars; num_vars;
+      { rp; opt; enum_vars; num_vars; all_vars;
          cl; cl_g; guarantees;
-        cycle; forget; d_vars; top;
-        env; delta; widen } in
+        cycle; forget; acc_d_vars; d_vars; top;
+        env = Hashtbl.create 12; delta; widen } in
+
+      (* calculate initial state and environment *)
+      List.iter (fun ed -> add_case st (pass_cycle st ed))
+        (apply_cl_get_all_cases top init_cl);
 
       Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
 
@@ -323,30 +350,6 @@ end = struct
 
 
     (*
-      pass_cycle : st -> case_v -> case_v
-    *)
-    let pass_cycle st (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)
-          ([], []) st.cycle in
-
-        let enum = ED.assign enum assign_e in
-        let num = ND.assign num assign_n in
-
-        List.fold_left
-            (fun (enum, num) (var, t) -> match t with
-              | TEnum _ -> ED.forgetvar enum var, num
-              | TReal | TInt -> enum, ND.forgetvar num var)
-            (enum, num) st.forget
-
-    let dd_pass_cycle st (v : dd_v) =
-      let vv = dd_bot v.d_vars in
-      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
-      vv
-
-    (*
       cycle : st -> cl -> dd_v -> dd_v
     *)
     let cycle st cl env =
@@ -362,10 +365,10 @@ end = struct
     let set_target_case st env case =
       List.fold_left2
         (fun env id v ->
-          if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
-            dd_apply_econs env (E_EQ, "N"^id, EItem v)
+          if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+            dd_apply_econs env (E_EQ, id, EItem v)
           else env)
-        env st.d_vars case
+        env st.acc_d_vars case
 
     (*
       do_prog : rooted_prog -> unit
@@ -387,7 +390,7 @@ end = struct
             (print_list Formula_printer.print_id ", ") case;
         
         let start = try Hashtbl.find st.env case with Not_found -> assert false in
-        let start_dd = dd_singleton st.d_vars start in
+        let start_dd = dd_singleton st.acc_d_vars start in
         let f i =
           let i = dd_singleton st.d_vars i in
           let i' = set_target_case st i case in
@@ -422,7 +425,6 @@ end = struct
               Hashtbl.iter (fun _ q -> add_case st q) j.data)
             !cases;
 
-
         if st.opt.verbose_ci then
           Format.printf "-> @[<hov>%a@]@." print_st st;