From ced4b9677189ea837e267678e9774584b81b087f Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 18 Jun 2014 18:21:27 +0200
Subject: Presentation changes.

---
 abstract/abs_interp.ml | 41 ++++++++++++++++++++++++++---------------
 1 file changed, 26 insertions(+), 15 deletions(-)

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index d706f35..00f7fad 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -179,33 +179,44 @@ end = struct
       let st = init_state widen_delay p root in
 
       let pnew = st.env in
+      let pnew_c = E.apply_cl pnew st.cl in
 
       let stay, stay_c = loop st pnew (E.vbottom pnew) in
 
-      let final = E.join (E.apply_cl pnew st.cl) stay_c in
+      Format.printf "@.@[<hov>New %a@]@.@."
+        E.print_all pnew_c;
+      Format.printf "@[<hov>Stay %a@]@.@."
+        E.print_all stay_c;
+
+      let final = E.join pnew_c stay_c in
 
       Format.printf "@[<hov>Final %a@]@.@."
         E.print_all final;
 
       let check_guarantee (id, f) =
-        Format.printf "@[<hv>%s:@ %a@ "
-          id Formula_printer.print_expr f;
-        let z = E.apply_f final (BAnd(f, st.f)) in
+        let cl = Formula.conslist_of_f f in
+        Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥  @ "
+          id Formula_printer.print_conslist cl;
+        let z = E.apply_cl final cl in
         if E.is_bot z then
           Format.printf "OK@]@ "
         else
           Format.printf "FAIL@]@ "
       in
-      Format.printf "Guarantees: @[<v 0>";
-      List.iter check_guarantee st.guarantees;
-      Format.printf "@]@.";
-
-      Format.printf "Probes:@[<v>";
-      List.iter (fun (p, id, _) ->
-        if p then Format.printf " %a ∊ %a@ "
-              Formula_printer.print_id id
-              E.print_itv (E.var_itv final id))
-        st.all_vars;
-      Format.printf "@]@."
+      if st.guarantees <> [] then begin
+        Format.printf "Guarantee @[<v 0>";
+        List.iter check_guarantee st.guarantees;
+        Format.printf "@]@."
+      end;
+
+      if List.exists (fun (p, _, _) -> p) st.all_vars then begin
+        Format.printf "Probes:@[<v>";
+        List.iter (fun (p, id, _) ->
+          if p then Format.printf " %a ∊ %a@ "
+                Formula_printer.print_id id
+                E.print_itv (E.var_itv final id))
+          st.all_vars;
+        Format.printf "@]@."
+      end
 
 end
-- 
cgit v1.2.3