diff options
| -rw-r--r-- | abstract/abs_interp_edd.ml | 11 | ||||
| -rw-r--r-- | abstract/transform.ml | 6 | ||||
| -rw-r--r-- | frontend/lexer.mll | 6 | ||||
| -rw-r--r-- | main.ml | 2 | ||||
| -rw-r--r-- | tests/source/NestedControl.scade | 8 | ||||
| -rw-r--r-- | tests/source/counters.scade | 38 | ||||
| -rw-r--r-- | tests/source/test5.scade | 4 |
7 files changed, 63 insertions, 12 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index c1fb905..35bdbfb 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -597,7 +597,7 @@ end = struct ve : varenv; (* program expressions *) - init_f : bool_expr; + init_cl : conslist; cl : conslist; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -933,6 +933,7 @@ end = struct let cl = Formula.conslist_of_f f in let cl_g = Formula.conslist_of_f f_g in + let init_cl = Formula.conslist_of_f init_f in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in @@ -975,6 +976,9 @@ end = struct (List.filter (fun n -> is_suffix n "init") evars)) in let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v])) (List.filter (fun n -> is_suffix n "state") evars)) in + let lv_f = lv_f @ + (List.map (fun v -> (0.7, [v; "L"^v])) + (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in let evars_ord = if true then time "FORCE" (fun () -> force_ordering evars lv_f) @@ -1010,7 +1014,7 @@ end = struct { rp; opt; ve; last_vars; all_vars; - init_f; cl; cl_g; guarantees; + init_cl; cl; cl_g; guarantees; cycle; forget } @@ -1092,8 +1096,9 @@ end = struct end in + Format.printf "Calculating initial state...@."; let init_acc = edd_star_new (edd_bot e.ve) - (pass_cycle e (edd_apply_cl (edd_top e.ve) (conslist_of_f e.init_f))) in + (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in (* Dump final state *) let acc = ch_it 0 init_acc in diff --git a/abstract/transform.ml b/abstract/transform.ml index 17fd064..480705f 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -143,6 +143,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = and f_of_bexpr td (node, prefix, clock_scope) where expr = let sub = f_of_bexpr td (node, prefix, clock_scope) in let sub_id = sub (fun x -> x) in + let le = loc_error (snd expr) in match fst expr with | AST_bool_const b -> where (BConst b) | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b)) @@ -159,7 +160,8 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | AST_NE -> E_NE | _ -> type_error "Invalid operator on enumerated values." in f_e_op eop x y - | _ -> invalid_arity "Binary operator") + | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator." + | _ -> le invalid_arity "Binary operator") (AST_tuple [a; b], snd expr)) (* Temporal *) | AST_arrow(a, b) -> @@ -187,7 +189,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = | _ -> assert false in f_of_neexpr td (node, prefix, clock_scope) ff expr - | _ -> type_error "Expected boolean value." + | _ -> le type_error "Expected boolean value." and f_of_expr td (node, prefix, clock_scope) expr = f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr diff --git a/frontend/lexer.mll b/frontend/lexer.mll index ef40aa7..837ee75 100644 --- a/frontend/lexer.mll +++ b/frontend/lexer.mll @@ -88,6 +88,7 @@ rule token = parse | const_real as c { REALVAL c } (* spaces, comments *) | "(*" { comment lexbuf; token lexbuf } + | "/*" { cppcomment lexbuf; token lexbuf } | "--" [^ '\n' '\r']* { token lexbuf } | newline { new_line lexbuf; token lexbuf } | space { token lexbuf } @@ -98,3 +99,8 @@ and comment = parse | "*)" { () } | [^ '\n' '\r'] { comment lexbuf } | newline { new_line lexbuf; comment lexbuf } + +and cppcomment = parse + | "*/" { () } + | [^ '\n' '\r'] { cppcomment lexbuf } + | newline { new_line lexbuf; cppcomment lexbuf } @@ -29,7 +29,7 @@ let ai_rel = ref false let ai_itv_edd = ref false let ai_rel_edd = ref false let ai_root = ref "test" -let ai_widen_delay = ref 3 +let ai_widen_delay = ref 5 let ai_no_time_scopes = ref "" let ai_init_scopes = ref "" let ai_disj_v = ref "" diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade index 2551eb6..af4fdab 100644 --- a/tests/source/NestedControl.scade +++ b/tests/source/NestedControl.scade @@ -1,13 +1,13 @@ node root(In : int; C : bool) returns (Out, Out1 : int) var last_Out, last_Out1: int; - isp, isn: bool; + disj, disj2: bool; let last_Out = 0 -> pre Out; last_Out1 = 0 -> pre Out1; - isp = In > 0; - isn = In < 0; - assume C_in_not_null: (not C) or isp or isn; + disj = In > 0; + disj2 = In < 0; + assume C_in_not_null: (not C) or disj or disj2; automaton SM1 initial state State1 diff --git a/tests/source/counters.scade b/tests/source/counters.scade new file mode 100644 index 0000000..334bca1 --- /dev/null +++ b/tests/source/counters.scade @@ -0,0 +1,38 @@ +/* + x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0 | 1 | 2 | ... | 10 | ... + y = 0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0 | ... + + b1 = t | f | f | f | f | f | ... | f | f | f | ... | t | ... + b2 = t | f | f | f | f | f | ... | f | f | f | ... | t | ... + + eq* = t | t | t | t | t | t | ... | t | t | t | ... | t | ... +*/ + + +-- type t2 = subrange [0,10] of int; + +const bound: int = 1000; + +node counters(z: bool) returns (eq_nind : bool ; probe x, probe y : int) +var + b1, b2 : bool; + a, b : bool; +let + + a = false -> (if pre a then pre x < bound else pre x <= 0); + --a = false -> pre(if a then x < bound else x <= 0); + x = bound -> (if a then pre x + 1 else pre x - 1); + + b = true -> (if pre b then pre y < bound else pre y <= 0); + --b = true -> pre(if b then y < bound else y <= 0); + y = 0 -> (if b then pre y + 1 else pre y - 1); + + b1 = x=bound; + b2 = y=0; + + + guarantee xy : x+y = bound; + guarantee bb : b1 = b2; + guarantee rp : -bound <= (x-y) and (x-y) <= bound; + +tel diff --git a/tests/source/test5.scade b/tests/source/test5.scade index 1de390d..566acf0 100644 --- a/tests/source/test5.scade +++ b/tests/source/test5.scade @@ -1,8 +1,8 @@ -node test(i: int) returns(probe a, b, c: int; exit: bool) +node test(i: int) returns(probe a, probe b, probe c: int; exit: bool) let b = 0 -> pre a; a = if b > 4 then 0 else b + 1; - c = 0; + c = i; exit = i >= 10; tel |