Fix non-termination issue in EDDs

3 files changed, 130 insertions, 75 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3b2d79..0db128f 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -174,9 +174,7 @@ end = struct
         num_vars    : (id * bool) list;
 
         (* program expressions *)
-        f           : bool_expr;
         cl          : conslist;
-        f_g         : bool_expr;
         cl_g        : conslist;
         guarantees  : (id * bool_expr) list;
 
@@ -237,14 +235,12 @@ end = struct
           (print_list Ast_printer.print_typed_var ", ")
           rp.all_vars;
 
-      let enum_vars = List.fold_left
-          (fun v (_, id, t) -> match t with
-              | TEnum ch -> (id, ch)::v | _ -> v)
-          [] rp.all_vars in
-      let num_vars = List.fold_left
-          (fun v (_, id, t) -> match t with
-              | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v)
-          [] rp.all_vars in
+      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
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
@@ -317,7 +313,7 @@ end = struct
       
       let st = 
       { rp; opt; enum_vars; num_vars;
-        f; cl; f_g; cl_g; guarantees;
+         cl; cl_g; guarantees;
         cycle; forget; d_vars; top;
         env; delta; widen } in
 
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6e45240..cdcdab2 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -125,6 +125,11 @@ end = struct
         let leaves, get_leaf = get_leaf_fun_st () in
         leaves, get_leaf (false, 0)
 
+    let rank ve = function
+        | DChoice(_, x, _) -> Hashtbl.find ve.ev_order x
+        | _ -> 10000000 (* HYPOTHESIS : program will never have more than
+                              that number of variables *)
+
     (*
       edd_print : Format.formatter -> edd_v -> unit
     *)
@@ -288,22 +293,14 @@ end = struct
                 la lb
             in
             dq va kl
-          | DChoice(_, va, la), DChoice(_, vb, lb) ->
-            let v, kl =
-              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
-              else
-                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
-            in
-            dq v kl
 
           | DTop, _ | _, DTop -> DTop
           | DBot, DBot -> DBot
 
-          | DChoice(_,va, la), _ ->
+          | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
             dq va kl
-          | _, DChoice(_, vb, lb) ->
+          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
 
@@ -314,6 +311,8 @@ end = struct
             get_leaf (Hashtbl.find a.leaves u)
           | DBot, DVal(v, _) ->
             get_leaf (Hashtbl.find b.leaves v)
+
+          | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
         in
           { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
 
@@ -331,22 +330,14 @@ end = struct
                 la lb
             in
             dq va kl
-          | DChoice(_, va, la), DChoice(_, vb, lb) ->
-            let v, kl =
-              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
-              else
-                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
-            in
-            dq v kl
 
           | DBot, _ | _, DBot -> DBot
           | DTop, DTop -> DTop
 
-          | DChoice(_, va, la), _ ->
+          | DChoice(_, va, la), _ when rank ve na < rank ve nb ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
             dq va kl
-          | _, DChoice(_, vb, lb) ->
+          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
 
@@ -357,6 +348,8 @@ end = struct
             get_leaf (Hashtbl.find a.leaves u)
           | DTop, DVal(v, _) ->
             get_leaf (Hashtbl.find b.leaves v)
+
+          | _ -> assert false (* see above *)
         in
           { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
 
@@ -456,6 +449,33 @@ end = struct
 
 
     (*
+      edd_subset : edd_v -> edd_v -> bool
+    *)
+    let edd_subset a b =
+        let rank = rank a.ve in
+        let f f_rec na nb =
+          match na, nb with
+          | DBot, _ -> true
+          | _, DTop -> true
+          | DTop, DBot -> false
+
+          | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i)
+          | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i)
+
+          | DVal(i, _), DVal(j, _) ->
+            ND.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+              la lb
+          | DChoice(_, va, la), _ when rank na < rank nb ->
+            List.for_all (fun (c, n) -> f_rec n nb) la
+          | _, DChoice(_, vb, lb) when rank na > rank nb ->
+            List.for_all (fun (c, n) -> f_rec na n) lb
+          | _ -> assert false
+        in memo2 f a.root b.root
+
+    (*
       edd_forget_vars : edd_v -> id list -> edd_v
     *)
     let edd_forget_vars v vars =
@@ -566,9 +586,7 @@ end = struct
         ve            : varenv;
 
         (* program expressions *)
-        f             : bool_expr;
         cl            : conslist;
-        f_g           : bool_expr;
         cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
 
@@ -604,7 +622,7 @@ end = struct
     (*
       edd_join_widen : edd_v -> edd_v -> edd_v
     *)
-    let edd_join_widen (a:edd_v) (b:edd_v) =
+    let edd_widen (a:edd_v) (b:edd_v) =
         let ve = a.ve in
         let leaves, get_leaf = get_leaf_fun () in
         let dq = new_node_fun () in
@@ -621,14 +639,6 @@ end = struct
                 la lb
             in
             dq va kl
-          | DChoice(_, va, la), DChoice(_, vb, lb) ->
-            let v, kl =
-              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
-              else
-                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
-            in
-            dq v kl
 
           | DBot, DVal (i, _) ->
               get_leaf (Hashtbl.find b.leaves i)
