diff options
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | frontend/ast.ml | 17 | ||||
-rw-r--r-- | frontend/ast_printer.ml | 1 | ||||
-rw-r--r-- | frontend/file_parser.ml | 10 | ||||
-rw-r--r-- | frontend/lexer.mll | 1 | ||||
-rw-r--r-- | frontend/parser.mly | 9 | ||||
-rw-r--r-- | interpret/ast_util.ml | 35 | ||||
-rw-r--r-- | interpret/data.ml | 12 | ||||
-rw-r--r-- | interpret/interpret.ml | 43 | ||||
-rw-r--r-- | interpret/sca.ml | 101 | ||||
-rw-r--r-- | libs/util.ml | 25 | ||||
-rw-r--r-- | main.ml | 25 | ||||
-rw-r--r-- | tests/Makefile | 13 | ||||
-rw-r--r-- | tests/count.scade | 36 | ||||
-rw-r--r-- | tests/merge.scade | 22 | ||||
-rw-r--r-- | tests/result/limiter.out | 31 | ||||
-rw-r--r-- | tests/result/limitera.out | 31 | ||||
-rw-r--r-- | tests/result/locals.out | 13 | ||||
-rw-r--r-- | tests/result/test0.out | 6 | ||||
-rw-r--r-- | tests/result/test1.out | 6 | ||||
-rw-r--r-- | tests/result/test2.out | 6 | ||||
-rw-r--r-- | tests/result/test3.out | 6 | ||||
-rw-r--r-- | tests/result/test4.out | 6 | ||||
-rw-r--r-- | tests/result/test5.out | 11 | ||||
-rw-r--r-- | tests/result/test6.out | 6 | ||||
-rw-r--r-- | tests/result/test7.out | 6 | ||||
-rw-r--r-- | tests/result/testc.out | 1 | ||||
-rw-r--r-- | tests/result/train.out | 101 | ||||
-rw-r--r-- | tests/result/updown.out | 31 | ||||
-rw-r--r-- | tests/source/limiter.scade (renamed from tests/limiter.scade) | 0 | ||||
-rw-r--r-- | tests/source/limitera.scade (renamed from tests/limitera.scade) | 0 | ||||
-rw-r--r-- | tests/source/locals.scade | 20 | ||||
-rw-r--r-- | tests/source/test0.scade | 7 | ||||
-rw-r--r-- | tests/source/test1.scade (renamed from tests/tests/test1.scade) | 2 | ||||
-rw-r--r-- | tests/source/test2.scade (renamed from tests/tests/test2.scade) | 2 | ||||
-rw-r--r-- | tests/source/test3.scade (renamed from tests/tests/test3.scade) | 2 | ||||
-rw-r--r-- | tests/source/test4.scade (renamed from tests/tests/test4.scade) | 0 | ||||
-rw-r--r-- | tests/source/test5.scade (renamed from tests/tests/test5.scade) | 0 | ||||
-rw-r--r-- | tests/source/test6.scade (renamed from tests/tests/test6.scade) | 2 | ||||
-rw-r--r-- | tests/source/test7.scade (renamed from tests/tests/test7.scade) | 0 | ||||
-rw-r--r-- | tests/source/testc.scade (renamed from tests/tests/testc.scade) | 4 | ||||
-rw-r--r-- | tests/source/train.scade (renamed from tests/train.scade) | 14 | ||||
-rw-r--r-- | tests/source/updown.scade (renamed from tests/updown.scade) | 0 | ||||
-rw-r--r-- | tests/tests/test0.scade | 7 |
44 files changed, 521 insertions, 153 deletions
@@ -9,7 +9,8 @@ SRC= main.ml \ frontend/lexer.mll \ frontend/ast_printer.ml \ interpret/data.ml \ - interpret/interpret.ml + interpret/interpret.ml \ + interpret/sca.ml all: $(BIN) diff --git a/frontend/ast.ml b/frontend/ast.ml index cf04166..8392bc6 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -1,10 +1,6 @@ open Lexing +open Util -type position = Lexing.position -let position_unknown = Lexing.dummy_pos - -type extent = position * position -let extent_unknown = (position_unknown, position_unknown) type 'a ext = 'a * extent @@ -44,6 +40,7 @@ type bin_bool_op = type expr = | AST_identifier of id ext + | AST_idconst of id ext (* on numerical values *) | AST_int_const of string ext | AST_real_const of string ext @@ -74,13 +71,13 @@ and state = { and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *) and activate_block = { - id : id; - locals : var_def list; - body : eqn ext list; + id : id; + locals : var_def list; + body : eqn ext list; } and activate_if = - | AST_activate_body of activate_block - | AST_activate_if of expr ext * activate_if * activate_if + | AST_activate_body of activate_block + | AST_activate_if of expr ext * activate_if * activate_if and activate = activate_if * id list and eqn = diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 25b1c11..edd27e9 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -152,6 +152,7 @@ let rec print_expr fmt e = print_expr c print_expr t print_expr e | AST_identifier (v,_) -> print_id fmt v + | AST_idconst (v,_) -> print_id fmt v | AST_instance ((i,_),l, _) -> Format.fprintf fmt "%a(%a)" diff --git a/frontend/file_parser.ml b/frontend/file_parser.ml index 672c695..85eb9cd 100644 --- a/frontend/file_parser.ml +++ b/frontend/file_parser.ml @@ -10,10 +10,8 @@ let parse_file (filename : string) : prog = Parser.file Lexer.token lex with | Parser.Error -> - Printf.eprintf "Parse error (invalid syntax) near %s\n" - (string_of_position lex.lex_start_p); - failwith "Parse error" + Util.error (Printf.sprintf "Parse error (invalid syntax) near %s" + (string_of_position lex.lex_start_p)) | Failure "lexing: empty token" -> - Printf.eprintf "Parse error (invalid token) near %s\n" - (string_of_position lex.lex_start_p); - failwith "Parse error" + Util.error (Printf.sprintf "Parse error (invalid token) near %s" + (string_of_position lex.lex_start_p)) diff --git a/frontend/lexer.mll b/frontend/lexer.mll index 8a4ef26..ef40aa7 100644 --- a/frontend/lexer.mll +++ b/frontend/lexer.mll @@ -12,6 +12,7 @@ "const", CONST; "node", NODE; + "function", FUNCTION; "returns", RETURNS; "var", VAR; "let", LET; diff --git a/frontend/parser.mly b/frontend/parser.mly index ec283c3..2483f09 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -9,7 +9,7 @@ open Util %token IF THEN ELSE %token NOT AND OR %token MOD -%token CONST NODE RETURNS +%token CONST NODE FUNCTION RETURNS %token VAR LET TEL %token PRE %token ASSUME GUARANTEE @@ -188,8 +188,11 @@ var_decl: | VAR l=nonempty_list(terminated(vari, SEMICOLON)) { List.flatten l } +node_kw: +| NODE {} +| FUNCTION {} node_decl: -| NODE id=IDENT LPAREN v=vars RPAREN +| node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN e = dbody { { name = id; @@ -198,7 +201,7 @@ node_decl: var = []; body = e; } } -| NODE id=IDENT LPAREN v=vars RPAREN +| node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN lv=var_decl b=body diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml new file mode 100644 index 0000000..db9a76f --- /dev/null +++ b/interpret/ast_util.ml @@ -0,0 +1,35 @@ +open Ast +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 + +let extract_const_decls = + List.fold_left + (fun l d -> match d with + | AST_const_decl d -> d::l + | _ -> l) + [] + +(* Some errors *) + +let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v) +let no_variable e = error ("No such variable: " ^ e) +let type_error e = error ("Type error: " ^ e) +let not_implemented e = error ("Not implemented: " ^ e) + diff --git a/interpret/data.ml b/interpret/data.ml index 51afcc3..cf7d820 100644 --- a/interpret/data.ml +++ b/interpret/data.ml @@ -2,13 +2,7 @@ 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) +open Ast_util type scope = string @@ -38,10 +32,10 @@ let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) = let r = f (VarMap.add id VBusy st) c in (* Format.printf "]%s " id; *) r - with Not_found -> raise (No_variable id) + with Not_found -> no_variable id in match VarMap.find id st with - | VBusy -> raise (Combinatorial_cycle id) + | VBusy -> combinatorial_cycle id | v -> st, v (* pretty-printing *) diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 373ed5f..6ff125c 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -1,32 +1,17 @@ open Ast open Data open Util +open Ast_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 - -(* Utility : build subscopes of equation ; extract pre declarations *) +(* 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_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] + | 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) -> @@ -41,7 +26,8 @@ let rec subscopes p e = match fst e with (* 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_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) -> @@ -69,13 +55,13 @@ 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_identifier (id, _) | AST_idconst(id, _) -> let rec aux = function | [] -> let st, v = get_var st env.c ("cst/"^id) in st, [v] | sc::q -> try let st, v = get_var st env.c (sc^"/"^id) in st, [v] - with No_variable _ -> aux q + with _ -> aux q in aux env.scopes (* on numerical values *) | AST_int_const (i, _) -> st, [VInt (int_of_string i)] @@ -172,18 +158,13 @@ let rec calc_const p d st c = | _ -> 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 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.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.name) in st) VarMap.empty cdecl @@ -211,8 +192,8 @@ let program_init_state p root_node = in aux (program_consts p) p "" n.body -(* Program execution *) +(* Program execution *) (* build calc map *) let rec build_prog_ccmap p scopes eqs st = diff --git a/interpret/sca.ml b/interpret/sca.ml new file mode 100644 index 0000000..4a012ae --- /dev/null +++ b/interpret/sca.ml @@ -0,0 +1,101 @@ +(* Scope analyzer *) + +open Ast +open Util +open Ast_util + +type renaming = (id * bool) VarMap.t + +(* consts_renaming : prog -> renaming *) +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) + VarMap.empty + cdecl + +(* add_var_defs : string -> renaming -> var_def list -> renaming *) +let add_var_defs prefix = + List.fold_left + (fun rn (_,(n,_),_) -> VarMap.add n (prefix^n, false) rn) + +(* rename_expr : expr ext -> renaming -> expr ext *) +let rec rename_expr exp rn = + let sub e = rename_expr e rn in + let a = match fst exp with + | AST_identifier(id, l) -> + begin try let (nn, const) = VarMap.find id rn in + if const then AST_idconst(nn, l) else AST_identifier(nn, l) + with Not_found -> loc_error l no_variable id + end + | AST_idconst(id, l) -> assert false (* expression not already renamed *) + | AST_unary(op, e) -> AST_unary(op, sub e) + | AST_binary(op, a, b) -> AST_binary(op, sub a, sub b) + | AST_binary_rel(op, a, b) -> AST_binary_rel(op, sub a, sub b) + | AST_binary_bool(op, a, b) -> AST_binary_bool(op, sub a, sub b) + | AST_not(e) -> AST_not(sub e) + | AST_pre (e, x) -> AST_pre(sub e, x) + | AST_arrow(a, b) -> AST_arrow(sub a, sub b) + | AST_if(a, b, c) -> AST_if(sub a, sub b, sub c) + | AST_instance(i, l, s) -> AST_instance(i, List.map sub l, s) + | x -> x (* other cases : constant literals *) + in a, snd exp + +(* rename_var : renaming -> id -> id *) +let rename_var rn id = + try let (nn, const)= VarMap.find id rn in + if const then error ("Constant "^id^" cannot be defined in node."); + nn + with Not_found -> no_variable id + +let rename_var_ext rn (id, loc) = (rename_var rn id, loc) + +let rename_var_def rn (p, id, t) = (p, rename_var_ext rn id, t) + +(* rename_eqn : renaming -> eqn ext -> eqn ext *) +let rec rename_eqn rn e = + let a = match fst e with + | AST_assign(s, e) -> AST_assign (List.map (rename_var_ext rn) s, rename_expr e rn) + | AST_guarantee(g, e) -> AST_guarantee(g, rename_expr e rn) + | 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 + { st with + locals = List.map (rename_var_def rn) 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 + in + AST_automaton(aid, List.map rename_state states, List.map (rename_var rn) ret) + | AST_activate (c, ret) -> + let rec rename_activate_if = function + | 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 + AST_activate_body{ b with + locals = List.map (rename_var_def rn) b.locals; + body = List.map (rename_eqn rn) b.body; + } + in + AST_activate(rename_activate_if c, List.map (rename_var rn) ret) + in a, snd e + +(* rename_node : renaming -> node_decl -> node_decl *) +let rename_node const_rn node = + let rn = add_var_defs "" const_rn node.args in + let rn = add_var_defs "" rn node.ret in + let rn = add_var_defs "" rn node.var in + { node with + body = List.map (rename_eqn rn) node.body } + +(* rename_prog : prog -> prog *) +let rename_prog p = + let const_rn = consts_renaming p in + let rn_toplevel = function + | AST_node_decl (n, l) -> AST_node_decl (rename_node const_rn n, l) + | x -> x + in + List.map rn_toplevel p + diff --git a/libs/util.ml b/libs/util.ml index 522c3ec..494faac 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -1,11 +1,30 @@ -exception TypeError +(* Locations *) + +type position = Lexing.position +let position_unknown = Lexing.dummy_pos + +type extent = position * position +let extent_unknown = (position_unknown, position_unknown) + + +(* Exceptions *) + +exception NoLocError of string +let error x = raise (NoLocError x) + +exception LocError of extent list * string +let loc_error l f x = + try f x with + | NoLocError e -> raise (LocError([l], e)) + | LocError(q, e) -> raise (LocError(l::q, e)) + +(* Varmaps *) module VarMap = Mapext.Make(String) -exception Duplicate of string let disjoint_union k a b = match a, b with | Some x, None -> Some x | None, Some y -> Some y - | _ -> raise (Duplicate k) + | _ -> error ("Duplicate name in disjoint union: " ^ k) let rec fix equal f s = let fs = f s in @@ -2,6 +2,7 @@ open Ast (* command line options *) let dump = ref false +let dumprn = ref false let test = ref false let vtest = ref false let ifile = ref "" @@ -10,6 +11,7 @@ let usage = "usage: analyzer [options] file.scade" let options = [ "--dump", Arg.Set dump, "Dump program source."; + "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; "--vtest", Arg.Set vtest, "Verbose testing."; "--test", Arg.Set test, "Simple testing."; ] @@ -22,9 +24,13 @@ let () = exit 1 end; - let prog = File_parser.parse_file !ifile in - if !dump then Ast_printer.print_prog Format.std_formatter prog; try + let prog = File_parser.parse_file !ifile in + if !dump then Ast_printer.print_prog Format.std_formatter prog; + + let prog = Sca.rename_prog prog in + if !dumprn then Ast_printer.print_prog Format.std_formatter prog; + if !vtest then begin let s0 = Interpret.program_init_state prog "test" in Format.printf "Init state:@."; @@ -60,13 +66,10 @@ let () = it 0 s0 end 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 - + | Util.NoLocError e -> Format.eprintf "Error: %s@." e + | Util.LocError(l, e) -> + Format.eprintf "Error: %s@." e; + List.iter + (fun loc -> Format.eprintf "At: %s@." (Ast_printer.string_of_extent loc)) + l diff --git a/tests/Makefile b/tests/Makefile index 4073cad..d306161 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,4 +1,15 @@ -%.test: %.scade test.c +ALL_OUT=result/limiter.out result/limitera.out result/locals.out \ + result/test4.out result/test5.out result/test7.out \ + result/train.out result/updown.out \ + result/test0.out result/test1.out result/test2.out result/test3.out \ + result/test6.out result/testc.out + +bin/%.test: source/%.scade test.c rm kcg/* kcg64 -target C -node test $< gcc -o $@ test.c kcg/*.c -I./kcg + +result/%.out: bin/%.test + $< > $@ + +all: $(ALL_OUT) diff --git a/tests/count.scade b/tests/count.scade deleted file mode 100644 index c5ce47d..0000000 --- a/tests/count.scade +++ /dev/null @@ -1,36 +0,0 @@ -node count() returns (c: int) -let - c = 0 -> (1 + pre c); -tel - -node resettable_count (r: bool) returns (c: int) -let - c = (restart count every r)(); -tel - -node nat() returns (s: int) s = 1 -> (1 + pre s); - -node rst_clk(rst: bool; clock h: bool) - returns (s: int; t: int) -let - s = (restart nat every rst) (); - t = merge(h; ((restart nat every rst) (() when h)); 0 when not h); -tel - -node even_times(c: bool; i: int) returns (o: int) -let - automaton - initial state EVEN - unless if c resume ODD; - let - o = i+1; - tel - - state ODD - unless if c resume EVEN; - let - o = -2 * i; - tel - returns o; -tel - diff --git a/tests/merge.scade b/tests/merge.scade deleted file mode 100644 index 9e666a1..0000000 --- a/tests/merge.scade +++ /dev/null @@ -1,22 +0,0 @@ -type t1 = enum { True, False, Error }; - -node #pragma kcg expand #end - mm(clock clk: t1; v: int when (clk match True)) returns(r: int) -var lr: int; -let - lr = 0 -> pre r; - r = merge(clk; - v; - lr when (clk match False); - -1 when (clk match Error)); -tel - -node test(i: int) returns (a, b, c: int; exit: bool) -var clock clk: t1; -let - exit = i >= 30; - clk = if i mod 5 = 0 then True else if i mod 9 = 8 then Error else False; - a = mm(clk, i when (clk match True)); - b = if clk = True then 1 else 0; - c = if clk = Error then 1 else 0; -tel diff --git a/tests/result/limiter.out b/tests/result/limiter.out new file mode 100644 index 0000000..1851c7d --- /dev/null +++ b/tests/result/limiter.out @@ -0,0 +1,31 @@ +0. -6 16 -6 +1. 15 16 10 +2. 36 16 26 +3. 57 16 42 +4. 78 16 58 +5. 99 16 74 +6. 120 16 90 +7. -115 16 74 +8. -94 16 58 +9. -73 16 42 +10. -52 16 26 +11. -31 16 10 +12. -10 16 -6 +13. 11 16 10 +14. 32 16 26 +15. 53 16 42 +16. 74 16 58 +17. 95 16 74 +18. 116 16 90 +19. -119 16 74 +20. -98 16 58 +21. -77 16 42 +22. -56 16 26 +23. -35 16 10 +24. -14 16 -6 +25. 7 16 7 +26. 28 16 23 +27. 49 16 39 +28. 70 16 55 +29. 91 16 71 +30. 112 16 87 diff --git a/tests/result/limitera.out b/tests/result/limitera.out new file mode 100644 index 0000000..1851c7d --- /dev/null +++ b/tests/result/limitera.out @@ -0,0 +1,31 @@ +0. -6 16 -6 +1. 15 16 10 +2. 36 16 26 +3. 57 16 42 +4. 78 16 58 +5. 99 16 74 +6. 120 16 90 +7. -115 16 74 +8. -94 16 58 +9. -73 16 42 +10. -52 16 26 +11. -31 16 10 +12. -10 16 -6 +13. 11 16 10 +14. 32 16 26 +15. 53 16 42 +16. 74 16 58 +17. 95 16 74 +18. 116 16 90 +19. -119 16 74 +20. -98 16 58 +21. -77 16 42 +22. -56 16 26 +23. -35 16 10 +24. -14 16 -6 +25. 7 16 7 +26. 28 16 23 +27. 49 16 39 +28. 70 16 55 +29. 91 16 71 +30. 112 16 87 diff --git a/tests/result/locals.out b/tests/result/locals.out new file mode 100644 index 0000000..e111948 --- /dev/null +++ b/tests/result/locals.out @@ -0,0 +1,13 @@ +0. 0 0 0 +1. 0 0 0 +2. 1 0 0 +3. 2 0 0 +4. 3 0 0 +5. 5 0 0 +6. 4 0 0 +7. 6 0 0 +8. 7 0 0 +9. 8 0 0 +10. 10 0 0 +11. 9 0 0 +12. 11 0 0 diff --git a/tests/result/test0.out b/tests/result/test0.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test0.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test1.out b/tests/result/test1.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test1.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test2.out b/tests/result/test2.out new file mode 100644 index 0000000..d080f21 --- /dev/null +++ b/tests/result/test2.out @@ -0,0 +1,6 @@ +0. 12 0 0 +1. 12 0 0 +2. 12 0 0 +3. 12 0 0 +4. 12 0 0 +5. 12 0 0 diff --git a/tests/result/test3.out b/tests/result/test3.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test3.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test4.out b/tests/result/test4.out new file mode 100644 index 0000000..f5ad578 --- /dev/null +++ b/tests/result/test4.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 1 0 +3. 3 2 0 +4. 4 3 0 +5. 5 4 0 diff --git a/tests/result/test5.out b/tests/result/test5.out new file mode 100644 index 0000000..388c744 --- /dev/null +++ b/tests/result/test5.out @@ -0,0 +1,11 @@ +0. 1 0 0 +1. 2 1 0 +2. 3 2 0 +3. 4 3 0 +4. 5 4 0 +5. 0 5 0 +6. 1 0 0 +7. 2 1 0 +8. 3 2 0 +9. 4 3 0 +10. 5 4 0 diff --git a/tests/result/test6.out b/tests/result/test6.out new file mode 100644 index 0000000..fa316b4 --- /dev/null +++ b/tests/result/test6.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 1 0 0 +2. 2 0 0 +3. 3 0 0 +4. 4 0 0 +5. 5 0 0 diff --git a/tests/result/test7.out b/tests/result/test7.out new file mode 100644 index 0000000..90ae696 --- /dev/null +++ b/tests/result/test7.out @@ -0,0 +1,6 @@ +0. 0 0 0 +1. 0 0 1 +2. 0 0 2 +3. 0 0 3 +4. 0 0 4 +5. 0 0 5 diff --git a/tests/result/testc.out b/tests/result/testc.out new file mode 100644 index 0000000..5553419 --- /dev/null +++ b/tests/result/testc.out @@ -0,0 +1 @@ +0. 12 27 24 diff --git a/tests/result/train.out b/tests/result/train.out new file mode 100644 index 0000000..4af78b5 --- /dev/null +++ b/tests/result/train.out @@ -0,0 +1,101 @@ +0. 0 0 0 +1. 0 0 0 +2. 0 0 0 +3. 0 0 0 +4. 0 0 0 +5. 0 0 0 +6. 0 0 0 +7. 0 0 0 +8. 0 0 0 +9. 0 0 0 +10. 0 0 0 +11. 0 0 0 +12. 0 0 0 +13. 0 0 0 +14. 0 0 0 +15. 0 0 0 +16. 0 0 0 +17. 0 0 0 +18. 0 0 0 +19. 0 0 0 +20. 0 0 0 +21. 0 0 0 +22. 0 0 0 +23. 0 0 0 +24. 0 0 0 +25. 0 0 0 +26. 0 0 0 +27. 0 0 0 +28. 0 0 0 +29. 0 0 0 +30. 0 0 0 +31. 0 0 0 +32. 0 0 0 +33. 0 0 0 +34. 0 0 0 +35. 0 0 0 +36. 0 0 0 +37. 0 0 0 +38. 0 0 0 +39. 0 0 0 +40. 0 0 0 +41. 0 0 0 +42. 0 0 0 +43. 0 0 0 +44. 0 0 0 +45. 0 0 0 +46. 0 0 0 +47. 0 0 0 +48. 0 0 0 +49. 0 0 0 +50. 0 0 0 +51. 0 0 0 +52. 0 0 0 +53. 0 0 0 +54. 0 0 0 +55. 0 0 0 +56. 0 0 0 +57. 0 0 0 +58. 0 0 0 +59. 0 0 0 +60. 1 0 0 +61. 1 0 0 +62. 1 0 0 +63. 1 0 0 +64. 1 0 0 +65. 1 0 0 +66. 1 0 0 +67. 1 0 0 +68. 1 0 0 +69. 1 0 0 +70. 1 0 0 +71. 1 0 0 +72. 1 0 0 +73. 1 0 0 +74. 1 0 0 +75. 1 0 0 +76. 1 0 0 +77. 1 0 0 +78. 1 0 0 +79. 1 0 0 +80. 1 0 0 +81. 1 0 0 +82. 1 0 0 +83. 1 0 0 +84. 1 0 0 +85. 1 0 0 +86. 1 0 0 +87. 1 0 0 +88. 1 0 0 +89. 1 0 0 +90. 1 0 0 +91. 1 0 0 +92. 1 0 0 +93. 1 0 0 +94. 1 0 0 +95. 1 0 0 +96. 1 0 0 +97. 1 0 0 +98. 1 0 0 +99. 1 0 0 +100. 1 0 0 diff --git a/tests/result/updown.out b/tests/result/updown.out new file mode 100644 index 0000000..89e38ca --- /dev/null +++ b/tests/result/updown.out @@ -0,0 +1,31 @@ +0. 1 0 0 +1. 2 0 0 +2. 3 0 0 +3. 4 0 0 +4. 5 0 0 +5. 6 0 0 +6. 7 0 0 +7. 6 0 0 +8. 5 0 0 +9. 4 0 0 +10. 3 0 0 +11. 2 0 0 +12. 1 0 0 +13. 0 0 0 +14. -1 0 0 +15. -2 0 0 +16. -3 0 0 +17. -4 0 0 +18. -5 0 0 +19. -6 0 0 +20. -7 0 0 +21. -6 0 0 +22. -5 0 0 +23. -4 0 0 +24. -3 0 0 +25. -2 0 0 +26. -1 0 0 +27. 0 0 0 +28. 1 0 0 +29. 2 0 0 +30. 3 0 0 diff --git a/tests/limiter.scade b/tests/source/limiter.scade index a611d98..a611d98 100644 --- a/tests/limiter.scade +++ b/tests/source/limiter.scade diff --git a/tests/limitera.scade b/tests/source/limitera.scade index 1e4927e..1e4927e 100644 --- a/tests/limitera.scade +++ b/tests/source/limitera.scade diff --git a/tests/source/locals.scade b/tests/source/locals.scade new file mode 100644 index 0000000..379cbde --- /dev/null +++ b/tests/source/locals.scade @@ -0,0 +1,20 @@ +node test(i: int) returns(a, b, c: int; exit: bool) +let + activate + if i mod 5 = 0 then + var x: int; + let + x = i; + a = x; + tel + else + var x: int; + let + x = (0 -> pre i); + a = x; + tel + returns a; + b = 0; + c = 0; + exit = i >= 12; +tel diff --git a/tests/source/test0.scade b/tests/source/test0.scade new file mode 100644 index 0000000..65a5331 --- /dev/null +++ b/tests/source/test0.scade @@ -0,0 +1,7 @@ +function test(i: int) returns(probe a, b, c: int; exit: bool) +let + exit = i >= 5; + a = i; + b = 0; + c = 0; +tel diff --git a/tests/tests/test1.scade b/tests/source/test1.scade index 350b920..f247a57 100644 --- a/tests/tests/test1.scade +++ b/tests/source/test1.scade @@ -1,4 +1,4 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) +function test(i: int) returns(probe a, b, c: int; exit: bool) let assume i_pos : i >= 0; exit = i >= 5; diff --git a/tests/tests/test2.scade b/tests/source/test2.scade index 1777689..28a3e2d 100644 --- a/tests/tests/test2.scade +++ b/tests/source/test2.scade @@ -1,4 +1,4 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) +function test(i: int) returns(probe a, b, c: int; exit: bool) let assume i_pos : i >= 0; exit = i >= 5; diff --git a/tests/tests/test3.scade b/tests/source/test3.scade index 9380a49..541b9f5 100644 --- a/tests/tests/test3.scade +++ b/tests/source/test3.scade @@ -1,4 +1,4 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) +function test(i: int) returns(probe a, b, c: int; exit: bool) let exit = i >= 5; a = if i < 0 then -i else i; diff --git a/tests/tests/test4.scade b/tests/source/test4.scade index c66a56f..c66a56f 100644 --- a/tests/tests/test4.scade +++ b/tests/source/test4.scade diff --git a/tests/tests/test5.scade b/tests/source/test5.scade index 1de390d..1de390d 100644 --- a/tests/tests/test5.scade +++ b/tests/source/test5.scade diff --git a/tests/tests/test6.scade b/tests/source/test6.scade index 574e271..e3257cc 100644 --- a/tests/tests/test6.scade +++ b/tests/source/test6.scade @@ -1,4 +1,4 @@ -node test(probe i: int) returns(probe a, b, c: int; exit: bool) +function test(probe i: int) returns(probe a, b, c: int; exit: bool) let assume i_bounded : i >= -10 and i <= 10; a = i; diff --git a/tests/tests/test7.scade b/tests/source/test7.scade index c756a9e..c756a9e 100644 --- a/tests/tests/test7.scade +++ b/tests/source/test7.scade diff --git a/tests/tests/testc.scade b/tests/source/testc.scade index 7c99b32..40a04d3 100644 --- a/tests/tests/testc.scade +++ b/tests/source/testc.scade @@ -2,9 +2,9 @@ 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) +function test(i: int) returns (a, b, c: int; exit: bool) let - exit = true; + exit = i >= 0; a = x; b = y; c = z; diff --git a/tests/train.scade b/tests/source/train.scade index d91df01..c51971e 100644 --- a/tests/train.scade +++ b/tests/source/train.scade @@ -16,22 +16,22 @@ let automaton initial state NotEarly - unless if advance > 10 resume Early; let early = false; tel + until if advance >= 10 resume Early; state Early - unless if advance = 0 resume NotEarly; let early = true; tel + until if advance = 0 resume NotEarly; returns early; automaton initial state NotLate - unless if advance < -10 resume Late; let late = false; tel + until if advance <= -10 resume Late; state Late - unless if advance = 0 resume NotLate; let late = true; tel + until if advance = 0 resume NotLate; returns late; tel @@ -41,12 +41,12 @@ let ontime = not (late or early); automaton initial state Ok - unless if early resume Early; let alarm = false; tel + until if early resume Early; state Early - unless if ontime resume Ok; - let alarm = late; tel + let alarm = late and not early; tel + until if ontime resume Ok; returns alarm; tel diff --git a/tests/updown.scade b/tests/source/updown.scade index 089293a..089293a 100644 --- a/tests/updown.scade +++ b/tests/source/updown.scade diff --git a/tests/tests/test0.scade b/tests/tests/test0.scade deleted file mode 100644 index 3d03be5..0000000 --- a/tests/tests/test0.scade +++ /dev/null @@ -1,7 +0,0 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) -let - exit = i >= 5; - a = i; - b = 0; - c = 0; -tel |