Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)

5 files changed, 144 insertions, 63 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index b80ca14..b139f9e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -775,6 +775,11 @@ end = struct
     let init_env opt rp =
         let init_f, f = Transform.f_of_prog rp false in
         let _, f_g = Transform.f_of_prog rp true in
+
+        let init_f = simplify_k (get_root_true init_f) init_f in
+        let f = simplify_k (get_root_true f) f in
+        let f_g = simplify_k (get_root_true f_g) f_g in
+
         Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f;
         Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 0045489..1882c85 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -48,6 +48,8 @@ type bool_expr =
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
+  | BTernary of bool_expr * bool_expr * bool_expr
+      (* (A and B) or ((not A) and C) *)
   | BNot of bool_expr
 
 let is_false = function
@@ -71,6 +73,11 @@ let f_or a b =
   else if is_false b then a
   else BOr(a, b)
 
+let f_ternary c a b =
+  if is_true c then a
+  else if is_false c then b
+  else BTernary(c, a, b)
+
 let f_e_op op a b = match a, b with
   | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
   | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
@@ -82,6 +89,8 @@ let rec eliminate_not = function
   | BNot e -> eliminate_not_negate e
   | BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b)
   | BOr(a, b) -> BOr(eliminate_not a, eliminate_not b)
+  | BTernary(c, a, b) ->
+    BTernary(eliminate_not c, eliminate_not a, eliminate_not b)
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
@@ -100,6 +109,7 @@ and eliminate_not_negate = function
       | AST_GE -> AST_LT
       in
       BRel(r', a, b, is_real)
+  | BTernary _ -> assert false
   | BAnd(a, b) ->
     BOr(eliminate_not_negate a, eliminate_not_negate b)
   | BOr(a, b) ->
@@ -159,4 +169,62 @@ let rec conslist_of_f = function
       | _, CLTrue -> econs, cons, ra
       | _, _ -> econs, cons, CLAnd(ra, rb)
     end
+  | BTernary(c, a, b) ->
+    conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
+
 
+
+(*
+  Simplify formula considering something is true
+*)
+
+let rec get_root_true = function
+  | BAnd(a, b) ->
+    get_root_true a @ get_root_true b
+  | BEnumCons e -> [BEnumCons e]
+  | BRel (a, b, c, d) -> [BRel (a, b, c, d)]
+  | _ -> []
+
+let rec simplify true_eqs e =
+  if List.exists
+      (fun f ->
+        try eliminate_not e = eliminate_not f with _ -> false)
+      true_eqs
+    then BConst true
+  else if List.exists
+      (fun f ->
+        match e, f with
+        | BEnumCons(E_EQ, a, EItem v), BEnumCons(E_EQ, b, EItem w)
+          when a = b && v <> w -> true
+        | _ -> try eliminate_not e = eliminate_not_negate f with _ -> false)
+      true_eqs
+    then BConst false
+  else
+    match e with
+    | BAnd(a, b) ->
+      f_and
+        (simplify true_eqs a)
+        (simplify true_eqs b)
+    | BOr(a, b) ->
+      f_or
+        (simplify true_eqs a)
+        (simplify true_eqs b)
+    | BTernary(c, a, b) ->
+      let c, a, b =
+        simplify true_eqs c,
+        simplify true_eqs a,
+        simplify true_eqs b in
+      begin match c with
+      | BConst true -> a
+      | BConst false -> b
+      | _ -> BTernary(c, a, b)
+      end
+    | BNot(n) ->
+      begin match simplify true_eqs n with
+      | BConst e -> BConst (not e)
+      | x -> BNot x
+      end
+    | v -> v
+    
+let rec simplify_k true_eqs e =
+  List.fold_left f_and (simplify true_eqs e) true_eqs
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 9c6c403..a5359a8 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -17,6 +17,7 @@ let ne_prec = function
   | _ -> 100
 
 let be_prec = function
+  | BTernary _ -> 10
   | BRel(op, _, _, _) -> binary_rel_precedence op
   | BAnd _ -> binary_bool_precedence AST_AND
   | BOr _ -> binary_bool_precedence AST_OR
@@ -97,11 +98,16 @@ let rec print_bool_expr fmt e = match e with
       if be_prec b < be_prec e || is_or b
         then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr b
         else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr b
-
   | BOr (a, b) ->
     print_ch fmt print_bool_expr be_prec a be_prec e;
     Format.fprintf fmt "@ ∨ ";
     print_ch fmt print_bool_expr be_prec b be_prec e
+  | BTernary(c, a, b) ->
+    print_ah fmt print_bool_expr be_prec c be_prec e;
+    Format.fprintf fmt "@ ? ";
+    print_ah fmt print_bool_expr be_prec a be_prec e;
+    Format.fprintf fmt "@ : ";
+    print_ah fmt print_bool_expr be_prec b be_prec e;
   | BNot (a) ->
     Format.pp_print_string fmt "¬";
     print_ch fmt print_bool_expr be_prec a be_prec e
diff --git a/abstract/transform.ml b/abstract/transform.ml
index e0f32c2..9bce192 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -88,25 +88,27 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
   | AST_arrow(a, b) ->
     if td.rp.init_scope clock_scope
     then
-      f_or
-        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
-          (sub where a))
-        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
-          (sub where b))
+      f_ternary
+          (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
+          (sub where a)
+          (sub where b)
     else if not (td.rp.no_time_scope clock_scope)
     then
-      f_or
-        (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false))
-          (sub where a))
-        (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
-          (sub where b))
-    else
+      f_ternary
+          (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
+          (sub where b)
+          (sub where a)
+    else begin
+      Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@."
+        clock_scope;
       f_or (sub where a) (sub where b)
+    end
   (* other *)
   | AST_if(c, a, b) ->
-    f_or
-      (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a))
-      (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b))
+    f_ternary
+      (f_of_expr td (node, prefix, clock_scope) c)
+      (sub where a)
+      (sub where b)
   | AST_instance ((f, _), args, nid) ->
     let (n, _) = find_node_decl td.rp.p f in
     where
