diff options
Diffstat (limited to 'interpret')
| -rw-r--r-- | interpret/interpret2.ml | 140 |
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 |