summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml27
-rw-r--r--abstract/formula.ml20
-rw-r--r--abstract/formula_printer.ml5
-rw-r--r--abstract/nonrelational.ml7
-rw-r--r--abstract/transform.ml106
5 files changed, 105 insertions, 60 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 4c3fddb..feaf037 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -9,12 +9,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
type st
- val do_prog : prog -> id -> unit
+ val do_prog : int -> prog -> id -> unit
end = struct
type st = {
p : prog;
+ widen_delay : int;
root_scope : scope;
all_vars : var_def list;
env : E.t;
@@ -69,7 +70,7 @@ end = struct
(List.flatten (List.map vars_of_eq eqs))
(* init state *)
- let init_state p root =
+ let init_state widen_delay p root =
let root_scope = get_root_scope p root in
let f = Formula.eliminate_not (Transform.f_of_prog p root) in
@@ -86,11 +87,11 @@ end = struct
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
- Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+ Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
let env = E.apply_f env init_f in
- { p; root_scope; f; cl; all_vars; env }
+ { p; root_scope; widen_delay; f; cl; all_vars; env }
(*
pass_cycle : var_def list -> E.t -> E.t
@@ -121,13 +122,12 @@ end = struct
(* cycle : st -> cl -> env -> env *)
let cycle st cl i =
- E.apply_cl (pass_cycle st.all_vars i) cl
+ (pass_cycle st.all_vars (E.apply_cl i cl))
(*
loop : st -> cl -> env -> env -> env
*)
let loop st cycle_cl pnew stay =
- let pnew = E.apply_cl pnew cycle_cl in
Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
Formula_printer.print_conslist cycle_cl
@@ -142,10 +142,9 @@ end = struct
E.join acc0 j
in
- let widen_delay = 10 in
let rec iter n i =
let i' =
- if n < widen_delay
+ if n < st.widen_delay
then E.join i (fsharp i)
else E.widen i (fsharp i)
in
@@ -159,21 +158,23 @@ end = struct
(*
do_prog : prog -> id -> unit
*)
- let do_prog p root =
- let st = init_state p root in
+ let do_prog widen_delay p root =
+ let st = init_state widen_delay p root in
let pnew = st.env in
let stay = loop st st.cl pnew (E.vbottom pnew) in
- Format.printf "@[<hov>Final stay %a@]@."
- E.print_all stay;
+ let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+
+ Format.printf "@[<hov>Final %a@]@."
+ E.print_all final;
Format.printf "Probes:@[<hov>";
List.iter (fun (p, id, _) ->
if p then Format.printf "@ %a ∊ %a,"
Formula_printer.print_id id
- E.print_itv (E.var_itv stay id))
+ E.print_itv (E.var_itv final id))
st.all_vars;
Format.printf "@]@."
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 262bccb..44495c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -12,17 +12,31 @@ type num_expr =
(* identifier *)
| NIdent of id
+
type bool_expr =
(* constants *)
| BConst of bool
(* operators from numeric values to boolean values *)
| BRel of binary_rel_op * num_expr * num_expr
+ | BBoolEq of id * bool
(* boolean operators *)
| BAnd of bool_expr * bool_expr
| BOr of bool_expr * bool_expr
| BNot of bool_expr
+let f_and a b = match a, b with
+ | BConst false, _ | _, BConst false -> BConst false
+ | BConst true, b -> b
+ | a, BConst true -> a
+ | a, b -> BAnd(a, b)
+
+let f_or a b = match a, b with
+ | BConst true, _ | _, BConst true -> BConst true
+ | BConst false, b -> b
+ | a, BConst false -> a
+ | a, b -> BOr(a, b)
+
(* Write all formula without using the NOT operator *)
@@ -33,6 +47,7 @@ let rec eliminate_not = function
| x -> x
and eliminate_not_negate = function
| BConst x -> BConst(not x)
+ | BBoolEq(id, v) -> BBoolEq(id, not v)
| BNot e -> eliminate_not e
| BRel(r, a, b) ->
let r' = match r with
@@ -83,6 +98,11 @@ let rec conslist_of_f = function
in [cons], CLTrue
| BConst x ->
[], if x then CLTrue else CLFalse
+ | BBoolEq(id, v) ->
+ if v then
+ [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
+ else
+ [NIdent id, CONS_EQ], CLTrue
| BOr(a, b) ->
let ca, ra = conslist_of_f a in
let cb, rb = conslist_of_f b in
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 53a9b6a..1b31ba1 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -60,6 +60,11 @@ let rec print_num_expr fmt e = match e with
let rec print_bool_expr fmt e = match e with
| BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
+ | BBoolEq(id, v) ->
+ if v then
+ Format.fprintf fmt "%a" print_id id
+ else
+ Format.fprintf fmt "¬%a" print_id id
| BRel(op, a, b) ->
print_ch fmt print_num_expr ne_prec a be_prec e;
Format.fprintf fmt "@ %s " (string_of_binary_rel op);
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 3cdcc31..855f970 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -215,14 +215,15 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
List.iteri
(fun j (v, ids) ->
if j > 0 then Format.fprintf fmt "@ ";
+ Format.fprintf fmt "@[<hov 4>";
List.iteri
(fun i id ->
- if i > 0 then Format.fprintf fmt ", ";
+ if i > 0 then Format.fprintf fmt ",@ ";
Format.fprintf fmt "%a" Formula_printer.print_id id)
ids;
match V.as_const v with
- | Some i -> Format.fprintf fmt " = %d" i
- | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v))
+ | Some i -> Format.fprintf fmt " = %d@]" i
+ | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
sbl;
Format.fprintf fmt " }@]"
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b141cc6..87da1bd 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,11 +18,6 @@ type transform_data = {
(* future : the automata state *)
}
-let f_and a b =
- if a = BConst true then b
- else if b = BConst true then a
- else BAnd(a, b)
-
(* f_of_nexpr :
transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
@@ -55,48 +50,76 @@ let rec f_of_nexpr td (node, prefix) where expr =
(* temporal *)
| AST_pre(_, id) -> where [NIdent id]
| AST_arrow(a, b) ->
- BOr(
- BAnd(BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0),
- sub where a),
- BAnd(BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1),
- sub where b))
+ f_or
+ (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+ (sub where a))
+ (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+ (sub where b))
(* other *)
| AST_if(c, a, b) ->
- BOr(
- BAnd(f_of_bexpr td (node, prefix) c, sub where a),
- BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b))
+ f_or
+ (f_and (f_of_expr td (node, prefix) c) (sub where a))
+ (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
| AST_instance ((f, _), args, nid) ->
let (n, _) = find_node_decl td.p f in
where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
(* boolean values treated as integers *)
| _ ->
- BOr(
- BAnd ((f_of_bexpr td (node, prefix) expr), where [NIntConst 1]),
- BAnd (BNot(f_of_bexpr td (node, prefix) expr), where [NIntConst 0])
- )
+ f_or
+ (f_and ((f_of_expr td (node, prefix) expr)) (where [NIntConst 1]))
+ (f_and (BNot(f_of_expr td (node, prefix) expr)) (where [NIntConst 0]))
+
-(* f_of_expr :
+(*
+ f_of_expr :
transform_data -> (string, string) -> expr -> bool_expr
+ f_of_bexpr :
+ transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a
*)
-and f_of_bexpr td (node, prefix) expr =
+and f_of_bexpr td (node, prefix) where expr =
let sub = f_of_bexpr td (node, prefix) in
match fst expr with
- | AST_bool_const b -> BConst b
- | AST_binary_bool(AST_AND, a, b) -> BAnd(sub a, sub b)
- | AST_binary_bool(AST_OR, a, b) -> BOr(sub a, sub b)
- | AST_not(a) -> BNot(sub a)
+ | AST_bool_const b -> where (BConst b)
+ | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b)
+ | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b)
+ | AST_not(a) -> BNot(sub where a)
| AST_binary_rel(rel, a, b) ->
- f_of_nexpr td (node, prefix)
- (function
- | [x] -> f_of_nexpr td (node, prefix)
- (function
- | [y] -> BRel(rel, x, y)
- | _ -> invalid_arity "boolean relation") b
- | _ -> invalid_arity "boolean relation")
- a
- | _ -> loc_error (snd expr) error "Invalid type : expected boolean value"
-
+ where
+ (f_of_nexpr td (node, prefix)
+ (function
+ | [x] -> f_of_nexpr td (node, prefix)
+ (function
+ | [y] -> BRel(rel, x, y)
+ | _ -> invalid_arity "boolean relation") b
+ | _ -> invalid_arity "boolean relation")
+ a)
+ | AST_identifier (id, _) ->
+ let id = node^"/"^id in
+ f_or
+ (f_and (BBoolEq(id, true)) (where (BConst true)))
+ (f_and (BBoolEq(id, false)) (where (BConst false)))
+ (* temporal *)
+ | AST_pre(_, id) ->
+ f_or
+ (f_and (BBoolEq(id, true)) (where (BConst true)))
+ (f_and (BBoolEq(id, false)) (where (BConst false)))
+ | AST_arrow(a, b) ->
+ f_or
+ (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+ (sub where a))
+ (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+ (sub where b))
+ (* other *)
+ | AST_if(c, a, b) ->
+ f_or
+ (f_and (f_of_expr td (node, prefix) c) (sub where a))
+ (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
+
+ | _ -> loc_error (snd expr) error "Expected boolean value."
+
+and f_of_expr td (node, prefix) expr =
+ f_of_bexpr td (node, prefix) (fun x -> x) expr
and f_of_scope active td (node, prefix, eqs) =
@@ -148,7 +171,7 @@ and f_of_scope active td (node, prefix, eqs) =
| AST_assume (_, e) ->
let assume_eq =
if active then
- f_of_bexpr td (node, prefix) e
+ f_of_expr td (node, prefix) e
else
BConst true
in
@@ -166,12 +189,11 @@ and f_of_scope active td (node, prefix, eqs) =
| AST_activate_body b ->
f_of_scope true td (node, b.act_id^".", b.body)
| AST_activate_if(c, a, b) ->
- BOr(
- f_and (f_of_bexpr td (node, prefix) c)
- (f_and (do_tree_act a) (do_tree_inact b)),
- f_and (BNot(f_of_bexpr td (node, prefix) c))
- (f_and (do_tree_act b) (do_tree_inact a))
- )
+ f_or
+ (f_and (f_of_expr td (node, prefix) c)
+ (f_and (do_tree_act a) (do_tree_inact b)))
+ (f_and (BNot(f_of_expr td (node, prefix) c))
+ (f_and (do_tree_act b) (do_tree_inact a)))
and do_tree_inact = function
| AST_activate_body b ->
f_of_scope false td (node, b.act_id^".", b.body)
@@ -202,10 +224,6 @@ and f_of_prog p root =
} in
f_of_scope true td td.root_scope
-
-
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-22 02:14:35 +0000