Working prototype for an interpret ! But very messy.

19 files changed, 533 insertions, 74 deletions

diff --git a/Makefile b/Makefile
index 5e785e0..9f1896f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,13 +1,15 @@
 .PHONY: clean
 
 BIN=analyze
-SRCDIRS=libs,frontend
+SRCDIRS=libs,frontend,interpret
 
 SRC= 	main.ml \
 		frontend/ast.ml \
 		frontend/parser.mly \
 		frontend/lexer.mll \
-		frontend/ast_printer.ml
+		frontend/ast_printer.ml \
+		interpret/data.ml \
+		interpret/interpret.ml
 
 all: $(BIN)
 
diff --git a/frontend/ast.ml b/frontend/ast.ml
index b245119..50fa3f4 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -14,7 +14,6 @@ type typ =
     | AST_TINT
     | AST_TBOOL
     | AST_TREAL
-    | AST_TGROUP of typ list
 
 type unary_op =
     | AST_UPLUS
@@ -56,20 +55,29 @@ type expr =
     | AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
     | AST_not         of expr ext
     (* temporal primitives *)
-    | AST_pre         of expr ext
+    | AST_pre         of expr ext * id
     | AST_arrow       of (expr ext) * (expr ext)
     (* other *)
     | AST_if          of (expr ext) * (expr ext) * (expr ext)
-    | AST_instance    of (id ext) * (expr ext list)
-    (* (TODO) and more : when, merge, activate instances, ... *)
+    | AST_instance    of (id ext) * (expr ext list) * id
 
-type eqn =
+type var_def = bool * (id ext) * typ
+
+type automaton = id * state ext list * id list
+and  state = {
+    initial : bool;
+    name    : id;
+    locals  : var_def list;
+    body    : eqn ext list;
+    until   : transition list;
+}
+and transition = (expr ext) * (id ext)
+
+and eqn =
     | AST_assign     of (id ext list) * (expr ext)
     | AST_guarantee  of (id ext) * (expr ext)
     | AST_assume     of (id ext) * (expr ext)
-    (* (TODO) and more : automaton, activate... *)
-
-type var_def = bool * (id ext) * typ
+    | AST_automaton  of automaton
 
 type node_decl = {
     name : id;
@@ -90,3 +98,4 @@ type toplevel =
     | AST_const_decl of const_decl ext
 
 type prog = toplevel list
+
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 611e802..857e01d 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -57,7 +57,7 @@ let arrow_precedence = 20
 let if_precedence = 10
 
 let expr_precedence = function
-  | AST_unary (_, _) | AST_pre(_) | AST_not(_) -> 99
+  | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> 99
   | AST_binary(op, _, _) -> binary_op_precedence op
   | AST_binary_rel(r, _, _) -> binary_rel_precedence r
   | AST_binary_bool(r, _, _) -> binary_bool_precedence r
@@ -84,11 +84,6 @@ let rec string_of_typ = function
   | AST_TINT -> "int"
   | AST_TBOOL -> "bool"
   | AST_TREAL -> "real"
-  | AST_TGROUP its ->
-    List.fold_left (fun s t ->
-      (if s = "" then "" else s ^ ", ") ^ (string_of_typ t))
-      ""
-      its
 
 (* expressions *)
 
@@ -108,7 +103,7 @@ let rec print_expr fmt e =
       if expr_precedence e1 <= expr_precedence e
       then Format.fprintf fmt "(%a)" print_expr e1
       else Format.fprintf fmt "%a" print_expr e1
-  | AST_pre (e1,_) ->
+  | AST_pre ((e1,_), _) ->
       Format.pp_print_string fmt "pre ";
       if expr_precedence e1 <= expr_precedence e
       then Format.fprintf fmt "(%a)" print_expr e1
@@ -158,7 +153,7 @@ let rec print_expr fmt e =
         
   | AST_identifier (v,_) -> print_id fmt v
 
-  | AST_instance ((i,_),l) ->
+  | AST_instance ((i,_),l, _) ->
         Format.fprintf fmt "%a(%a)"
           print_id i (print_list print_expr ", ") (List.map fst l)
 
@@ -176,19 +171,42 @@ let rec print_eqn ind fmt = function
   | AST_guarantee((i, _), (e, _)) ->
       Format.fprintf fmt "%sguarantee %s: %a;@\n"
           ind i print_expr e
+  | AST_automaton a -> print_automaton ind fmt a
+
+and print_automaton ind fmt (n, sts, r) =
+  Format.fprintf fmt "%sautomaton %s@\n" ind n;
+  List.iter (print_state (indent ind) fmt) sts;
+  Format.fprintf fmt "%sreturns %a;@\n" ind (print_list print_id ", ") r
+
+and print_state ind fmt (st, _) =
+  Format.fprintf fmt "%s%sstate %s@\n"
+    ind (if st.initial then "initial " else "") st.name;
+  if st.locals <> [] then begin
+    Format.fprintf fmt "%svar" ind;
+    List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) st.locals;
+    Format.fprintf fmt "@\n";
+  end;
+  Format.fprintf fmt "%slet@\n%a%stel@\n"
+    ind (print_block ind) st.body ind;
+  if st.until <> [] then begin
+    Format.fprintf fmt "%suntil@\n" ind;
+    List.iter (fun ((e, _),(s, _)) -> 
+        Format.fprintf fmt "%sif %a resume %s;@\n" (indent ind) print_expr e s)
+      st.until
+  end
 
 and print_block ind fmt b =
   List.iter (fun (bb,_) -> print_eqn (indent ind) fmt bb) b
 
 (* declarations *)
 
