Implement automata and activate blocks in interpret.

1 files changed, 117 insertions, 23 deletions

diff --git a/interpret/interpret2.ml b/interpret/interpret2.ml
index 33439e6..d6f7731 100644
--- a/interpret/interpret2.ml
+++ b/interpret/interpret2.ml
@@ -16,7 +16,7 @@ module I : INTERPRET = struct
     | VState of id
     | VPrevious of value list
     | VBusy   (* intermediate value : calculating ! *)
-    | VCalc of (unit -> value)
+    | VCalc of (unit -> unit)
 
   let int_value i = VInt i
   let bool_value b = VBool b
@@ -78,12 +78,13 @@ module I : INTERPRET = struct
 
     Gets the value of a variable relative to a node path.
   *)
-  let get_var env node id =
+  let rec get_var env node id =
     let p = node^"/"^id in
     try match Hashtbl.find env.vars p with
       | VCalc f ->
         Hashtbl.replace env.vars p VBusy;
-        f ()
+        f ();
+        get_var env node id
       | VBusy -> combinatorial_cycle p
       | x -> x
     with
@@ -182,6 +183,8 @@ module I : INTERPRET = struct
 
     Sets all the init variables to true, and all the state variables
     to initial state. Does this recursively.
+    The state reset done by this on the environment is only applied on the
+    next iteration, when the state info has been extracted by extract_st.
   *)
   let rec reset_scope env (node, prefix, eqs) =
     Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
@@ -226,7 +229,7 @@ module I : INTERPRET = struct
             let apath = node^"/"^id^"/"^name in
             let calc () =
               match eval_expr env (node, prefix) expr with
-              | [v] -> Hashtbl.replace env.vars apath v; v
+              | [v] -> Hashtbl.replace env.vars apath v
               | _ -> loc_error (snd expr) error "Unsupported arity for argument."
             in
             Hashtbl.replace env.vars apath (VCalc calc)
@@ -237,18 +240,43 @@ module I : INTERPRET = struct
     let do_eq (e, _) = match e with
       | AST_assign(vars, e) ->
         do_expr e;
-        let calc i () =
+        let calc () =
           let vals = eval_expr env (node, prefix) e in
           List.iter2 (fun (id, _) v ->
-            Hashtbl.replace env.vars (node^"/"^id) v) vars vals;
-          List.nth vals i
+            Hashtbl.replace env.vars (node^"/"^id) v) vars vals
         in
-        List.iteri
-          (fun i (id, _) ->
-              Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc i)))
+        List.iter
+          (fun (id, _) ->
+              Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc)))
           vars
       | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e
-      | _ -> not_implemented "activate_scope"
+      | AST_activate(t, vars) ->
+        let rec do_tree = function
+          | AST_activate_body _ -> ()
+          | AST_activate_if(c, a, b) ->
+            do_expr c; do_tree a; do_tree b
+        in do_tree t;
+        let rec needed x () = match x with
+          | AST_activate_body b ->
+            activate_scope env (node, b.act_id^".", b.body)
+          | AST_activate_if (c, t, f) ->
+            begin match eval_expr env (node, prefix) c with
+            | [VBool true] -> needed t ()
+            | [VBool false] -> needed f ()
+            | _ -> error "Invalid value in activate if condition."
+            end
+        in
+        List.iter (fun id ->
+            Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t)))
+          vars
+      | AST_automaton(aid, states, vars) ->
+        let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with
+          | VState s -> s
+          | _ -> assert false
+        in
+        let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
+        activate_scope env (node, aid^"."^st.st_name^".", st.body);
+        List.iter (fun (c, _, _) -> do_expr c) st.until
     in
     List.iter do_eq eqs
 
@@ -262,8 +290,50 @@ module I : INTERPRET = struct
   (*
     do_weak_transitions : env -> scope -> unit
   *)
