Begin of new interpret with more imperative concepts. Scope activation 'n stuff.

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