-let print_var_decl fmt (pr, (i, _), ty) =
+and print_var_decl fmt (pr, (i, _), ty) =
     Format.fprintf fmt "%s%s: %s"
       (if pr then "probe " else "")
       i
       (string_of_typ ty)
 
-let print_node_decl fmt (d : node_decl) =
+and print_node_decl fmt (d : node_decl) =
     Format.fprintf fmt "node %s(%a) returns(%a)@\n"
       d.name
       (print_list print_var_decl "; ") d.args
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index 1fd638b..9dc7da3 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -6,32 +6,39 @@
   let kwd_table = Hashtbl.create 10
   let () = List.iter (fun (a, b) -> Hashtbl.add kwd_table a b)
     [
-      "bool",     BOOL;
-      "int",      INT;
-      "real",     REAL;
+      "bool",       BOOL;
+      "int",        INT;
+      "real",       REAL;
 
-      "const",    CONST;
-      "node",     NODE;
-      "returns",  RETURNS;
-      "var",      VAR;
-      "let",      LET;
-      "tel",      TEL;
+      "const",      CONST;
+      "node",       NODE;
+      "returns",    RETURNS;
+      "var",        VAR;
+      "let",        LET;
+      "tel",        TEL;
 
-      "if",       IF;
-      "then",     THEN;
-      "else",     ELSE;
-      "pre",      PRE;
-      "not",      NOT;
-      "and",      AND;
-      "or",       OR;
-      "mod",      MOD;
+      "if",         IF;
+      "then",       THEN;
+      "else",       ELSE;
+      "pre",        PRE;
+      "not",        NOT;
+      "and",        AND;
+      "or",         OR;
+      "mod",        MOD;
 
-      "true",     TRUE;
-      "false",    FALSE;
+      "automaton",  AUTOMATON;
+      "state",      STATE;
+      "initial",    INITIAL;
+      "unless",     UNLESS;
+      "until",      UNTIL;
+      "resume",     RESUME;
 
-      "assume",   ASSUME;
-      "guarantee",GUARANTEE;
-      "probe",    PROBE;
+      "true",       TRUE;
+      "false",      FALSE;
+
+      "assume",     ASSUME;
+      "guarantee",  GUARANTEE;
+      "probe",      PROBE;
     ]
 }
 
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 51974d1..fb00478 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -1,5 +1,6 @@
 %{
 open Ast
+open Util
 %}
 
 %token BOOL INT REAL
@@ -12,6 +13,7 @@ open Ast
 %token VAR LET TEL
 %token PRE
 %token ASSUME GUARANTEE