-  let do_weak_transitions env (node, prefix, eqs) =
-    not_implemented "do_weak_transitions"
+  let rec do_weak_transitions env (node, prefix, eqs) =
+    let do_expr e =
+      List.iter
+        (fun (id, eqs, args) ->
+          do_weak_transitions env (node^"/"^id, "", eqs))
+        (extract_instances env.st.p e)
+    in
+    let do_eq (e, _) = match e with
+      | AST_assign(_, e) -> do_expr e
+      | AST_assume (_, e) | AST_guarantee (_, e) -> do_expr e
+      | AST_activate(t, _) ->
+        let rec do_tree = function
+          | AST_activate_body b -> do_weak_transitions env (node, b.act_id^".", b.body)
+          | AST_activate_if(c, a, b) ->
+            do_expr c; do_tree a; do_tree b
+        in do_tree t
+      | AST_automaton(aid, states, vars) ->
+        let svn = node^"/"^aid^".state" in
+        let stv = VarMap.find svn env.st.save in
+        let new_st =
+          if is_scope_active env (node, prefix, eqs) then begin
+            let asn = match stv with
+              | VState s -> s
+              | _ -> assert false
+            in
+            let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
+            try
+              let (_, (next_st,_), rst) = List.find
+                (fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true])
+                st.until
+              in
+                if rst then begin
+                  let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in
+                  reset_scope env (node, aid^"."^next_st^".", st.body)
+                end;
+                VState(next_st)
+            with
+              | _ -> stv
+          end else
+            stv
+        in
+            Hashtbl.replace env.vars svn new_st
+    in
+    List.iter do_eq eqs
 
   (*
     extract_st : env -> state
@@ -282,10 +352,18 @@ module I : INTERPRET = struct
       let save_expr save e =
         let save = List.fold_left
           (fun save (id, expr) ->
-            VarMap.add
-              (node^"/"^prefix^id)
-              (VPrevious (eval_expr env (node, prefix) expr))
-              save)
+            let n = node^"/"^prefix^id in
+            if is_scope_active env (node, prefix, eqs) then
+              VarMap.add
+                n
+                (VPrevious (eval_expr env (node, prefix) expr))
+                save
+            else
+              try VarMap.add n
+                (VarMap.find n env.st.save)
+                save
+              with Not_found -> save
+          )
           save (extract_pre e) in
         let save = List.fold_left
           (fun save (n, eqs, _) ->
@@ -296,8 +374,25 @@ module I : INTERPRET = struct
       let save_eq save eq = match fst eq with
         | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
             save_expr save e
-        | AST_automaton(aid, states, _) -> not_implemented "save_eq automaton"
-        | AST_activate(r, _) -> not_implemented "save_eq activate"
+        | AST_automaton(aid, states, _) ->
+          let svn = node^"/"^aid^".state" in
+          let st = Hashtbl.find env.vars svn in
+          let save = VarMap.add (node^"/"^aid^".state") st save in
+          List.fold_left (fun save (st, _) ->
+              let save = 
+                List.fold_left (fun save (c, _, _) -> save_expr save c) save st.until in
+              aux (node, aid^"."^st.st_name^".", st.body) save)
+            save states
+        | AST_activate(r, _) ->
+          let rec do_t save = function
+            | AST_activate_if(c, t, f) ->
+              let save = save_expr save c in
+              let save = do_t save t in
+              do_t save f
+            | AST_activate_body b ->
+              aux (node, b.act_id^".", b.body) save
+          in
+          do_t save r
       in
       List.fold_left save_eq save eqs
 
@@ -327,7 +422,7 @@ module I : INTERPRET = struct
           let cpath = "cst/" ^ d.c_name in
           Hashtbl.replace env.vars cpath (VCalc (fun () ->
             match eval_expr env ("cst", "") d.value with
-            | [v] -> Hashtbl.replace env.vars cpath v; v
+            | [v] -> Hashtbl.replace env.vars cpath v
             | _ -> loc_error l error "Arity error in constant expression."))
         | _ -> ())
       p;
@@ -348,11 +443,10 @@ module I : INTERPRET = struct
     let env = { st = st; vars = vars } in
     
     activate_scope env st.root_scope; 
-    (*
+    if false then
       Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars;
-    *)
     let out = List.map (fun id -> id, get_var env "" id) st.outputs in
-    (* do_weak_transitions env st.root_scope; *)
+    do_weak_transitions env st.root_scope;
     extract_st env, out