summaryrefslogtreecommitdiff
path: root/interpret
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 17:45:00 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 17:45:00 +0200
commit617231f214ace1bc3a2aa48e18db319575166047 (patch)
tree83b05fa9da1e77c91ded9145dcd07e8432252b58 /interpret
parentdedc98b0c14262c53e8573d7fe1dcaa370e43fb5 (diff)
downloadscade-analyzer-617231f214ace1bc3a2aa48e18db319575166047.tar.gz
scade-analyzer-617231f214ace1bc3a2aa48e18db319575166047.zip
Begin of new interpret with more imperative concepts. Scope activation 'n stuff.
Diffstat (limited to 'interpret')
-rw-r--r--interpret/ast_util.ml42
-rw-r--r--interpret/bad_interpret.ml (renamed from interpret/interpret.ml)108
-rw-r--r--interpret/data.ml49
-rw-r--r--interpret/interface.ml40
-rw-r--r--interpret/interpret2.ml359
-rw-r--r--interpret/rename.ml (renamed from interpret/sca.ml)10
6 files changed, 507 insertions, 101 deletions
diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
index db9a76f..e7428bd 100644
--- a/interpret/ast_util.ml
+++ b/interpret/ast_util.ml
@@ -5,7 +5,7 @@ open Util
let find_const_decl p id =
match List.find (function
- | AST_const_decl (c, _) when c.name = id -> true
+ | AST_const_decl (c, _) when c.c_name = id -> true
| _ -> false)
p with
| AST_const_decl d -> d
@@ -13,7 +13,7 @@ let find_const_decl p id =
let find_node_decl p id =
match List.find (function
- | AST_node_decl (c, _) when c.name = id -> true
+ | AST_node_decl (c, _) when c.n_name = id -> true
| _ -> false)
p with
| AST_node_decl d -> d
@@ -26,6 +26,44 @@ let extract_const_decls =
| _ -> l)
[]
+
+(* Utility : find instances declared in an expression *)
+
+(* extract_instances :
+ prog -> expr ext -> (id * eqs * (var_def * expr ext) list) list
+*)
+let rec extract_instances p e = match fst e with
+ | AST_idconst _ | AST_identifier _
+ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+ | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> extract_instances p e'
+ | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+ | AST_arrow(e1, e2) ->
+ extract_instances p e1 @ extract_instances p e2
+ | AST_if(e1, e2, e3) ->
+ extract_instances p e1 @ extract_instances p e2 @ extract_instances p e3
+ | AST_instance((f, _), args, id) ->
+ let more = List.flatten (List.map (extract_instances p) args) in
+ let (node, _) = find_node_decl p f in
+ let args_x = List.map2 (fun id arg -> id, arg) node.args args in
+ (id, node.body, args_x)::more
+
+(* Utility : find pre declarations in an expression *)
+
+(* extract_pre : expr ext -> (id * expr ext) list *)
+let rec extract_pre e = match fst e with
+ | AST_identifier _ | AST_idconst _
+ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+ | AST_unary (_, e') | AST_not e' -> extract_pre e'
+ | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+ | AST_arrow(e1, e2) ->
+ extract_pre e1 @ extract_pre e2
+ | AST_if(e1, e2, e3) ->
+ extract_pre e1 @ extract_pre e2 @ extract_pre e3
+ | AST_instance((f, _), args, id) ->
+ List.flatten (List.map extract_pre args)
+ | AST_pre(e', n) ->
+ (n, e')::(extract_pre e')
+
(* Some errors *)
let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
diff --git a/interpret/interpret.ml b/interpret/bad_interpret.ml
index 6ff125c..08ccf85 100644
--- a/interpret/interpret.ml
+++ b/interpret/bad_interpret.ml
@@ -3,41 +3,57 @@ open Data
open Util
open Ast_util
+(* Data structures for the interpret *)
+
+type scope = string
+
+type svalue =
+ | VInt of int
+ | VBool of bool
+ | VReal of float
+ | VState of id
+ | VPrevious of value
+ | VBusy (* intermediate value : calculating ! for detection of cycles *)
+and value = svalue list
+
+type state = svalue VarMap.t
+
+(* functions for recursively getting variables *)
+
+type calc_fun =
+ | F of (state -> calc_map -> state)
+and calc_map = calc_fun VarMap.t
+
+let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) =
+ let st =
+ if VarMap.mem id st then st
+ else match VarMap.find id c with
+ | F f ->
+ (* Format.printf "%s[ " id; *)
+ let r = f (VarMap.add id VBusy st) c in
+ (* Format.printf "]%s " id; *)
+ r
+ in
+ match VarMap.find id st with
+ | VBusy -> combinatorial_cycle id
+ | v -> st, v
+
+(* pretty-printing *)
+
+let rec str_of_value = function
+ | VInt i -> string_of_int i
+ | VReal r -> string_of_float r
+ | VBool b -> if b then "true" else "false"
+ | VState s -> "state " ^ s
+ | VPrevious p ->
+ "[" ^
+ List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p
+ ^ "]"
+ | VBusy -> "#"
+let print_state st =
+ VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st
-(* Utility : extract subscopes of equation ; extract pre declarations *)
-(* subscopes :
- prog -> expr ext -> (id * eqs * (id * expr ext) list) list
-*)
-let rec subscopes p e = match fst e with
- | AST_idconst _ | AST_identifier _
- | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
- | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e'
- | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
- | AST_arrow(e1, e2) ->
- subscopes p e1 @ subscopes p e2
- | AST_if(e1, e2, e3) ->
- subscopes p e1 @ subscopes p e2 @ subscopes p e3
- | AST_instance((f, _), args, id) ->
- let more = List.flatten (List.map (subscopes p) args) in
- let (node, _) = find_node_decl p f in
- let args_x = List.map2 (fun id arg -> id, arg) node.args args in
- (id, node.body, args_x)::more
-
-(* extract_pre : expr ext -> (id * expr ext) list *)
-let rec extract_pre e = match fst e with
- | AST_identifier _ | AST_idconst _
- | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
- | AST_unary (_, e') | AST_not e' -> extract_pre e'
- | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
- | AST_arrow(e1, e2) ->
- extract_pre e1 @ extract_pre e2
- | AST_if(e1, e2, e3) ->
- extract_pre e1 @ extract_pre e2 @ extract_pre e3
- | AST_instance((f, _), args, id) ->
- List.flatten (List.map extract_pre args)
- | AST_pre(e', n) ->
- (n, e')::(extract_pre e')
(* Expression evaluation *)
@@ -55,14 +71,16 @@ let rec eval_expr env st exp =
let sub_eval = eval_expr env in
let scope = List.hd env.scopes in
match fst exp with
- | AST_identifier (id, _) | AST_idconst(id, _) ->
+ | AST_identifier (id, _) ->
let rec aux = function
| [] ->
- let st, v = get_var st env.c ("cst/"^id) in st, [v]
+ no_variable id
| sc::q ->
try let st, v = get_var st env.c (sc^"/"^id) in st, [v]
- with _ -> aux q
- in aux env.scopes
+ with Not_found -> aux q
+ in loc_error (snd exp) aux env.scopes
+ | AST_idconst (id, _) ->
+ let st, v = get_var st env.c ("cst/"^id) in st, [v]
(* on numerical values *)
| AST_int_const (i, _) -> st, [VInt (int_of_string i)]
| AST_real_const (r, _) -> st, [VReal (float_of_string r)]
@@ -131,7 +149,7 @@ let rec eval_expr env st exp =
| VBool true -> sub_eval st before
| VBool false -> sub_eval st after
| _ -> assert false
- with Not_found -> assert false
+ with Not_found -> error ("Internal: could not find init for scope " ^ scope)
end
(* other *)
| AST_if(cond, a, b) ->
@@ -154,17 +172,17 @@ let rec eval_expr env st exp =
let rec calc_const p d st c =
let env = { p = p; c = c; scopes = ["cst"] } in
match eval_expr env st d.value with
- | st, [v] -> VarMap.add ("cst/"^d.name) v st
- | _ -> type_error ("Cannot assign tuple to constant" ^ d.name)
+ | st, [v] -> VarMap.add ("cst/"^d.c_name) v st
+ | _ -> type_error ("Cannot assign tuple to constant" ^ d.c_name)
let program_consts p =
let cdecl = extract_const_decls p in
let ccmap = List.fold_left
- (fun c (d, _) -> VarMap.add ("cst/"^d.name) (F (calc_const p d)) c)
+ (fun c (d, _) -> VarMap.add ("cst/"^d.c_name) (F (calc_const p d)) c)
VarMap.empty cdecl
in
List.fold_left
- (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.name) in st)
+ (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.c_name) in st)
VarMap.empty
cdecl
@@ -177,7 +195,7 @@ let program_init_state p root_node =
List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs)
in
let add_eq st eq = match fst eq with
- | AST_assign(_, e) -> add_subscopes st (subscopes p e)
+ | AST_assign(_, e) -> add_subscopes st (extract_instances p e)
| AST_assume _ | AST_guarantee _ -> st
| AST_automaton (aid, astates, ret) ->
let (initial, _) = List.find (fun (s, _) -> s.initial) astates in
@@ -225,7 +243,7 @@ let rec build_prog_ccmap p scopes eqs st =
in
List.fold_left add_v c ss_args
in
- List.fold_left add_subscope c (subscopes p e)
+ List.fold_left add_subscope c (extract_instances p e)
| AST_assume _ | AST_guarantee _ -> c
| AST_automaton _ -> not_implemented "build_prog_ccmap for automaton"
| AST_activate _ -> not_implemented "build_prog_ccmap for activate"
@@ -251,7 +269,7 @@ let extract_next_state active env eqs st =
in
let add_eq (st, nst) eq = match fst eq with
| AST_assign(vars, e) ->
- let st, nst = add_subscopes active (st, nst) (subscopes env.p e) in
+ let st, nst = add_subscopes active (st, nst) (extract_instances env.p e) in
List.fold_left (fun (st, nst) (pn, pe) ->
let st, v = if active then eval_expr { env with scopes = scopes } st pe
else st,
diff --git a/interpret/data.ml b/interpret/data.ml
index cf7d820..1d91e93 100644
--- a/interpret/data.ml
+++ b/interpret/data.ml
@@ -4,52 +4,3 @@ open Util
open Ast
open Ast_util
-type scope = string
-
-type svalue =
- | VInt of int
- | VBool of bool
- | VReal of float
- | VState of id
- | VPrevious of value
- | VBusy (* intermediate value : calculating ! for detection of cycles *)
-and value = svalue list
-
-type state = svalue VarMap.t
-
-(* functions for recursively getting variables *)
-
-type calc_fun =
- | F of (state -> calc_map -> state)
-and calc_map = calc_fun VarMap.t
-
-let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) =
- let st =
- if VarMap.mem id st then st
- else try match VarMap.find id c with
- | F f ->
- (* Format.printf "%s[ " id; *)
- let r = f (VarMap.add id VBusy st) c in
- (* Format.printf "]%s " id; *)
- r
- with Not_found -> no_variable id
- in
- match VarMap.find id st with
- | VBusy -> combinatorial_cycle id
- | v -> st, v
-
-(* pretty-printing *)
-
-let rec str_of_value = function
- | VInt i -> string_of_int i
- | VReal r -> string_of_float r
- | VBool b -> if b then "true" else "false"
- | VState s -> "state " ^ s
- | VPrevious p ->
- "[" ^
- List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p
- ^ "]"
- | VBusy -> "#"
-let print_state st =
- VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st
-
diff --git a/interpret/interface.ml b/interpret/interface.ml
new file mode 100644
index 0000000..7b84396
--- /dev/null
+++ b/interpret/interface.ml
@@ -0,0 +1,40 @@
+open Ast
+
+
+module type INTERPRET = sig
+
+
+ exception Bad_datatype
+ type value
+
+ val int_value : int -> value
+ val bool_value : bool -> value
+ val real_value : float -> value
+
+ val as_int : value -> int
+ val as_bool : value -> bool
+ val as_real : value -> float
+
+ val str_repr_of_val : value -> string
+
+ type state
+
+ val print_state : Format.formatter -> state -> unit
+
+ type io = (id * value) list
+
+ (*
+ Construct initial state for a program.
+ The id is the root node of the program evaluation.
+ *)
+ val init_state : prog -> id -> state
+
+ (*
+ Run a step of the program (not necessary to specify the program,
+ it should be encoded in the state).
+ State -> Inputs -> Next state, Outputs
+ *)
+ val step : state -> io -> (state * io)
+
+end
+
diff --git a/interpret/interpret2.ml b/interpret/interpret2.ml
new file mode 100644
index 0000000..33439e6
--- /dev/null
+++ b/interpret/interpret2.ml
@@ -0,0 +1,359 @@
+open Ast
+open Util
+open Ast_util
+open Interface
+
+module I : INTERPRET = struct
+
+ (* Values for variables *)
+
+ exception Bad_datatype
+
+ type value =
+ | VInt of int
+ | VBool of bool
+ | VReal of float
+ | VState of id
+ | VPrevious of value list
+ | VBusy (* intermediate value : calculating ! *)
+ | VCalc of (unit -> value)
+
+ let int_value i = VInt i
+ let bool_value b = VBool b
+ let real_value r = VReal r
+
+ let as_int = function
+ | VInt i -> i
+ | _ -> raise Bad_datatype
+ let as_bool = function
+ | VBool b -> b
+ | _ -> raise Bad_datatype
+ let as_real = function
+ | VReal r -> r
+ | _ -> raise Bad_datatype
+
+ let rec str_repr_of_val = function
+ | VInt i -> string_of_int i
+ | VReal r -> string_of_float r
+ | VBool b -> if b then "true" else "false"
+ | VState s -> "state " ^ s
+ | VPrevious p ->
+ "[" ^
+ List.fold_left (fun s v ->
+ (if s = "" then "" else s ^ ", ") ^ str_repr_of_val v)
+ "" p
+ ^ "]"
+ | VBusy -> "#"
+ | VCalc _ -> "()"
+
+ (* States of the interpret *)
+
+ (* path to node * subscope prefix in node * equations in scope *)
+ type scope = id * id * eqn ext list
+
+ type state = {
+ p : prog;
+ root_scope : scope;
+ outputs : id list;
+ save : value VarMap.t;
+ }
+
+ let print_state fmt st =
+ VarMap.iter
+ (fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v))
+ st.save
+
+ type io = (id * value) list
+
+
+ (* Internal type env : contains the environment for state calculation *)
+ type env = {
+ st : state;
+ vars : (id, value) Hashtbl.t;
+ }
+
+
+ (*
+ get_var : env -> id -> id -> value
+
+ Gets the value of a variable relative to a node path.
+ *)
+ let 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 ()
+ | VBusy -> combinatorial_cycle p
+ | x -> x
+ with
+ | Not_found -> no_variable p
+
+ (*
+ eval_expr : env -> (id * id) -> expr ext -> value list
+ *)
+ let rec eval_expr env (node, prefix) exp =
+ let sub_eval = eval_expr env (node, prefix) in
+ match fst exp with
+ | AST_identifier (id, _) ->
+ [loc_error (snd exp) (get_var env node) id]
+ | AST_idconst (id, _) ->
+ begin try [VarMap.find ("cst/"^id) env.st.save]
+ with Not_found -> loc_error (snd exp) no_variable id end
+ (* on numerical values *)
+ | AST_int_const (i, _) -> [VInt (int_of_string i)]
+ | AST_real_const (r, _) -> [VReal (float_of_string r)]
+ | AST_unary(AST_UPLUS, e) -> sub_eval e
+ | AST_unary(AST_UMINUS, e) ->
+ begin match sub_eval e with
+ | [VInt x] -> [VInt (-x)]
+ | [VReal x] -> [VReal(-. x)]
+ | _ -> type_error "Unary on non-numerical."
+ end
+ | AST_binary(op, e1, e2) ->
+ let iop, fop = match op with
+ | AST_PLUS -> (+), (+.)
+ | AST_MINUS -> (-), (-.)
+ | AST_MUL -> ( * ), ( *. )
+ | AST_DIV -> (/), (/.)
+ | AST_MOD -> (mod), mod_float
+ in
+ begin match sub_eval e1, sub_eval e2 with
+ | [VInt a], [VInt b] -> [VInt (iop a b)]
+ | [VReal a], [VReal b] -> [VReal(fop a b)]
+ | _ -> type_error "Invalid arguments for numerical binary."
+ end
+ (* on boolean values *)
+ | AST_bool_const b -> [VBool b]
+ | AST_binary_rel(op, e1, e2) ->
+ let r = match op with
+ | AST_EQ -> (=) | AST_NE -> (<>)
+ | AST_LT -> (<) | AST_LE -> (<=)
+ | AST_GT -> (>) | AST_GE -> (>=)
+ in
+ begin match sub_eval e1, sub_eval e2 with
+ | [VInt a], [VInt b] -> [VBool (r a b)]
+ | [VReal a], [VReal b] -> [VBool (r a b)]
+ | [VBool a], [VBool b] -> [VBool (r a b)]
+ | _ -> type_error "Invalid arguments for binary relation."
+ end
+ | AST_binary_bool(op, e1, e2) ->
+ let r = match op with
+ | AST_AND -> (&&) | AST_OR -> (||)
+ in
+ begin match sub_eval e1, sub_eval e2 with
+ | [VBool a], [VBool b] -> [VBool (r a b)]
+ | _ -> type_error "Invalid arguments for boolean relation."
+ end
+ | AST_not(e) ->
+ begin match sub_eval e with
+ | [VBool b] -> [VBool (not b)]
+ | _ -> type_error "Invalid arguments for boolean negation."
+ end
+ (* temporal primitives *)
+ | AST_pre(exp, n) ->
+ begin try match VarMap.find (node^"/"^prefix^n) env.st.save with
+ | VPrevious x -> x
+ | _ -> assert false
+ with Not_found -> []
+ end
+ | AST_arrow(before, after) ->
+ begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with
+ | VBool true -> sub_eval before
+ | VBool false -> sub_eval after
+ | _ -> assert false
+ with Not_found -> assert false
+ end
+ (* other *)
+ | AST_if(cond, a, b) ->
+ begin match sub_eval cond with
+ | [VBool true] -> sub_eval a
+ | [VBool false] -> sub_eval b
+ | _ -> type_error "Invalid condition in if."
+ end
+ | AST_instance((f, _), args, nid) ->
+ let (n, _) = find_node_decl env.st.p f in
+ List.map
+ (fun (_, (id, _), _) -> get_var env (node^"/"^nid) id)
+ n.ret
+
+ (*
+ reset_scope : env -> scope -> unit
+
+ Sets all the init variables to true, and all the state variables
+ to initial state. Does this recursively.
+ *)
+ let rec reset_scope env (node, prefix, eqs) =
+ Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
+ let do_exp e =
+ List.iter
+ (fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs))
+ (extract_instances env.st.p e)
+ in
+ let do_eq (e, _) = match e with
+ | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e
+ | AST_automaton (aid, states, _) ->
+ let (init_state, _) = List.find (fun (st, _) -> st.initial) states in
+ Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name);
+ List.iter
+ (fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body))
+ states
+ | AST_activate (x, _) ->
+ let rec aux = function
+ | AST_activate_if (_, a, b) -> aux a; aux b
+ | AST_activate_body b ->
+ reset_scope env (node, b.act_id^".", b.body)
+ in aux x
+ in
+ List.iter do_eq eqs
+
+ (*
+ activate_scope : env -> scope -> unit
+
+ Adds functions for calculating the variables in this scope.
+ For assign : simple !
+ For automaton : lazily select+activate automaton state (would enable
+ implementation of strong transitions)
+ For activate : lazily select+activate active block
+ *)
+ let rec activate_scope env (node, prefix, eqs) =
+ Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true);
+ let do_expr e =
+ List.iter
+ (fun (id, eqs, args) ->
+ activate_scope env (node^"/"^id, "", eqs);
+ let do_arg ((_,(name,_),_), expr) =
+ let apath = node^"/"^id^"/"^name in
+ let calc () =
+ match eval_expr env (node, prefix) expr with
+ | [v] -> Hashtbl.replace env.vars apath v; v
+ | _ -> loc_error (snd expr) error "Unsupported arity for argument."
+ in
+ Hashtbl.replace env.vars apath (VCalc calc)
+ in
+ List.iter do_arg args)
+ (extract_instances env.st.p e)
+ in
+ let do_eq (e, _) = match e with
+ | AST_assign(vars, e) ->
+ do_expr e;
+ let calc i () =
+ 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
+ in
+ List.iteri
+ (fun i (id, _) ->
+ Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc i)))
+ vars
+ | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e
+ | _ -> not_implemented "activate_scope"
+ in
+ List.iter do_eq eqs
+
+ (*
+ is_scope_active : env -> scope -> bool
+ *)
+ let is_scope_active env (node, prefix, _) =
+ try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act"))
+ with Not_found -> false
+
+ (*
+ do_weak_transitions : env -> scope -> unit
+ *)
+ let do_weak_transitions env (node, prefix, eqs) =
+ not_implemented "do_weak_transitions"
+
+ (*
+ extract_st : env -> state
+ *)
+ let extract_st env =
+ let rec aux (node, prefix, eqs) save =
+
+ let init =
+ try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init"))
+ with Not_found ->
+ let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save)
+ in pre_init && (not (is_scope_active env (node, prefix, eqs)))
+ in
+ let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in
+
+ 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)
+ save (extract_pre e) in
+ let save = List.fold_left
+ (fun save (n, eqs, _) ->
+ aux (node^"/"^n, "", eqs) save)
+ save (extract_instances env.st.p e)
+ in save
+ in
+ 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"
+ in
+ List.fold_left save_eq save eqs
+
+ in
+ let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in
+ { env.st with save = aux env.st.root_scope consts }
+
+ (*
+ init_state : prog -> id -> state
+ *)
+ let init_state p root =
+ let (n, _) = find_node_decl p root in
+ let root_scope = ("", "", n.body) in
+
+ let st = {
+ p = p;
+ root_scope = root_scope;
+ save = VarMap.empty;
+ outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
+ } in
+
+ let env = { st = st; vars = Hashtbl.create 42 } in
+
+ (* calculate constants *)
+ List.iter (function
+ | AST_const_decl(d, l) ->
+ 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
+ | _ -> loc_error l error "Arity error in constant expression."))
+ | _ -> ())
+ p;
+ List.iter (function
+ | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name)
+ | _ -> ())
+ p;
+
+ reset_scope env root_scope;
+ { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
+
+ (*
+ step : state -> io -> (state * io)
+ *)
+ let step st i =
+ let vars = Hashtbl.create 10 in
+ List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i;
+ let env = { st = st; vars = vars } in
+
+ activate_scope env st.root_scope;
+ (*
+ 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; *)
+ extract_st env, out
+
+
+end
diff --git a/interpret/sca.ml b/interpret/rename.ml
index 4a012ae..46c6f04 100644
--- a/interpret/sca.ml
+++ b/interpret/rename.ml
@@ -10,7 +10,7 @@ type renaming = (id * bool) VarMap.t
let consts_renaming p =
let cdecl = extract_const_decls p in
List.fold_left
- (fun rn (d,_) -> VarMap.add d.name (d.name, true) rn)
+ (fun rn (d,_) -> VarMap.add d.c_name (d.c_name, true) rn)
VarMap.empty
cdecl
@@ -60,9 +60,9 @@ let rec rename_eqn rn e =
| AST_assume(a, e) -> AST_assume(a, rename_expr e rn)
| AST_automaton(aid, states, ret) ->
let rename_state ((st:Ast.state),l) =
- let rn = add_var_defs (aid^"."^st.name^".") rn st.locals in
+ let rn = add_var_defs (aid^"."^st.st_name^".") rn st.st_locals in
{ st with
- locals = List.map (rename_var_def rn) st.locals;
+ st_locals = List.map (rename_var_def rn) st.st_locals;
body = List.map (rename_eqn rn) st.body;
until = List.map (fun (c, n, r) -> (rename_expr c rn, n, r)) st.until;
}, l
@@ -73,9 +73,9 @@ let rec rename_eqn rn e =
| AST_activate_if(c, a, b) ->
AST_activate_if(rename_expr c rn, rename_activate_if a, rename_activate_if b)
| AST_activate_body b ->
- let rn = add_var_defs (b.id^".") rn b.locals in
+ let rn = add_var_defs (b.act_id^".") rn b.act_locals in
AST_activate_body{ b with
- locals = List.map (rename_var_def rn) b.locals;
+ act_locals = List.map (rename_var_def rn) b.act_locals;
body = List.map (rename_eqn rn) b.body;
}
in