@@ -643,21 +653,23 @@ end = struct
                  (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
             get_leaf x
 
-          | DChoice(_,va, la), _ ->
+          | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
             dq va kl
-          | _, DChoice(_, vb, lb) ->
+          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
+
+          | _ -> assert false
         in
         { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
 
     (*
-      edd_join_star : edd_v -> edd_v -> edd_v
+      edd_accumulate : edd_v -> edd_v -> edd_v
 
-      Star in A all things that are in B and not in A.
+      Sometimes do global widening.
     *)
-    let edd_join_star_widen env (a:edd_v) (b:edd_v) =
+    let edd_accumulate 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
@@ -674,14 +686,6 @@ end = struct
                 la lb
             in
             dq va kl
-          | DChoice(_, va, la), DChoice(_, vb, lb) ->
-            let v, kl =
-              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
-              else
-                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
-            in
-            dq v kl
 
           | DBot, DVal (i, _) ->
               get_leaf (true, 0) (Hashtbl.find b.leaves i)
@@ -690,23 +694,39 @@ end = struct
           | 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 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
+            get_leaf (s1, i1 + 1) x
 
-          | DChoice(_,va, la), _ ->
+          | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
             dq va kl
-          | _, DChoice(_, vb, lb) ->
+          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
+
+          | _ -> assert false
         in
         { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
 
     (*
+      edd_star_new : edd_v -> edd_v -> edd_v
+
+      Star in s leaves that were not present in s0
+    *)
+    let edd_star_new s0 s =
+        let f f_rec = function
+          | DChoice(n, x, l) ->
+            DChoice(n, x, List.map (fun (c, x) -> c, f_rec x) l)
+          | DVal(i, (false, n)) when
+              not (edd_subset (edd_meet (edd_extract_path s i) s) s0)
+            ->
+              DVal(i, (true, n))
+          | x -> x
+        in
+        { s with root = memo f s.root }
+
+    (*
       pass_cycle : env -> edd_v -> edd_v
       unpass_cycle : env -> edd_v -> edd_v
     *)
@@ -842,14 +862,12 @@ end = struct
             (print_list Ast_printer.print_typed_var ", ")
             rp.all_vars;
 
-        let enum_vars = List.fold_left
-            (fun v (_, id, t) -> match t with
-                | TEnum ch -> (id, ch)::v | _ -> v)
-            [] rp.all_vars in
-        let num_vars = List.fold_left
-            (fun v (_, id, t) -> match t with
-                | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v)
-            [] rp.all_vars in
+        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
         Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
@@ -868,6 +886,7 @@ end = struct
 
         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;
 
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
@@ -909,7 +928,7 @@ end = struct
         Format.printf "Init: @[<hov>%a@]@." edd_print data;
 
         { rp; opt; ve;
-          f; cl; f_g; cl_g; guarantees;
+          cl; cl_g; guarantees;
           cycle; forget; data }
 
           
@@ -927,7 +946,7 @@ end = struct
 
             let d2 = edd_apply_cl x e.cl in
             let dc = pass_cycle e d2 in
-            let y = edd_join_star_widen e x dc in
+            let y = edd_star_new x (edd_accumulate e x dc) in
 
             if e.opt.vverbose_ci then
               Format.printf "d2 %a@. dc %a@. y %a@."
@@ -965,7 +984,7 @@ end = struct
                 if n < e.opt.widen_delay then
                   edd_join i fi
                 else
-                  edd_join_widen i fi
+                  edd_widen i fi
               in
               if edd_eq i j then j else iter (n+1) j
             in
@@ -973,8 +992,8 @@ end = struct
             let z = fix edd_eq f y in
 
 
-            let j = pass_cycle e (edd_apply_cl z e.cl) in
-            let r = edd_join_star_widen e x j in
+            let fj = pass_cycle e (edd_apply_cl z e.cl) in
+            let r = edd_star_new x (edd_accumulate e x fj) in
 
             if e.opt.verbose_ci then
               Format.printf " -> %a@." edd_print r;
@@ -982,7 +1001,7 @@ end = struct
             ch_it (n+1) r
         in
 
-        let init_acc = edd_join_star_widen e (edd_bot e.data.ve) e.data in
+        let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
new file mode 100644
index 0000000..73d111a
--- /dev/null
+++ b/tests/source/updown2.scade
@@ -0,0 +1,40 @@
+const bound: int = 7;
+
+node updown() returns(probe x, probe y, probe z: int)
+var last_x, last_y: int;
+let
+    last_x = 0 -> pre x;
+    automaton
+        initial state UP
+        let x = last_x + 1; tel
+        until if x >= bound resume DOWN;
+
+        state DOWN
+        let x = last_x - 1; tel
+        until if x <= -bound resume UP;
+
+    returns x;
+    guarantee x_bounded: x >= -bound and x <= bound;
+
+    last_y = 0 -> pre y;
+    automaton
+        initial state DOWN
+        let y = last_y - 1; tel
+        until if y <= -bound resume UP;
+
+        state UP
+        let y = last_y + 1; tel
+        until if y >= bound resume DOWN;
+
+    returns y;
+    guarantee y_bounded: y >= -bound and y <= bound;
+
+    z = x + y;
+    guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+    exit = i >= 30;
+    a, b, c = updown2();
+tel