summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abstract/abs_interp_edd.ml19
-rw-r--r--abstract/formula.ml6
-rw-r--r--abstract/transform.ml57
-rw-r--r--frontend/typing.ml11
-rw-r--r--tests/source/two_counters.scade28
5 files changed, 89 insertions, 32 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index b139f9e..56b366e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -588,7 +588,6 @@ end = struct
(* program expressions *)
init_cl : conslist;
cl : conslist;
- cl_g : conslist;
guarantees : (id * bool_expr) list;
}
@@ -773,18 +772,24 @@ end = struct
init_env : cmdline_opt -> rooted_prog -> env
*)
let init_env opt rp =
- let init_f, f = Transform.f_of_prog rp false in
- let _, f_g = Transform.f_of_prog rp true in
+ let f = Transform.f_of_prog_incl_init rp false in
+
+ let f = simplify_k (get_root_true f) f in
+ Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
+
+ (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
+ (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
+
+ let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in
+ let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in
let init_f = simplify_k (get_root_true init_f) init_f in
let f = simplify_k (get_root_true f) f in
- let f_g = simplify_k (get_root_true f_g) f_g in
Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
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;
@@ -795,10 +800,10 @@ end = struct
guarantees;
Format.printf "@.";
- let ve = mk_varenv rp f_g cl_g in
+ let ve = mk_varenv rp f cl in
- { rp; opt; ve; init_cl; cl; cl_g; guarantees; }
+ { rp; opt; ve; init_cl; cl; guarantees; }
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 1882c85..4c2c397 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -76,7 +76,8 @@ let f_or a b =
let f_ternary c a b =
if is_true c then a
else if is_false c then b
- else BTernary(c, a, b)
+ else
+ BTernary(c, a, b)
let f_e_op op a b = match a, b with
| EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
@@ -109,7 +110,8 @@ and eliminate_not_negate = function
| AST_GE -> AST_LT
in
BRel(r', a, b, is_real)
- | BTernary _ -> assert false
+ | BTernary (c, a, b) ->
+ eliminate_not_negate(BOr(BAnd(c, a), BAnd(BNot c, b)))
| BAnd(a, b) ->
BOr(eliminate_not_negate a, eliminate_not_negate b)
| BOr(a, b) ->
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 9bce192..0144637 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -209,6 +209,13 @@ let clock_scope_here (node, prefix, _) =
let gen_clock td (node, prefix, _) active rst_exprs =
let clock_scope = node^"/"^prefix in
+ let act_eq =
+ if clock_scope = "/"
+ then BConst true
+ else if active
+ then BEnumCons(E_EQ, clock_scope^"act", EItem bool_true)
+ else BEnumCons(E_NE, clock_scope^"act", EItem bool_true)
+ in
let clock_eq =
let rst_code =
f_and
@@ -219,28 +226,36 @@ let gen_clock td (node, prefix, _) active rst_exprs =
then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
else BConst true)
in
+ let last_act_eq =
+ (f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ, NIdent(clock_scope^"time"),
+ NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
+ false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
+ else BConst true))
+ in
+ let last_inact_eq =
+ (f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ,
+ NIdent(clock_scope^"time"),
+ NIdent("L"^clock_scope^"time"), false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent(clock_scope^"init"))
+ (EIdent ("L"^clock_scope^"init"))
+ else BConst true))
+ in
let no_rst_code =
- if active then
- f_and
- (if not (td.rp.no_time_scope clock_scope)
- then BRel(AST_EQ, NIdent(clock_scope^"time"),
- NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
- false)
- else BConst true)
- (if td.rp.init_scope clock_scope
- then BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
- else BConst true)
+ if clock_scope = "/"
+ then last_act_eq
else
- f_and
- (if not (td.rp.no_time_scope clock_scope)
- then BRel(AST_EQ,
- NIdent(clock_scope^"time"),
- NIdent("L"^clock_scope^"time"), false)
- else BConst true)
- (if td.rp.init_scope clock_scope
- then f_e_eq (EIdent(clock_scope^"init"))
- (EIdent ("L"^clock_scope^"init"))
- else BConst true)
+ f_ternary
+ (BEnumCons(E_EQ, "L"^clock_scope^"act", EItem bool_true))
+ last_act_eq last_inact_eq
in
if rst_code = BConst true && no_rst_code = BConst true
then BConst true
@@ -250,7 +265,7 @@ let gen_clock td (node, prefix, _) active rst_exprs =
rst_code
no_rst_code
in
- (clock_scope, rst_exprs), clock_eq
+ (clock_scope, rst_exprs), f_and act_eq clock_eq
let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
let expr_eq e =
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 883e8e0..83374ed 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -136,7 +136,12 @@ let clock_vars rp (node, prefix, _) =
then
(false, node^"/"^prefix^"init", bool_type)::v
else v in
- v
+ let v =
+ (* root scope is always active *)
+ if node = "" && prefix = ""
+ then v
+ else (false, node^"/"^prefix^"act", bool_type)::v
+ in v
(*
extract_all_vars : rooted_prog -> scope -> var list
@@ -231,7 +236,9 @@ let root_prog p root no_time_scope init_scope =
const_vars;
all_vars = [] } in
- let root_vars = vars_in_node "" (decls_of_node root_node) in
+ let root_vars =
+ (false, "/must_reset", bool_type)::
+ (vars_in_node "" (decls_of_node root_node)) in
let root_clock_vars = clock_vars rp root_scope in
{ rp with all_vars = root_clock_vars @
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
new file mode 100644
index 0000000..7970aab
--- /dev/null
+++ b/tests/source/two_counters.scade
@@ -0,0 +1,28 @@
+const n1: int = 10;
+const n2: int = 6;
+
+
+node top(a,b,c : bool) returns (ok, r1, r2 : bool)
+var
+ x, y, pre_x, pre_y: int;
+ o1, o2: bool;
+
+ m: bool;
+let
+ x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
+ y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
+ o1= x = n1;
+ o2= y = n2;
+ ok= if o1 then o2 else true;
+ r1 = 0<=x and x<=n1;
+ r2 = 0<=y and y<=n2;
+ pre_x = 0 -> pre(x);
+ pre_y = 0 -> pre(y);
+
+ m = true -> pre o2;
+
+ guarantee g1: ok;
+ guarantee g2: r1;
+ guarantee g3: r2;
+tel
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 16:50:16 +0000