Add heuristic...

5 files changed, 133 insertions, 41 deletions

diff --git a/.gitignore b/.gitignore
index d6413c0..5b727b1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,4 @@ analyze
 
 # Plots
 graphs/*
+graphs2/*
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 32ed890..006854e 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -35,6 +35,9 @@ end = struct
 
         mutable out_t   : int list;
         mutable in_t    : int list;
+
+        mutable verif_g   : id list;
+        mutable violate_g : id list;
     }
 
     type env = {
@@ -230,10 +233,12 @@ end = struct
             cl = conslist_of_f rstf;
 
             in_c = 0;
-            v = (ED.top ve.evars, ND.bottom ve.nvars);
+            v = bottom env;
 
             out_t = [];
             in_t = [];
+            verif_g = [];
+            violate_g = [];
           };
         Hashtbl.add env.loc 1
           {
@@ -246,10 +251,12 @@ end = struct
             cl = conslist_of_f nrstf;
 
             in_c = 0;
-            v = (ED.top ve.evars, ND.bottom ve.nvars);
+            v = bottom env;
 
             out_t = [];
             in_t = [];
+            verif_g = [];
+            violate_g = [];
           };
         env
 
@@ -321,13 +328,33 @@ end = struct
           (fun id loc ->
             Format.printf "@.";
             Format.printf "q%d (depth = %d):@.  D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
-            (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
+            Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;
             Format.printf "  V: %a@." print_v loc.v;
             Format.printf " -> @[<hov>[%a]@]@."
               (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
             )
           e.loc
 
+    let dump_graphwiz_trans_graph e file =
+        let o = open_out file in
+        let fmt = Format.formatter_of_out_channel o in
+        Format.fprintf fmt "digraph G{@[<v 4>@ ";
+
+        Hashtbl.iter
+          (fun id loc ->
+            if loc.is_init then
+              Format.fprintf fmt "q%d [shape=doublecircle, label=\"q%d [%a]\"];@ "
+                id id (print_list Format.pp_print_string ", ") loc.violate_g
+            else
+              Format.fprintf fmt "q%d [label=\"q%d [%a]\"];@ "
+                id id (print_list Format.pp_print_string ", ") loc.violate_g;
+            List.iter (fun v -> Format.fprintf fmt "q%d -> q%d;@ " id v) loc.out_t)
+          e.loc;
+
+        Format.fprintf fmt "@]@.}@.";
+        close_out o
+      
+
     (*
       chaotic_iter : env -> unit
 
@@ -432,6 +459,18 @@ end = struct
           e.loc;
         List.iter (Hashtbl.remove e.loc) !useless;
 
+        (* check which states verify/violate guarantees *)
+        Hashtbl.iter
+          (fun _ loc ->
+            let verif, violate = List.partition
+              (fun (_, f) ->
+                is_bot (apply_cl loc.v (conslist_of_f f)))
+              e.guarantees
+            in
+            loc.verif_g <- List.map fst verif;
+            loc.violate_g <- List.map fst violate)
+          e.loc;
+
         print_locs e
 
 
@@ -443,6 +482,7 @@ end = struct
           Format.printf "@.--------------@.Refinement #%d@." n;
 
           chaotic_iter e;
+          dump_graphwiz_trans_graph e (Format.sprintf "/tmp/part%03d.dot" n);
 
           let qc = ref None in
 
@@ -474,7 +514,7 @@ end = struct
           (* find splitting condition *)
           Hashtbl.iter
             (fun q (loc:location) ->
-              if !qc = None && loc.depth < e.opt.max_dp_depth then
+              if loc.depth < e.opt.max_dp_depth then
               let cs = ternary_conds loc.f in
               List.iter
                 (fun c ->
@@ -487,31 +527,46 @@ end = struct
                         (fun case -> not (is_bot (meet loc.v case)))
                         cases)
                       >= 2
-                  &&
-                    (List.exists
-                        (fun qi ->
-                          let loci = Hashtbl.find e.loc qi in
-                          let v = apply_cl
-                            (meet (pass_cycle e.ve loci.v) loc.def)
-                            loc.cl in
-                          List.exists
-                            (fun case -> is_bot (meet v case))
-                            cases)
-                        loc.in_t
-                    || List.exists
-                        (fun case ->
-                          let v = meet loc.v case in
-                          List.exists
-                            (fun qo ->
-                              let loco = Hashtbl.find e.loc qo in
-                              let w = apply_cl
-                                (meet (pass_cycle e.ve v) loco.def)
-                                loco.cl in
-                              is_bot w)
-                            loc.out_t)
-                        cases)
                   then
-                    qc := Some(q, c, cases_t, cases_f)
+                    let score =
+                      let w1 = List.fold_left (+.) 0.
+                        (List.map
+                          (fun qi ->
+                            let loci = Hashtbl.find e.loc qi in
+                            let v = apply_cl
+                              (meet (pass_cycle e.ve loci.v) loc.def)
+                              loc.cl in
+                            let n = List.length @@ List.filter
+                                (fun case -> is_bot (meet v case))
+                                cases
+                            in if n > 0 then 1. else 0.)
+                          loc.in_t)
+                      in
+                      let w2 = List.fold_left (+.) 0.
+                        (List.map
+                          (fun qo ->
+                            let loco = Hashtbl.find e.loc qo in
+                            let n = List.length @@ List.filter
+                              (fun case ->
+                                let v = meet loc.v case in
+                                let w = apply_cl
+                                  (meet (pass_cycle e.ve v) loco.def)
+                                  loco.cl
+                                in is_bot w)
+                              cases
+                            in if n > 0 then 1. else 0.)
+                          loc.out_t)
+                      in
+                      ((w1 /. 1. (*(float_of_int (List.length loc.in_t))*))
+                        +. (w2 /. 1. (*(float_of_int (List.length loc.out_t))*)))
+                      /. (float_of_int (List.length cases))
+                    in
+                    if
+                      match !qc with
+                      | None -> true
+                      | Some (s, _, _, _, _) -> score >= s
+                    then
+                      qc := Some(score, q, c, cases_t, cases_f)
                   )
                 cs
             )
@@ -521,7 +576,7 @@ end = struct
             match !qc with
             | None ->
               Format.printf "@.Found no more possible refinement.@.@."
-            | Some (q, c, cases_t, cases_f) ->
+            | Some (score, q, c, cases_t, cases_f) ->
               Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
                 (print_list print_v ", ") (cases_t@cases_f);
 
@@ -556,9 +611,9 @@ end = struct
             id Formula_printer.print_conslist cl;
           let violate = ref [] in
           Hashtbl.iter
-            (fun id loc ->
-              if not (is_bot (apply_cl loc.v cl)) then
-                violate := id::!violate)
+            (fun lid loc ->
+              if List.mem id loc.violate_g then
+                violate := lid::!violate)
             e.loc;
           if !violate = [] then
             Format.printf "OK"
@@ -571,9 +626,27 @@ end = struct
           Format.printf "Guarantee @[<v 0>";
           List.iter check_guarantee e.guarantees;
           Format.printf "@]@."
+        end;
+
+        (* Examine probes *)
+        if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin
+          let final =
+            Hashtbl.fold
+              (fun _ loc v -> join v loc.v)
+              e.loc (bottom e) in
+
+          Format.printf "Probes: @[<v 0>";
+          List.iter (fun (p, id, ty) ->
+            if p then match ty with
+            | TInt | TReal ->
+              Format.printf "%a ∊ %a@ " Formula_printer.print_id id
+                ND.print_itv (ND.project (snd final) id)
+            | TEnum _ -> Format.printf "%a : enum variable@ "
+                Formula_printer.print_id id)
+            e.ve.all_vars;
+          Format.printf "@]@."
         end
 
 
 
-
 end
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 23d4734..bff8e2b 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -971,9 +971,9 @@ end = struct
           List.iter (fun (p, id, ty) ->
             if p then match ty with
             | TInt | TReal ->
-              Format.printf "%a ∊ %a@." Formula_printer.print_id id
+              Format.printf "%a ∊ %a@ " Formula_printer.print_id id
                 ND.print_itv (ND.project final_flat id)
-            | TEnum _ -> Format.printf "%a : enum variable@."
+            | TEnum _ -> Format.printf "%a : enum variable@ "
                 Formula_printer.print_id id)
             e.ve.all_vars;
           Format.printf "@]@."
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 0144637..5fe4ed1 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -442,12 +442,14 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
                   (must_reset_c cr (fun _ -> false))
                   (BEnumCons(E_EQ, nstv, EItem st.st_name))
               | (c, (target, l), rst)::q ->
-                f_ternary
-                  (f_of_expr td (node, prefix, clock_scope) c)
-                  (f_and
-                    (BEnumCons(E_EQ, nstv, EItem target))
-                    (must_reset_c cr (fun i -> rst && i = target)))
-                  (aux q)
+                let c =  f_of_expr td (node, prefix, clock_scope) c in
+                let b1 = 
+                    f_and
+                      (BEnumCons(E_EQ, nstv, EItem target))
+                      (must_reset_c cr (fun i -> rst && i = target))
+                in
+                let b2 = aux q in
+                f_ternary c b1 b2
             in
             let trans_code = must_reset_c cnr (fun _ -> false) in
             let trans_code = f_and trans_code (aux st.until) in
diff --git a/tests/source/jeannet.scade b/tests/source/jeannet.scade
new file mode 100644
index 0000000..9fca060
--- /dev/null
+++ b/tests/source/jeannet.scade
@@ -0,0 +1,16 @@
+node test() returns(x, y, probe z: int; a, b: bool)
+var px, py: int;
+let
+  a = false -> pre b;
+  b = true -> not pre a;
+
+  px = pre x;
+  py = pre y;
+
+  x = 0 -> (if a = b then px + 1 else px);
+  y = 0 -> (if a = b then py else py + 1);
+
+  z = x - y;
+
+  guarantee g1: x >= y;
+tel