Correct some bugs on clocks.

5 files changed, 89 insertions, 32 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 =
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 883e8e0..83374ed 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -136,7 +136,12 @@ let clock_vars rp (node, prefix, _) =
         then
           (false, node^"/"^prefix^"init", bool_type)::v
         else v in
-    v
+    let v =
+      (* root scope is always active *)
+      if node = "" && prefix = ""
+        then v
+        else (false, node^"/"^prefix^"act", bool_type)::v
+    in v
 
 (*
     extract_all_vars : rooted_prog -> scope -> var list
@@ -231,7 +236,9 @@ let root_prog p root no_time_scope init_scope =
       const_vars;
       all_vars = [] } in
 
-    let root_vars = vars_in_node "" (decls_of_node root_node) in
+    let root_vars =
+        (false, "/must_reset", bool_type)::
+        (vars_in_node "" (decls_of_node root_node)) in
     let root_clock_vars = clock_vars rp root_scope in
 
     { rp with all_vars = root_clock_vars @
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
new file mode 100644
index 0000000..7970aab
--- /dev/null
+++ b/tests/source/two_counters.scade
@@ -0,0 +1,28 @@
+const n1: int = 10;
+const n2: int = 6;
+
+
+node top(a,b,c : bool) returns (ok, r1, r2 : bool)
+var
+  x, y, pre_x, pre_y: int;
+  o1, o2: bool;
+
+  m: bool;
+let
+  x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
+  y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
+  o1= x = n1;
+  o2= y = n2;
+  ok= if o1 then o2 else true;
+  r1 = 0<=x and x<=n1;
+  r2 = 0<=y and y<=n2;
+  pre_x = 0 -> pre(x);
+  pre_y = 0 -> pre(y);
+
+  m = true -> pre o2;
+
+  guarantee g1: ok;
+  guarantee g2: r1;
+  guarantee g3: r2;
+tel
+