@@ -125,11 +127,10 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
     in rl l []
   (* boolean values treated as enumerated types *)
   | _ when type_expr td.rp node expr = [bool_type] ->
-    f_or
-      (f_and (f_of_expr td (node, prefix, clock_scope) expr)
-        (where [EE (EItem bool_true)]))
-      (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr))
-        (where [EE (EItem bool_false)]))
+    f_ternary
+      (f_of_expr td (node, prefix, clock_scope) expr)
+      (where [EE (EItem bool_true)])
+      (where [EE (EItem bool_false)])
   | _ -> le type_error "Expected numerical/enumerated value"
 
 
@@ -167,20 +168,21 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
   | AST_arrow(a, b) ->
     if td.rp.init_scope clock_scope
     then
-      f_or
-        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
-          (sub where a))
-        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
-          (sub where b))
+      BTernary(
+        (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)),
+        (sub where a),
+        (sub where b))
     else if not (td.rp.no_time_scope clock_scope)
     then
-      f_or
-        (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false))
+      BTernary(
+        (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)),
+          (sub where b),
           (sub where a))
-        (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
-          (sub where b))
-    else
+    else begin
+      Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@."
+        clock_scope;
       f_or (sub where a) (sub where b)
+    end
   (* Enumerations... *)
   | _ when type_expr td.rp node expr = [bool_type] ->
     let ff = function
@@ -201,8 +203,6 @@ and f_of_expr td (node, prefix, clock_scope) expr =
 
 let reset_cond rst_exprs =
   List.fold_left f_or (BConst false) rst_exprs
-let no_reset_cond rst_exprs =
-  List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs
 
 let clock_scope_here (node, prefix, _) =
   node^"/"^prefix
@@ -228,7 +228,7 @@ let gen_clock td (node, prefix, _) active rst_exprs =
                   false)
               else BConst true)
             (if td.rp.init_scope clock_scope
-              then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false)
+              then BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
               else BConst true)
         else
           f_and
@@ -245,9 +245,10 @@ let gen_clock td (node, prefix, _) active rst_exprs =
     if rst_code = BConst true && no_rst_code = BConst true
       then BConst true
       else
-        f_or
-          (f_and (reset_cond rst_exprs) rst_code)
-          (f_and (no_reset_cond rst_exprs) no_rst_code)
+        f_ternary
+          (reset_cond rst_exprs)
+          rst_code
+          no_rst_code
   in
   (clock_scope, rst_exprs), clock_eq
 