+%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME
 
 %token LPAREN RPAREN
 %token LCURLY RCURLY
@@ -57,12 +59,12 @@ primary_expr:
 | TRUE                      { AST_bool_const true }
 | FALSE                     { AST_bool_const false }
 | e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN 
-                            { AST_instance (e, l) }
+                            { AST_instance (e, l, fst e ^ uid ()) }
 
 unary_expr:
 | e=primary_expr                   { e }
 | NOT e=ext(unary_expr)            { AST_not(e) }
-| PRE e=ext(unary_expr)            { AST_pre(e) }
+| PRE e=ext(unary_expr)            { AST_pre(e, "pre"^uid()) }
 | o=unary_op e=ext(unary_expr)     { AST_unary (o, e) }
 
 %inline unary_op:
@@ -103,23 +105,52 @@ expr:
 
 
 (* Equations (can be asserts, automata, ...) *)
+automaton:
+| AUTOMATON a=IDENT? s=list(ext(state)) RETURNS r=separated_list(COMMA, IDENT)
+    { ((match a with Some n -> n | None -> "aut") ^ uid (), s, r) }
+
+state:
+| i=boption(INITIAL) STATE n=IDENT
+  unless=trans(UNLESS)
+  v=option(var_decl)
+  b=body
+  until=trans(UNTIL)
+{ if unless <> [] then failwith "UNLESS transitions not supported.";
+  { initial = i;
+    name = n;
+    locals = (match v with Some v -> v | None -> []);
+    body = b;
+    until = until;
+} }
+
+trans(TT):
+| TT t=nonempty_list(terminated(transition, SEMICOLON))   { t }
+|                                                         { [] }
+
+transition:
+| IF e=ext(expr) RESUME s=ext(IDENT)                      { (e, s) }
+
+
 eqn:
 | i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr)         
                                                 { AST_assign(i, e) }
 | ASSUME i=ext(IDENT) COLON e=ext(expr)         { AST_assume(i, e) }
 | GUARANTEE i=ext(IDENT) COLON e=ext(expr)      { AST_guarantee(i, e) }
+| a=automaton                                   { AST_automaton(a) }
 
 typ:
 | INT                                           { AST_TINT }
 | BOOL                                          { AST_TBOOL }
 | REAL                                          { AST_TREAL }
-| LPAREN l=separated_list(COMMA, typ) RPAREN    { AST_TGROUP(l) }
 
 (* Declarations *)
 dbody:
 | e=ext(eqn) SEMICOLON                          { [e] }
+| l=body                                        { l }
+
+body:
 | LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
-                                                { l }
+  { l }
 
 var:
 |   p=boption(PROBE) i=ext(IDENT)   { (p, i) }
@@ -157,7 +188,7 @@ node_decl:
 | NODE id=IDENT LPAREN v=vars RPAREN
     RETURNS LPAREN rv=vars RPAREN
     lv=var_decl
