diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | frontend/ast.ml | 25 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 38 | ||||
| -rw-r--r-- | frontend/lexer.mll | 51 | ||||
| -rw-r--r-- | frontend/parser.mly | 41 | ||||
| -rw-r--r-- | interpret/data.ml | 61 | ||||
| -rw-r--r-- | interpret/interpret.ml | 273 | ||||
| -rw-r--r-- | libs/util.ml | 7 | ||||
| -rw-r--r-- | main.ml | 26 | ||||
| -rw-r--r-- | tests/tests/test0.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test1.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test2.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test3.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test4.scade | 7 | ||||
| -rw-r--r-- | tests/tests/test5.scade | 9 | ||||
| -rw-r--r-- | tests/tests/test6.scade | 9 | ||||
| -rw-r--r-- | tests/tests/test7.scade | 5 | ||||
| -rw-r--r-- | tests/tests/testc.scade | 11 | ||||
| -rw-r--r-- | tests/updown.scade | 10 |
19 files changed, 533 insertions, 74 deletions
@@ -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 + @@ -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 |