summaryrefslogtreecommitdiff
path: root/interpret/interpret2.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interpret/interpret2.ml')
-rw-r--r--interpret/interpret2.ml140
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-24 02:41:17 +0000