-    LET b=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
+    b=body
 { { name = id;
     args = v;
     ret = rv;
diff --git a/interpret/data.ml b/interpret/data.ml
new file mode 100644
index 0000000..2721528
--- /dev/null
+++ b/interpret/data.ml
@@ -0,0 +1,61 @@
+(* Data structures for representing the state of a system *)
+
+open Util
+open Ast
+
+exception Combinatorial_cycle of string
+exception No_variable of string
+exception Type_error of string
+let type_error e = raise (Type_error e)
+exception Not_implemented of string
+let not_implemented e = raise (Not_implemented e)
+
+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 -> raise (No_variable id)
+  in
+    match VarMap.find id st with
+    | VBusy -> raise (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/interpret.ml b/interpret/interpret.ml
new file mode 100644
index 0000000..4584fa4
--- /dev/null
+++ b/interpret/interpret.ml
@@ -0,0 +1,273 @@
+open Ast
+open Data
+open Util
+
+(* Utility : find declaration of a const / a node *)
+
+let find_const_decl p id =
+  match List.find (function
+                   | AST_const_decl (c, _) when c.name = id -> true
+                   | _ -> false) 
+                  p with
+  | AST_const_decl d -> d
+  | _ -> assert false
+
+let find_node_decl p id =
+  match List.find (function
+                   | AST_node_decl (c, _) when c.name = id -> true
+                   | _ -> false) 
+                  p with
+  | AST_node_decl d -> d
+  | _ -> assert false
+
+(* Expression evaluation *)
+
+(*
+  eval_expr : calc_map -> state -> string -> expr ext -> (state * value)
+*)
+let rec eval_expr c scope st exp =
+  let sub_eval = eval_expr c scope in
+  match fst exp with
+  | AST_identifier (id, _) ->
+    begin try let st, v = get_var st c (scope^"/"^id) in st, [v]
+    with No_variable _ -> let st, v = get_var st c ("cst/"^id) in st, [v]
+    end
+  (* on numerical values *)
+  | AST_int_const (i, _) -> st, [VInt (int_of_string i)]
+  | AST_real_const (r, _) -> st, [VReal (float_of_string r)]
+  | AST_unary(AST_UPLUS, e) -> sub_eval st e
+  | AST_unary(AST_UMINUS, e) ->
+    begin match sub_eval st e with
+    | st, [VInt x] -> st, [VInt (-x)]
+    | st, [VReal x] -> st, [VReal(-. x)]
+    | _ -> type_error "Unary on non-numerical."
+    end
+  | AST_binary(op, e1, e2) ->
+    let st, v1 = sub_eval st e1 in
+    let st, v2 = sub_eval st e2 in
+    let iop, fop = match op with
+    | AST_PLUS -> (+), (+.)
+    | AST_MINUS -> (-), (-.)
+    | AST_MUL -> ( * ), ( *. )
+    | AST_DIV -> (/), (/.)
+    | AST_MOD -> (mod), mod_float
+    in
+    begin match v1, v2 with
+    | [VInt a], [VInt b] -> st, [VInt (iop a b)]
+    | [VReal a], [VReal b] -> st, [VReal(fop a b)]
+    | _ -> type_error "Invalid arguments for numerical binary."
+    end
+  (* on boolean values *)
+  | AST_bool_const b -> st, [VBool b]
+  | AST_binary_rel(op, e1, e2) ->
+    let st, v1 = sub_eval st e1 in
+    let st, v2 = sub_eval st e2 in
+    let r = match op with
+    | AST_EQ -> (=)     | AST_NE -> (<>)
+    | AST_LT -> (<)     | AST_LE -> (<=)
+    | AST_GT -> (>)     | AST_GE -> (>=)
+    in
+    begin match v1, v2 with
+    | [VInt a], [VInt b] -> st, [VBool (r a b)]
+    | [VReal a], [VReal b] -> st, [VBool (r a b)]
+    | [VBool a], [VBool b] -> st, [VBool (r a b)]
+    | _ -> type_error "Invalid arguments for binary relation."
+    end
+  | AST_binary_bool(op, e1, e2) ->
+    let st, v1 = sub_eval st e1 in
+    let st, v2 = sub_eval st e2 in
+    let r = match op with
+    | AST_AND -> (&&)   | AST_OR -> (||)
+    in
+    begin match v1, v2 with
+    | [VBool a], [VBool b] -> st, [VBool (r a b)]
+    | _ -> type_error "Invalid arguments for boolean relation."
+    end
+  | AST_not(e) ->
+    begin match sub_eval st e with
+    | st, [VBool b] -> st, [VBool (not b)]
+    | _ -> type_error "Invalid arguments for boolean negation."
+    end
+  (* temporal primitives *)
+  | AST_pre(exp, n) ->
+    begin try match VarMap.find (scope^"/"^n) st with
+      | VPrevious x -> st, x
+      | _ -> st, []
+    with Not_found -> st, []
+    end
+  | AST_arrow(before, after) -> 
+    begin try match VarMap.find (scope^"/init") st with
+    | VBool true -> sub_eval st before
+    | VBool false -> sub_eval st after
+    | _ -> assert false
+    with Not_found -> assert false
+    end
+  (* other *)
+  | AST_if(cond, a, b) ->
+    let st, cv = sub_eval st cond in
+    begin match cv with
+    | [VBool true] -> sub_eval st a
+    | [VBool false] -> sub_eval st b
+    | _ -> type_error "Invalid condition in if."
+    end
+  | AST_instance((f, _), args, id) -> not_implemented "instance"
+
+(* Constant calculation *)
+
+let rec calc_const d st c =
+  match eval_expr c "cst" st d.value with
+  | st, [v] -> VarMap.add ("cst/"^d.name) v st
+  | _ -> type_error ("Cannot assign tuple to constant" ^ d.name)
+
+let program_consts p =
+  let cdecl = List.fold_left
+    (fun l d -> match d with
+      | AST_const_decl (d, _) -> d::l
+      | _ -> l)
+    [] p
+  in
+  let ccmap = List.fold_left
+    (fun c d -> VarMap.add ("cst/"^d.name) (F (calc_const d)) c)
+    VarMap.empty cdecl
+  in
+  List.fold_left
+    (fun st d -> let st, _ = get_var st ccmap ("cst/"^d.name) in st)
+    VarMap.empty
+    cdecl
+
+(* Program execution *)
+
+(* subscopes :
+      prog -> expr ext -> (id * eqs * (id * expr ext) list) list
+*)
+let rec subscopes p e = match fst e with
+  | 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_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')
+
+
+(* build calc map *)
+let rec build_prog_ccmap p scope eqs st =
+  let add_eq c eq = match fst eq with
+    | AST_assign(vars, e) ->
+      let calc st c =
+        let st, vals = eval_expr c scope st e in
+        List.fold_left2
+          (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st)
+          st vars vals
+      in
+      let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in
+
+      let add_subscope c (ss_id, ss_eqs, ss_args) =
+        let c = VarMap.merge (fun _ a b -> match a, b with
+          | Some x, None -> Some x
+          | None, Some y -> Some y
+          | _ -> assert false) c
+          (build_prog_ccmap p (scope^"/"^ss_id) ss_eqs st)
+        in
+        let add_v c ((_, (id, _), _), eq) =
+          let calc st c =
+            let st, vals = eval_expr c scope st eq in
+            match vals with
+            | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st
+            | _ -> type_error "invalid arity"
+          in
+          VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c
+        in
+        List.fold_left add_v c ss_args
+      in
+      List.fold_left add_subscope c (subscopes p e)
+    | AST_assume _ | AST_guarantee _ -> c
+    | AST_automaton _ -> not_implemented "build_prog_ccmap for automaton"
+  in
+  List.fold_left add_eq VarMap.empty eqs
+
+let extract_next_state active p scope eqs st ccmap =
+  let csts = VarMap.filter
+    (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/")
+    st
+  in
+  let rec aux active scope eqs st nst =
+    let r = VarMap.add (scope^"/init")
+        (if active then VBool false
+          else try VarMap.find (scope^"/init") st with Not_found -> assert false)
+        nst
+    in
+    let add_subscopes active =
+      List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) ->
+        aux active (scope^"/"^ss_id) ss_eqs st nst)
+    in
+    let add_eq (st, nst) eq = match fst eq with
+      | AST_assign(vars, e) ->
+        let st, nst = add_subscopes active (st, nst) (subscopes p e) in
+        List.fold_left (fun (st, nst) (pn, pe) ->
+            let st, v = if active then eval_expr ccmap scope st pe
+              else st,
+                try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> []
+                with Not_found -> []
+            in
+            st, VarMap.add (scope^"/"^pn) (VPrevious v) nst)
+          (st, nst) (extract_pre e)
+      | AST_assume _ | AST_guarantee _ -> st, nst
+      | AST_automaton _ -> not_implemented "extract_next_state automaton"
+    in
+    List.fold_left add_eq (st, r) eqs
+  in aux active scope eqs st csts
+
+let program_init_state p root_node =
+  let (n, _) = find_node_decl p root_node in
+  let rec prog_init_state_aux st p scope eqs =
+    let st = VarMap.add (scope^"/init") (VBool true) st in
+    let add_subscopes =
+      List.fold_left (fun st (ss_id, ss_eqs, _) -> prog_init_state_aux st p (scope^"/"^ss_id) ss_eqs)
+    in
+    List.fold_left (fun st eq -> match fst eq with
+        | AST_assign(_, e) -> add_subscopes st (subscopes p e)
+        | AST_assume _ | AST_guarantee _ -> st
+        | AST_automaton _ -> not_implemented "prog_init_state_aux automaton")
+      st eqs
+  in
+    prog_init_state_aux (program_consts p) p "" n.body
+
+
+let program_step p st inputs root_node =
+  let (n, _) = find_node_decl p root_node in
+  let st = List.fold_left
+    (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in
+
+  let ccmap = build_prog_ccmap p "" n.body st in
+
+  let st = List.fold_left
+    (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st)
+    st n.ret in
+  let outputs = List.map
+    (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v))
+    n.ret in
+  let st, next_st = extract_next_state true p "" n.body st ccmap in
+
+  st, outputs, next_st
+  
+
diff --git a/libs/util.ml b/libs/util.ml
index 2150abc..cfa1619 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -17,4 +17,9 @@ let print_list x l =
     | [a] -> Format.printf "%s" a
     | p::q -> Format.printf "%s, " p; aux q
   in
-  Format.printf "["; aux l; Format.printf "]@.";
+  Format.printf "["; aux l; Format.printf "]@."
+
+let uid =
+  let c = ref 0 in
+  fun () -> c := !c + 1; string_of_int !c
+
diff --git a/main.ml b/main.ml
index 4f70229..01cccbe 100644
--- a/main.ml
+++ b/main.ml
@@ -20,6 +20,30 @@ let () =
 
     let prog = File_parser.parse_file !ifile in
     if !dump then Ast_printer.print_prog Format.std_formatter prog;
-    ()  (* nothing to do yet ... *)
+    try
+      let s0 = Interpret.program_init_state prog "test" in
+      Format.printf "Init state:@.";
+      Data.print_state s0;
+      let rec it i st =
+        let st, outputs, next_st =
+          Interpret.program_step prog st
+          ["i", Data.VInt i] "test"
+        in
+        Format.printf "@.> Step %d:@." i;
+        Data.print_state st;
+        match List.assoc "exit" outputs with
+        | Data.VBool false -> it (i+1) next_st
+        | _ -> ()
+      in
+      it 0 s0
+    with
+    | Data.Combinatorial_cycle v ->
+      Format.eprintf "Combinatorial cycle (%s)@." v
+    | Data.Type_error e ->
+      Format.eprintf "Typing error: %s@." e
+    | Data.Not_implemented l ->
+      Format.eprintf "Not implemented: %s@." l
+    | Data.No_variable id ->
+      Format.eprintf "No such variable: %s@." id
     
 
diff --git a/tests/tests/test0.scade b/tests/tests/test0.scade
index a8dddf7..3d03be5 100644
--- a/tests/tests/test0.scade
+++ b/tests/tests/test0.scade
@@ -1,4 +1,7 @@
-node test0(i: int) returns(probe j: int)
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
-    j = i;
+    exit = i >= 5;
+    a = i;
+    b = 0;
+    c = 0;
 tel
diff --git a/tests/tests/test1.scade b/tests/tests/test1.scade
index db1d6bc..350b920 100644
--- a/tests/tests/test1.scade
+++ b/tests/tests/test1.scade
@@ -1,5 +1,8 @@
-node test1(i: int) returns(probe j: int)
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
     assume i_pos : i >= 0;
-    j = i;
+    exit = i >= 5;
+    a = i;
+    b = 0;
+    c = 0;
 tel
diff --git a/tests/tests/test2.scade b/tests/tests/test2.scade
index 2db6cf5..1777689 100644
--- a/tests/tests/test2.scade
+++ b/tests/tests/test2.scade
@@ -1,5 +1,8 @@
-node test2(i: int) returns(probe j: int)
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
     assume i_pos : i >= 0;
-    j = if i < 0 then 42 else 12;
+    exit = i >= 5;
+    a = if i < 0 then 42 else 12;
+    b = 0;
+    c = 0;
 tel
diff --git a/tests/tests/test3.scade b/tests/tests/test3.scade
index d133be7..9380a49 100644
--- a/tests/tests/test3.scade
+++ b/tests/tests/test3.scade
@@ -1,4 +1,7 @@
-node test3(i: int) returns(probe j: int)
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
-    j = if i < 0 then -i else i;
+    exit = i >= 5;
+    a = if i < 0 then -i else i;
+    b = 0;
+    c = 0;
 tel
diff --git a/tests/tests/test4.scade b/tests/tests/test4.scade
index 8c5bf2d..c66a56f 100644
--- a/tests/tests/test4.scade
+++ b/tests/tests/test4.scade
@@ -1,4 +1,7 @@
-node test4() returns(probe j: int)
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
-    j = 0 -> (if pre j > 10 then 0 else pre j + 1);
+    exit = i >= 5;
+    a = 0 -> (if pre a > 10 then 0 else pre a + 1);
+    b = 0 -> pre i;
+    c = 0;
 tel
diff --git a/tests/tests/test5.scade b/tests/tests/test5.scade
index 403a069..1de390d 100644
--- a/tests/tests/test5.scade
+++ b/tests/tests/test5.scade
@@ -1,7 +1,8 @@
-node test5() returns(probe j: int)
-var p: int;
+node test(i: int) returns(probe a, b, c: int; exit: bool)
 let
-    p = 0 -> pre j;
-    j = if p > 10 then 0 else p + 1;
+    b = 0 -> pre a;
+    a = if b > 4 then 0 else b + 1;
+    c = 0;   
+    exit = i >= 10;
 tel
 
diff --git a/tests/tests/test6.scade b/tests/tests/test6.scade
index a8d6cfe..574e271 100644
--- a/tests/tests/test6.scade
+++ b/tests/tests/test6.scade
@@ -1,6 +1,9 @@
-node test6(probe i: int) returns(probe j: int)
+node test(probe i: int) returns(probe a, b, c: int; exit: bool)
 let
     assume i_bounded : i >= -10 and i <= 10;
-    j = i;
-    guarantee j_eq_i : j = i;
+    a = i;
+    guarantee a_eq_i : a = i;
+    b = 0;
+    c = 0;
+    exit = i >= 5;
 tel
diff --git a/tests/tests/test7.scade b/tests/tests/test7.scade
index 4bd49b9..c756a9e 100644
--- a/tests/tests/test7.scade
+++ b/tests/tests/test7.scade
@@ -1,4 +1,7 @@
-node test7() returns(probe c: int)
+node test(i: int) returns(a, b, probe c: int; exit: bool)
 let
+    a = 0;
+    b = 0;
     c = 0 -> (pre c + 1);
+    exit = i >= 5;
 tel
diff --git a/tests/tests/testc.scade b/tests/tests/testc.scade
new file mode 100644
index 0000000..7c99b32
--- /dev/null
+++ b/tests/tests/testc.scade
@@ -0,0 +1,11 @@
+const x : int = 12;
+const y : int = z + 3;
+const z : int = x * 2;
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+let
+  exit = true;
+  a = x;
+  b = y;
+  c = z;
+tel
diff --git a/tests/updown.scade b/tests/updown.scade
index 02e2029..089293a 100644
--- a/tests/updown.scade
+++ b/tests/updown.scade
@@ -4,19 +4,15 @@ node updown() returns(probe x: int)
 var last_x: int;
 let
     last_x = 0 -> pre x;
-    guarantee x_bounded : x >= -bound and x <= bound;
+    guarantee x_bounded: x >= -bound and x <= bound;
     automaton
         initial state UP
         let x = last_x + 1; tel
-        until if x >= bound
-            do guarantee x_up : x = bound;
-            resume DOWN;
+        until if x >= bound resume DOWN;
 
         state DOWN
         let x = last_x - 1; tel
-        until if x <= -bound
-            do guarantee x_down : x = -bound;
-            resume UP;
+        until if x <= -bound resume UP;
 
     returns x;
 tel