diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 11 | ||||
| -rw-r--r-- | abstract/transform.ml | 6 |
2 files changed, 12 insertions, 5 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 |