First implementation of resetting transitions.

2 files changed, 80 insertions, 27 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 9c0ff71..0045489 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,20 +50,26 @@ type bool_expr =
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
-let f_and a b = match a, b with
-  | BConst false, _ | _, BConst false
-  | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false
-  | BConst true, b -> b
-  | a, BConst true -> a
-  | a, b -> BAnd(a, b)
+let is_false = function
+  | BConst false | BNot(BConst true) -> true
+  | _ -> false
+let is_true = function
+  | BConst true | BNot(BConst false) -> true
+  | _ -> false
+
+let f_and a b =
+  if is_false a || is_false b then BConst false
+  else if is_true a then b
+  else if is_true b then a
+  else BAnd(a, b)
 
 let f_and_list = List.fold_left f_and (BConst true)
 
-let f_or a b = match a, b with
-  | BConst true, _ | _, BConst true -> BConst true
-  | BConst false, b -> b
-  | a, BConst false -> a
-  | a, b -> BOr(a, b)
+let f_or a b =
+  if is_true a || is_true b then BConst true
+  else if is_false a then b
+  else if is_false b then a
+  else BOr(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)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 1cbc27d..17fd064 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -208,17 +208,17 @@ let clock_scope_here (node, prefix, _) =
 let gen_clock td (node, prefix, _) active rst_exprs =
   let clock_scope = node^"/"^prefix in
   let clock_eq =
-    f_or
-      (f_and (reset_cond rst_exprs)
-        (f_and
+    let rst_code =
+        f_and
           (if not (td.rp.no_time_scope clock_scope)
             then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)
             else BConst true)
           (if td.rp.init_scope clock_scope
             then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
-            else BConst true)))
-      (f_and (no_reset_cond rst_exprs)
-        (if active then
+            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"),
@@ -238,7 +238,14 @@ let gen_clock td (node, prefix, _) active rst_exprs =
             (if td.rp.init_scope clock_scope
               then f_e_eq (EIdent(clock_scope^"init"))
                     (EIdent ("L"^clock_scope^"init"))
-              else BConst true)))
+              else BConst true)
+    in
+    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)
   in
   (clock_scope, rst_exprs), clock_eq
 
@@ -374,6 +381,13 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
           (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
       in
 
+      let rst_states = uniq_sorted @@ List.sort compare @@ List.flatten
+          (List.map (fun (st, _) ->
+              List.map (fun (_, (id, _), _) -> id)
+              (List.filter (fun (_, _, rst) -> rst) st.until))
+            states)
+      in
+
       let st_eq_inact (st, _) =
         let st_scope = node, aid^"."^st.st_name^".", st.body in
         let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in
@@ -386,28 +400,61 @@ let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs)
         let st_eq_act (st, l) =
           let act_eq =
             let st_scope = node, aid^"."^st.st_name^".", st.body in
+            let rst_exprs =
+              if List.mem st.st_name rst_states then
+                  (f_e_eq (EIdent("L"^node^"/"^aid^"."^st.st_name^".must_reset"))
+                    (EItem bool_true))::rst_exprs
+              else rst_exprs
+            in
             let cs2, clock_eq = gen_clock td st_scope true rst_exprs in
             let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in
+
+            let cr, cnr = List.partition
+              (fun i -> List.exists (fun (_, (v, _), x) -> x && v = i) st.until)
+              rst_states in
+            let must_reset_c l f =
+              f_and_list
+                (List.map
+                  (fun i -> f_e_eq (EIdent (node^"/"^aid^"."^i^".must_reset"))
+                      (EItem (if f i then bool_true else bool_false)))
+                  l)
+            in
             let rec aux = function
-              | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
+              | [] ->
+                f_and
+                  (must_reset_c cr (fun _ -> false))
+                  (BEnumCons(E_EQ, nstv, EItem st.st_name))
               | (c, (target, l), rst)::q ->
-                if rst then loc_error l error "Resetting transitions not supported.";
                 f_or
                   (f_and (f_of_expr td (node, prefix, clock_scope) c)
-                        (BEnumCons(E_EQ, nstv, EItem target)))
+                        (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))
-            in f_and st_eq (aux st.until) 
+            in
+            let trans_code = must_reset_c cnr (fun _ -> false) in
+            let trans_code = f_and trans_code (aux st.until) in
+            f_and st_eq trans_code 
           in
-          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)))
+          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)))
         in
         f_and st_choice_eq
           (f_and_list (List.map st_eq_act states))
       else
         f_and st_choice_eq
-          (f_and_list (List.map st_eq_inact states))
+          (f_and
+            (f_and_list
+              (List.map
+                (fun s -> let n = node^"/"^aid^"."^s^".must_reset" in
+                  f_e_eq (EIdent n) (EIdent ("L"^n)))
+                rst_states))
+            (f_and_list (List.map st_eq_inact states)))
   in
   f_and_list (List.map do_eq eqs)