Finish up EDDs

4 files changed, 110 insertions, 44 deletions

diff --git a/.gitignore b/.gitignore
index e6c5390..4483b8c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,6 @@ analyze
 # Menhir automaton data
 *.conflicts
 *.automaton
+
+# Plots
+graphs/*
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 0dfc6f3..5b3b0ec 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -40,7 +40,7 @@ end = struct
     type edd =
         | DBot
         | DTop
-        | DVal of int * bool   (* bool : new case ? *)
+        | DVal of int * (bool * int)   (* bool*int : new case ? iterations before widen ? *)
         | DChoice of int * id * (item * edd) list
 
     type edd_v = {
@@ -122,7 +122,7 @@ end = struct
 
     let get_leaf_fun () =
         let leaves, get_leaf = get_leaf_fun_st () in
-        leaves, get_leaf false
+        leaves, get_leaf (false, 0)
 
     (*
       edd_print : Format.formatter -> edd_v -> unit
@@ -131,35 +131,62 @@ end = struct
         let max_n = ref 0 in
         let max_v = ref 0 in
 
-        let c_nodes = Hashtbl.create 12 in
-        let rec add = function
-            | DChoice(n, _, l) as x ->
-              if not (Hashtbl.mem c_nodes n) then begin
-                if n > !max_n then max_n := n;
-                Hashtbl.add c_nodes n x;
-                List.iter (fun (_, y) -> add y) l
-              end
-            | _ -> ()
-        in add v.root;
-
-        let print_n fmt = function
+        let print_nodes = Queue.create () in
+        let a = Hashtbl.create 12 in
+
+        let node_pc = Hashtbl.create 12 in
+        let f f_rec = function
+          | DChoice(_, _, l) ->
+            List.iter
+              (fun (_, c) -> match c with
+                  | DChoice(n, _, _) ->
+                      begin try Hashtbl.add node_pc n (Hashtbl.find node_pc n + 1)
+                      with Not_found -> Hashtbl.add node_pc n 1 end
+                  | _ -> ())
+            l;
+            List.iter (fun (_, c) -> f_rec c) l
+          | _ -> ()
+        in memo f v.root;
+
+        let rec print_n fmt = function
           | DBot -> Format.fprintf fmt "⊥";
           | DTop -> Format.fprintf fmt "⊤";
-          | DVal (i, s) -> if i > !max_v then max_v := i;
+          | DVal (i, (s, _)) -> if i > !max_v then max_v := i;
                     Format.fprintf fmt "v%d%s" i (if s then "*" else "");
-          | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
+          | DChoice(_, v, l) ->
+            match List.filter (fun (_, x) -> x <> DBot) l with
+            | [(c, nn)] ->
+              let aux fmt = function
+                | DChoice(nn, _, _) as i when Hashtbl.find node_pc nn >= 2 ->
+                  if Hashtbl.mem a nn then () else begin
+                    Queue.push i print_nodes;
+                    Hashtbl.add a nn ()
+                  end;
+                  Format.fprintf fmt "n%d" nn
+                | x -> print_n fmt x
+              in
+              Format.fprintf fmt "%a = %s,@ %a" Formula_printer.print_id v c aux nn
+            | _ ->
+              Format.fprintf fmt "%a ? " Formula_printer.print_id v;
+              let print_u fmt (c, i) =
+                Format.fprintf fmt "%s → " c;
+                match i with
+                | DChoice(nn, v, l) ->
+                  if Hashtbl.mem a nn then () else begin
+                    Queue.push i print_nodes;
+                    Hashtbl.add a nn ()
+                  end;
+                  Format.fprintf fmt "n%d" nn
+                | _ -> Format.fprintf fmt "%a" print_n i
+              in
+              Format.fprintf fmt "@[<h>%a@]" (print_list print_u ", ") l;
         in
-        Format.fprintf fmt "%a where:@." print_n v.root;
-
-        for id = !max_n downto 0 do
-          try match Hashtbl.find c_nodes id with
-              | DChoice (_, var, l) ->
-                let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
-                Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@."
-                    id Formula_printer.print_id var
-                    (print_list p ", ") l
-              | _ -> assert false
-          with Not_found -> ()
+        Format.fprintf fmt "@[<hov>%a@]@." print_n v.root;
+        while not (Queue.is_empty print_nodes) do
+          match Queue.pop print_nodes with
+          | DChoice(n, v, l) as x ->
+            Format.fprintf fmt "n%d: @[<hov>%a@]@." n print_n x
+          | _ -> assert false
         done;
 
         for id = 0 to !max_v do
@@ -168,6 +195,29 @@ end = struct
           with Not_found -> ()
         done
 
+    let edd_dump_graphviz v file =
+        let o = open_out file in
+        let fmt = Format.formatter_of_out_channel o in
+        Format.fprintf fmt "digraph G {@[<v 4>@,";
+
+        let f f_rec = function
+          | DChoice(n, v, x) ->
+            let aux fmt = function
+            | DBot -> Format.fprintf fmt "bot"
+            | DTop -> Format.fprintf fmt "top"
+            | DVal(i, _) -> Format.fprintf fmt "v%d" i
+            | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
+            in
+            Format.fprintf fmt "n%d [label=\"%s\"];@ " n v;
+            List.iter (fun (i, c) ->
+              if c <> DBot then Format.fprintf fmt "n%d -> %a [label=\"%s\"];@ " n aux c i;
+              f_rec c) x
+          | _ -> ()
+        in memo f v.root;
+        Format.fprintf fmt "@]}@.";
+
+        close_out o
+
 
     (*
       edd_bot : varenv -> edd_v
@@ -431,7 +481,7 @@ end = struct
                   let _, dv, cl = List.hd cn in
                   let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
                   let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
-                  let ch2 = List.map (fun i -> DVal (i, false)) fn in
+                  let ch2 = List.map (fun i -> DVal (i, (false, 0))) fn in
                   if List.mem dv vars then
                     (* Do union of all branches branching from nodes on variable dv *)
                     let ch3 = List.flatten
@@ -524,7 +574,7 @@ end = struct
     *)
     let edd_find_starred v =
         let f f_rec = function
-          | DVal (i, true) -> raise (Found_int i)
+          | DVal (i, (true, _)) -> raise (Found_int i)
           | DChoice(_, _, l) -> List.iter (fun (_, x) -> f_rec x) l
           | _ -> ()
         in
@@ -534,7 +584,7 @@ end = struct
     let edd_unstar v i =
         let f f_rec = function
           | DChoice(a, b, l) -> DChoice(a, b, List.map (fun (c, x) -> c, f_rec x) l)
-          | DVal(j, n) when i = j -> DVal(i, false)
+          | DVal(j, (s, n)) when i = j -> DVal(i, (false, n))
           | x -> x
         in
         { v with root = memo f v.root }
@@ -596,7 +646,7 @@ end = struct
 
       Star in A all things that are in B and not in A.
     *)
-    let edd_join_star (a:edd_v) (b:edd_v) =
+    let edd_join_star_widen env (a:edd_v) (b:edd_v) =
         let ve = a.ve in
         let leaves, get_leaf = get_leaf_fun_st () in
         let dq = new_node_fun () in
@@ -623,17 +673,18 @@ end = struct
             dq v kl
 
           | DBot, DVal (i, _) ->
-              get_leaf true (Hashtbl.find b.leaves i)
+              get_leaf (true, 0) (Hashtbl.find b.leaves i)
           | DVal (i, s), DBot ->
               get_leaf s (Hashtbl.find a.leaves i)
-          | DVal (u, s1), DVal (v, _) ->
+          | DVal (u, (s1, i1)), DVal (v, _) ->
             let p1, p2 = edd_extract_path a u, edd_extract_path b v in
             let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in
             let star = 
               s1 || not (edd_eq p1 p2) || not (ND.subset d2 d1)
             in
-            let x = ND.join d1 d2 in
-            get_leaf star x
+            let widen = edd_eq p1 p2 && i1 >= env.opt.widen_delay in
+            let x = (if widen then ND.widen else ND.join) d1 d2 in
+            get_leaf (star, i1 + 1) x
 
           | DChoice(_,va, la), _ ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
@@ -834,8 +885,6 @@ end = struct
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
 
-        let lv0 = List.map (fun x -> x, "N"^x)
-            (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in
         let lv1 = extract_linked_evars_root init_cl
             @ extract_linked_evars_root cl_g in
         let lv2 = extract_linked_evars init_cl @ extract_linked_evars cl_g in
@@ -844,7 +893,10 @@ end = struct
              (List.sort Pervasives.compare (List.map ord_couple lv1)) in
         let lv2 = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv2)) in
-        let evars_ord = List.rev @@  time "SCA" (fun () -> scope_constrict evars ( lv1 )) in
+        let evars_ord = time "SCA" (fun () -> scope_constrict evars ( lv1 )) in
+        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
+        let evars_ord = (List.rev va) @ vb @ vc in
 
         let ev_order = Hashtbl.create (List.length evars) in
         List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -884,13 +936,14 @@ end = struct
 
         (* Do iterations until fixpoint is reached *)
         let rec ch_it n x =
+          edd_dump_graphviz x (Format.sprintf "/tmp/graph-it%d.dot" n);
           match edd_find_starred x with
           | None ->
-            Format.printf "Chaotic iteration %d : full iteration.@." n;
+            Format.printf "It. %d : full iteration.@." n;
 
             let d2 = edd_apply_cl x e.cl in
             let dc = pass_cycle e d2 in
-            let y = edd_join_star x dc in
+            let y = edd_join_star_widen e x dc in
 
             if e.opt.verbose_ci then
               Format.printf " -> %a@." edd_print y;
@@ -900,7 +953,7 @@ end = struct
           | Some i ->
             let path = edd_extract_path x i in
             let x = edd_unstar x i in
-            Format.printf "Chaotic iteration %d: @[<hov>%a@]@." n edd_print path;
+            Format.printf "It. %d: @[<hov>%a@]@." n edd_print path;
 
             let path_target = unpass_cycle e path in
             let start = edd_meet path x in
@@ -927,7 +980,7 @@ end = struct
 
 
             let j = pass_cycle e (edd_apply_cl z e.cl) in
-            let r = edd_join_star x j in
+            let r = edd_join_star_widen e x j in
 
             if e.opt.verbose_ci then
               Format.printf " -> %a@." edd_print r;
@@ -935,12 +988,14 @@ end = struct
             ch_it (n+1) r
         in
 
-        let init_acc = edd_join_star (edd_bot e.data.ve) e.data in
+        let init_acc = edd_join_star_widen e (edd_bot e.data.ve) e.data in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
+        edd_dump_graphviz acc "/tmp/graph-final0.dot";
         Format.printf "Finishing up...@.";
         let final = edd_apply_cl acc e.cl in
+        edd_dump_graphviz final "/tmp/graph-final.dot";
         (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
 
         (* Check guarantees *)
diff --git a/libs/util.ml b/libs/util.ml
index 88b916f..940fe3e 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -80,6 +80,14 @@ let uid =
   fun () -> c := !c + 1; string_of_int !c
 
 
+(* String *)
+
+let is_suffix s sf =
+  let n = String.length s in
+  let k = String.length sf in
+  n >= k && sf = String.sub s (n-k) k
+
+
 (* Time heavy functions *)
 
 let times_k : (string, float) Hashtbl.t = Hashtbl.create 10
diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade
index 2b87278..9bfb6d2 100644
--- a/tests/source/limitera.scade
+++ b/tests/source/limitera.scade
@@ -4,7 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int)
     var s, r: int;
     let
         assume in_bounded: x >= -bound and x <= bound;
-        assume d_bounded: d = 16;
+        assume d_bounded: d >= 0 and d <= 16;
         guarantee out_bounded: y >= -bound and y <= bound;
         s = 0 -> pre y;
         r = x - s;