@@ -338,11 +339,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
           f_and (f_of_expr td (node, prefix, clock_scope) e)
                 (BEnumCons(E_EQ, gn, EItem bool_true))
         else
-          f_or
-            (f_and (f_of_expr td (node, prefix, clock_scope) e)
-                (BEnumCons(E_EQ, gn, EItem bool_true)))
-            (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e))
-                (BEnumCons(E_EQ, gn, EItem bool_false)))
+          f_ternary
+            (f_of_expr td (node, prefix, clock_scope) e)
+            (BEnumCons(E_EQ, gn, EItem bool_true))
+            (BEnumCons(E_NE, gn, EItem bool_true))
       in
         f_and (expr_eq e) guarantee_eq
     | AST_activate (b, _) ->
@@ -358,11 +358,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
             let cs2, clock_eq = gen_clock td b_scope true rst_exprs in
             f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees)
         | AST_activate_if(c, a, b) ->
-          f_or
-            (f_and (f_of_expr td (node, prefix, clock_scope) c)
-              (f_and (do_tree_act a) (do_tree_inact b)))
-            (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c))
-              (f_and (do_tree_act b) (do_tree_inact a)))
+          f_ternary
+            (f_of_expr td (node, prefix, clock_scope) c)
+            (f_and (do_tree_act a) (do_tree_inact b))
+            (f_and (do_tree_act b) (do_tree_inact a))
       and do_tree_inact = function
         | AST_activate_body b ->
             let b_scope = node, b.act_id^".", b.body in
@@ -378,9 +377,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
       let nstv = node^"/"^aid^".next_state" in
       let stv = node^"/"^aid^".state" in
       let st_choice_eq =
-        f_or
-          (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name)))
-          (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
+        f_ternary
+          (reset_cond rst_exprs)
+          (f_e_eq (EIdent stv) (EItem init_st.st_name))
+          (f_e_eq (EIdent stv) (EIdent lnstv))
       in
 
       let rst_states = uniq_sorted @@ List.sort compare @@ List.flatten
@@ -427,12 +427,12 @@ 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_or
-                  (f_and (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))))
-                  (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux 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)
             in
             let trans_code = must_reset_c cnr (fun _ -> false) in
             let trans_code = f_and trans_code (aux st.until) in
@@ -441,10 +441,10 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
           if List.length states = 1 then
             act_eq
           else
-            f_or
-              (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
-              (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
-                (st_eq_inact (st, l)))
+            f_ternary
+              (BEnumCons(E_EQ, stv, EItem st.st_name))
+              act_eq
+              (st_eq_inact (st, l))
         in
         f_and st_choice_eq
           (f_and_list (List.map st_eq_act states))
@@ -497,8 +497,8 @@ let f_of_prog_incl_init rp assume_guarantees =
       consts = I.consts rp;
     } in
 
-    let init_cond = BEnumCons(E_EQ, "L/must_reset", bool_true) in
-    let no_next_init_cond = BEnumCons(E_EQ, "/must_reset", bool_false) in
+    let init_cond = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
+    let no_next_init_cond = BEnumCons(E_NE, "/must_reset", EItem bool_true) in
 
     let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in
 
@@ -573,6 +573,8 @@ let rec extract_last_vars = function
   | BAnd(a, b) | BOr (a, b) ->
     extract_last_vars a @ extract_last_vars b
   | BNot(e) -> extract_last_vars e
+  | BTernary(c, a, b) -> extract_last_vars c @ 
+      extract_last_vars a @ extract_last_vars b
   | _ -> []
 
 and elv_ne = function
diff --git a/main.ml b/main.ml
index d91d139..e114554 100644
--- a/main.ml
+++ b/main.ml
@@ -30,8 +30,8 @@ let ai_itv_edd = ref false
 let ai_rel_edd = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 5
-let ai_no_time_scopes = ref ""
-let ai_init_scopes = ref ""
+let ai_no_time_scopes = ref "all"
+let ai_init_scopes = ref "all"
 let ai_disj_v = ref ""
 let ai_vci = ref false
 let ai_vvci = ref false