Nice view of guarantees ; add half test, proved.

4 files changed, 120 insertions, 37 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index feaf037..d706f35 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -21,6 +21,9 @@ end = struct
         env         : E.t;
         f           : bool_expr;
         cl          : conslist;
+        f_g         : bool_expr;
+        cl_g        : conslist;
+        guarantees  : (id * bool_expr) list;
     }
 
 
@@ -73,8 +76,11 @@ end = struct
     let init_state widen_delay p root =
       let root_scope = get_root_scope p root in
 
-      let f = Formula.eliminate_not (Transform.f_of_prog p root) in
+      let f = Formula.eliminate_not (Transform.f_of_prog p root false) in
       let cl = Formula.conslist_of_f f in
+      let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in
+      let cl_g = Formula.conslist_of_f f_g in
+
       let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
       let env = List.fold_left
         (fun env (_, id, ty) ->
@@ -83,15 +89,25 @@ end = struct
         all_vars
       in
       let init_f = Transform.init_f_of_prog p root in
+      let guarantees = Transform.guarantees_of_prog p root in
 
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-      Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+      Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
 
       Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
 
+      Format.printf "Guarantees:@.";
+      List.iter (fun (id, f) ->
+          Format.printf "  %s: %a@." id Formula_printer.print_expr f)
+        guarantees;
+      Format.printf "@.";
+
       let env = E.apply_f env init_f in
 
-      { p; root_scope; widen_delay; f; cl; all_vars; env }
+      { p; root_scope; widen_delay;
+        f; cl; f_g; cl_g;
+        guarantees; all_vars; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -125,35 +141,36 @@ end = struct
       (pass_cycle st.all_vars (E.apply_cl i cl)) 
 
     (*
-      loop : st -> cl -> env -> env -> env
+      loop : st -> env -> env -> env
     *)
-    let loop st cycle_cl pnew stay =
+    let loop st pnew stay =
 
       Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
-        Formula_printer.print_conslist cycle_cl
+        Formula_printer.print_conslist st.cl
         E.print_all pnew E.print_all stay;
 
-      let add_stay = cycle st cycle_cl pnew in
+      let add_stay = cycle st st.cl pnew in
       let acc0 = E.join stay add_stay in
 
-      let fsharp i = 
+      let fsharp cl i = 
         Format.printf "Acc @[<hv>%a@]@." E.print_all i;
-        let j = cycle st cycle_cl i in
+        let j = cycle st cl i in
         E.join acc0 j
       in
 
       let rec iter n i =
         let i' =
           if n < st.widen_delay
-            then E.join i (fsharp i)
-            else E.widen i (fsharp i)
+            then E.join i (fsharp st.cl_g i)
+            else E.widen i (fsharp st.cl_g i)
         in
         if E.eq i i' then i else iter (n+1) i'
       in
 
       let x = iter 0 acc0 in
-      fix E.eq fsharp x   (* decreasing iteration *)
-
+      let y = fix E.eq (fsharp st.cl_g) x in    (* decreasing iteration *)
+      let z = E.apply_cl y st.cl in
+      y, z
 
     (*
       do_prog : prog -> id -> unit
@@ -163,16 +180,29 @@ end = struct
 
       let pnew = st.env in
 
-      let stay = loop st st.cl pnew (E.vbottom pnew) in
+      let stay, stay_c = loop st pnew (E.vbottom pnew) in
 
-      let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+      let final = E.join (E.apply_cl pnew st.cl) stay_c in
 
-      Format.printf "@[<hov>Final %a@]@."
+      Format.printf "@[<hov>Final %a@]@.@."
         E.print_all final;
 
-      Format.printf "Probes:@[<hov>";
+      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
+        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,"
+        if p then Format.printf " %a ∊ %a@ "
               Formula_printer.print_id id
               E.print_itv (E.var_itv final id))
         st.all_vars;
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index d13afd7..cef6b66 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -133,6 +133,7 @@ module D : ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print_all fmt x =
+        Abstract1.minimize manager x;
         Abstract1.print fmt x;
         Format.fprintf fmt "@?"
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 44495c4..f3c1df1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,15 +50,18 @@ and eliminate_not_negate = function
   | BBoolEq(id, v) -> BBoolEq(id, not v)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
-    let r' = match r with
-    | AST_EQ -> AST_NE
-    | AST_NE -> AST_EQ
-    | AST_LT -> AST_GE
-    | AST_LE -> AST_GT
-    | AST_GT -> AST_LE
-    | AST_GE -> AST_LT
-    in
-    BRel(r', a, b)
+    if r = AST_EQ then
+      BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b))
+    else
+      let r' = match r with
+      | AST_EQ -> AST_NE
+      | AST_NE -> AST_EQ
+      | AST_LT -> AST_GE
+      | AST_LE -> AST_GT
+      | AST_GT -> AST_LE
+      | AST_GE -> AST_LT
+      in
+      BRel(r', a, b)
   | BAnd(a, b) ->
     BOr(eliminate_not_negate a, eliminate_not_negate b)
   | BOr(a, b) ->
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 87da1bd..25e4b43 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,7 +18,6 @@ type transform_data = {
     (* future : the automata state *)
 }
 
-
 (* f_of_nexpr :
     transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
 *)
@@ -122,10 +121,13 @@ and f_of_expr td (node, prefix) expr =
     f_of_bexpr td (node, prefix) (fun x -> x) expr
   
 
-and f_of_scope active td (node, prefix, eqs) =
+(*
+    Translate program into one big formula
+*)
+let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
   let expr_eq e eq =
     let instance_eq (_, id, eqs, args) =
-      let eq = f_of_scope active td (node^"/"^id, "", eqs) in
+      let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
       if active then
         List.fold_left (fun eq ((_,argname,_), expr) ->
             let eq_arg = f_of_nexpr td (node, prefix) (function
@@ -177,7 +179,13 @@ and f_of_scope active td (node, prefix, eqs) =
       in
         expr_eq e assume_eq
     | AST_guarantee (_, e) ->
-      expr_eq e (BConst true)
+      let guarantee_eq =
+        if active && assume_guarantees then
+          f_of_expr td (node, prefix) e
+        else
+          BConst true
+      in
+        expr_eq e guarantee_eq
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b -> BConst true
@@ -187,7 +195,7 @@ and f_of_scope active td (node, prefix, eqs) =
       in
       let rec do_tree_act = function
         | AST_activate_body b ->
-            f_of_scope true td (node, b.act_id^".", b.body)
+            f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees
         | AST_activate_if(c, a, b) ->
           f_or
             (f_and (f_of_expr td (node, prefix) c)
@@ -196,7 +204,7 @@ and f_of_scope active td (node, prefix, eqs) =
               (f_and (do_tree_act b) (do_tree_inact a)))
       and do_tree_inact = function
         | AST_activate_body b ->
-          f_of_scope false td (node, b.act_id^".", b.body)
+          f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees
         | AST_activate_if(_, a, b) ->
           f_and (do_tree_inact a) (do_tree_inact b)
       in
@@ -216,17 +224,18 @@ and f_of_scope active td (node, prefix, eqs) =
     time_incr_eq
     (List.map do_eq eqs)
 
-and f_of_prog p root =
+and f_of_prog p root assume_guarantees =
     let td = {
       root_scope = get_root_scope p root;
       p = p;
       consts = I.consts p root;
     } in
 
-    f_of_scope true td td.root_scope
-
-
+    f_of_scope true td td.root_scope assume_guarantees
 
+(*
+    Translate init state into a formula
+*)
 let rec init_f_of_scope p (node, prefix, eqs) =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
@@ -258,3 +267,43 @@ let rec init_f_of_scope p (node, prefix, eqs) =
 
 and init_f_of_prog p root =
     init_f_of_scope p (get_root_scope p root)
+
+(*
+    Get expressions for guarantee violation
+*)
+let rec g_of_scope td (node, prefix, eqs) cond =
+  let expr_g e =
+    let instance_g (_, id, eqs, args) =
+        g_of_scope td (node^"/"^id, "", eqs) cond
+    in
+    List.fold_left (fun x i -> (instance_g i) @ x)
+      [] (extract_instances td.p e)
+  in
+  let do_eq eq = match fst eq with
+    | AST_assign(_, e) | AST_assume(_, e) ->
+        expr_g e
+    | AST_guarantee((id, _), e) ->
+        (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e)))
+          :: (expr_g e)
+    | AST_activate (b, _) ->
+      let rec cond_g cond = function
+        | AST_activate_body b ->
+          g_of_scope td (node, b.act_id^".", b.body) cond
+        | AST_activate_if(c, a, b) ->
+          (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @
+          (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @
+          (expr_g c)
+      in
+      cond_g cond b
+    | AST_automaton _ -> not_implemented "g_of_scope automaton"
+  in
+  List.fold_left (@) [] (List.map do_eq eqs)
+
+and guarantees_of_prog p root =
+    let td = {
+      root_scope = get_root_scope p root;
+      p = p;
+      consts = I.consts p root;
+    } in
+
+    g_of_scope td (get_root_scope p root) (BConst true)