First implementation of resetting transitions.

5 files changed, 83 insertions, 40 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)
 
diff --git a/frontend/ast.ml b/frontend/ast.ml
index c561cef..d55626d 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -69,10 +69,6 @@ and  state = {
     st_locals : var_def list;
     body      : eqn ext list;
     until     : transition list;
-    (* these two rst info are determined after parsing, in typing.ml when
-        the variable list is extracted *)
-    mutable i_rst : bool;       (* resettable by S -> S transition *)
-    mutable o_rst : bool;       (* resettable by S' -> S transition *)
 }
 and transition = (expr ext) * (id ext) * bool   (* bool : does it reset ? *)
 
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 672bb9a..e8a6ecf 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -126,7 +126,6 @@ state:
     st_locals = v;
     body = b;
     until = until;
-    i_rst = false; o_rst = false; (* calculated later *)
 } }
 
 trans(TT):
diff --git a/frontend/typing.ml b/frontend/typing.ml
index d814bbe..883e8e0 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -178,17 +178,12 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
             vars_of_expr c @ do_branch a @ do_branch b
         in do_branch b
       | AST_automaton (aid, states, ret) ->
-        (* Determine which states can be reset *)
-        let rst_trans = List.flatten
+        let rst_states = List.flatten
             (List.map (fun (st, _) ->
-                List.map (fun (_, (id, _), _) -> (st.st_name, id))
+                List.map (fun (_, (id, _), _) -> id)
                 (List.filter (fun (_, _, rst) -> rst) st.until))
               states)
         in
-        List.iter (fun (st, _) ->
-            st.i_rst <- List.mem (st.st_name, st.st_name) rst_trans;
-            st.o_rst <- List.exists (fun (a, b) -> b = st.st_name && a <> b) rst_trans)
-          states;
 
         let do_state (st, _) =
           let tvars =
@@ -197,7 +192,7 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
           in
           let st_scope = (node, aid^"."^st.st_name^".", st.body) in
           let svars = vars_in_node node st.st_locals in
-          (if st.i_rst || st.o_rst then
+          (if List.mem st.st_name rst_states then
             [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
           else [])
           @ svars @ tvars @ clock_vars rp st_scope @