Correct some bugs on clocks.

3 files changed, 52 insertions, 30 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index b139f9e..56b366e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -588,7 +588,6 @@ end = struct
         (* program expressions *)
         init_cl       : conslist;
         cl            : conslist;
-        cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
     }
 
@@ -773,18 +772,24 @@ end = struct
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     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 f = Transform.f_of_prog_incl_init rp false in
+
+        let f = simplify_k (get_root_true f) f in
+        Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
+
+        (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
+        (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
+
+        let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in
+        let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f 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;
 
         let cl = Formula.conslist_of_f f in
-        let cl_g = Formula.conslist_of_f f_g in
         let init_cl = Formula.conslist_of_f init_f in
         Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
 
@@ -795,10 +800,10 @@ end = struct
           guarantees;
         Format.printf "@.";
         
-        let ve = mk_varenv rp f_g cl_g in
+        let ve = mk_varenv rp f cl in
 
 
-        { rp; opt; ve; init_cl; cl; cl_g; guarantees; }
+        { rp; opt; ve; init_cl; cl; guarantees; }
 
           
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 1882c85..4c2c397 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -76,7 +76,8 @@ let f_or 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)
+  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)
@@ -109,7 +110,8 @@ and eliminate_not_negate = function
       | AST_GE -> AST_LT
       in
       BRel(r', a, b, is_real)
-  | BTernary _ -> assert false
+  | BTernary (c, a, b) -> 
+    eliminate_not_negate(BOr(BAnd(c, a), BAnd(BNot c, 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 9bce192..0144637 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -209,6 +209,13 @@ let clock_scope_here (node, prefix, _) =
 
 let gen_clock td (node, prefix, _) active rst_exprs =
   let clock_scope = node^"/"^prefix in
+  let act_eq =
+    if clock_scope = "/"
+      then BConst true
+      else if active
+        then BEnumCons(E_EQ, clock_scope^"act", EItem bool_true)
+        else BEnumCons(E_NE, clock_scope^"act", EItem bool_true)
+  in
   let clock_eq =
     let rst_code =
         f_and
@@ -219,28 +226,36 @@ let gen_clock td (node, prefix, _) active rst_exprs =
             then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
             else BConst true)
     in
+    let last_act_eq =
+      (f_and
+        (if not (td.rp.no_time_scope clock_scope)
+          then BRel(AST_EQ, NIdent(clock_scope^"time"),
+              NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
+              false)
+          else BConst true)
+        (if td.rp.init_scope clock_scope
+          then BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
+          else BConst true))
+    in
+    let last_inact_eq =
+      (f_and
+        (if not (td.rp.no_time_scope clock_scope)
+          then BRel(AST_EQ,
+              NIdent(clock_scope^"time"),
+              NIdent("L"^clock_scope^"time"), false)
+          else BConst true)
+        (if td.rp.init_scope clock_scope
+          then f_e_eq (EIdent(clock_scope^"init"))
+                (EIdent ("L"^clock_scope^"init"))
+          else BConst true))
+    in
     let no_rst_code =
-        if active then
-          f_and
-            (if not (td.rp.no_time_scope clock_scope)
-              then BRel(AST_EQ, NIdent(clock_scope^"time"),
-                  NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
-                  false)
-              else BConst true)
-            (if td.rp.init_scope clock_scope
-              then BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
-              else BConst true)
+      if clock_scope = "/"
+        then last_act_eq
         else
-          f_and
-            (if not (td.rp.no_time_scope clock_scope)
-              then BRel(AST_EQ,
-                  NIdent(clock_scope^"time"),
-                  NIdent("L"^clock_scope^"time"), false)
-              else BConst true)
-            (if td.rp.init_scope clock_scope
-              then f_e_eq (EIdent(clock_scope^"init"))
-                    (EIdent ("L"^clock_scope^"init"))
-              else BConst true)
+          f_ternary
+            (BEnumCons(E_EQ, "L"^clock_scope^"act", EItem bool_true))
+            last_act_eq last_inact_eq
     in
     if rst_code = BConst true && no_rst_code = BConst true
       then BConst true
@@ -250,7 +265,7 @@ let gen_clock td (node, prefix, _) active rst_exprs =
           rst_code
           no_rst_code
   in
-  (clock_scope, rst_exprs), clock_eq
+  (clock_scope, rst_exprs), f_and act_eq clock_eq
 
 let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
   let expr_eq e =