summaryrefslogtreecommitdiff
path: root/abstract/transform.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/transform.ml')
-rw-r--r--abstract/transform.ml229
1 files changed, 135 insertions, 94 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b9c173d..4a13e18 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -26,8 +26,8 @@ type ne_expr =
(* f_of_neexpr :
transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr
*)
-let rec f_of_neexpr td (node, prefix) where expr =
- let sub = f_of_neexpr td (node, prefix) in
+let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
+ let sub = f_of_neexpr td (node, prefix, clock_scope) in
let le = loc_error (snd expr) in
match fst expr with
(* ident *)
@@ -71,24 +71,27 @@ let rec f_of_neexpr td (node, prefix) where expr =
| TEnum _ -> EE(EIdent x))
typ)
| AST_arrow(a, b) ->
- if td.rp.init_scope (node^"/")
+ if td.rp.init_scope clock_scope
then
f_or
- (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true))
+ (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
(sub where a))
- (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false))
+ (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
(sub where b))
- else
+ else if not (td.rp.no_time_scope clock_scope)
+ then
f_or
- (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+ (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
(sub where a))
- (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+ (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
(sub where b))
+ else
+ f_or (sub where a) (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))
+ (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a))
+ (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b))
| AST_instance ((f, _), args, nid) ->
let (n, _) = find_node_decl td.rp.p f in
where
@@ -107,8 +110,9 @@ let rec f_of_neexpr td (node, prefix) where expr =
(* boolean values treated as enumerated types *)
| _ when type_expr td.rp node expr = [bool_type] ->
f_or
- (f_and (f_of_expr td (node, prefix) expr) (where [EE (EItem bool_true)]))
- (f_and (f_of_expr td (node, prefix) (AST_not(expr), snd expr))
+ (f_and (f_of_expr td (node, prefix, clock_scope) expr)
+ (where [EE (EItem bool_true)]))
+ (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr))
(where [EE (EItem bool_false)]))
| _ -> le type_error "Expected numerical/enumerated value"
@@ -120,8 +124,8 @@ let rec f_of_neexpr td (node, prefix) where expr =
f_of_bexpr :
transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr
*)
-and f_of_bexpr td (node, prefix) where expr =
- let sub = f_of_bexpr td (node, prefix) in
+and f_of_bexpr td (node, prefix, clock_scope) where expr =
+ let sub = f_of_bexpr td (node, prefix, clock_scope) in
match fst expr with
| AST_bool_const b -> where (BConst b)
| AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b)
@@ -129,7 +133,7 @@ and f_of_bexpr td (node, prefix) where expr =
| AST_not(a) -> BNot(sub where a)
| AST_binary_rel(rel, a, b) ->
where
- (f_of_neexpr td (node, prefix)
+ (f_of_neexpr td (node, prefix, clock_scope)
(function
| [NE x; NE y] -> BRel(rel, x, y)
| [EE x; EE y] ->
@@ -142,11 +146,22 @@ and f_of_bexpr td (node, prefix) where expr =
(AST_tuple [a; b], snd expr))
(* Temporal *)
| AST_arrow(a, b) ->
+ if td.rp.init_scope clock_scope
+ then
f_or
- (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+ (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
(sub where a))
- (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+ (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
(sub where b))
+ else if not (td.rp.no_time_scope clock_scope)
+ then
+ f_or
+ (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
+ (sub where a))
+ (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
+ (sub where b))
+ else
+ f_or (sub where a) (sub where b)
(* Enumerations... *)
| _ when type_expr td.rp node expr = [bool_type] ->
let ff = function
@@ -156,23 +171,53 @@ and f_of_bexpr td (node, prefix) where expr =
(f_and (f_e_eq x (EItem bool_false)) (where (BConst false)))
| _ -> assert false
in
- f_of_neexpr td (node, prefix) ff expr
+ f_of_neexpr td (node, prefix, clock_scope) ff expr
| _ -> type_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_expr td (node, prefix, clock_scope) expr =
+ f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr
(*
Translate program into one big formula
*)
-let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
+
+let clock_scope_here (node, prefix, _) =
+ node^"/"^prefix
+
+let gen_clock td (node, prefix, _) active =
+ let clock_scope = node^"/"^prefix in
+ let clock_eq =
+ if active then
+ f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ, NIdent("N"^clock_scope^"time"),
+ NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time")))
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false)
+ else BConst true)
+ else
+ f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ,
+ NIdent("N"^clock_scope^"time"),
+ NIdent(clock_scope^"time"))
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent("N"^clock_scope^"init"))
+ (EIdent (clock_scope^"init"))
+ else BConst true)
+ in
+ clock_scope, clock_eq
+
+let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
- let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
+ let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
if active then
let arg_eq ((_,argname,_), expr) =
- f_of_neexpr td (node, prefix) (function
+ f_of_neexpr td (node, prefix, clock_scope) (function
| [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
| [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
| _ -> invalid_arity "in argument")
@@ -186,7 +231,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
let pre_expr (id, expr) =
let id = node^"/"^id in
if active then
- f_of_neexpr td (node, prefix) (fun elist ->
+ f_of_neexpr td (node, prefix, clock_scope) (fun elist ->
list_fold_op f_and
(List.mapi
(fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
@@ -222,7 +267,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
in
f_and_list rels
in
- f_of_neexpr td (node, prefix) apply_f e
+ f_of_neexpr td (node, prefix, clock_scope) apply_f e
else
BConst true
in
@@ -230,7 +275,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
| AST_assume (_, e) ->
let assume_eq =
if active then
- f_of_expr td (node, prefix) e
+ f_of_expr td (node, prefix, clock_scope) e
else
BConst true
in
@@ -239,13 +284,13 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
let gn = node^"/g_"^id in
let guarantee_eq =
if active && assume_guarantees then
- f_and (f_of_expr td (node, prefix) e)
+ f_and (f_of_expr td (node, prefix, clock_scope) e)
(BEnumCons(E_EQ, gn, EItem bool_true))
else
f_or
- (f_and (f_of_expr td (node, prefix) e)
+ (f_and (f_of_expr td (node, prefix, clock_scope) e)
(BEnumCons(E_EQ, gn, EItem bool_true)))
- (f_and (BNot (f_of_expr td (node, prefix) e))
+ (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e))
(BEnumCons(E_EQ, gn, EItem bool_false)))
in
f_and (expr_eq e) guarantee_eq
@@ -258,16 +303,20 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
in
let rec do_tree_act = function
| AST_activate_body b ->
- f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees
+ let b_scope = node, b.act_id^".", b.body in
+ let clock_scope, clock_eq = gen_clock td b_scope true in
+ f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees)
| AST_activate_if(c, a, b) ->
f_or
- (f_and (f_of_expr td (node, prefix) c)
+ (f_and (f_of_expr td (node, prefix, clock_scope) c)
(f_and (do_tree_act a) (do_tree_inact b)))
- (f_and (BNot(f_of_expr td (node, prefix) c))
+ (f_and (BNot(f_of_expr td (node, prefix, clock_scope) 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) assume_guarantees
+ let b_scope = node, b.act_id^".", b.body in
+ let clock_scope, clock_eq = gen_clock td b_scope false in
+ f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees)
| AST_activate_if(_, a, b) ->
f_and (do_tree_inact a) (do_tree_inact b)
in
@@ -276,24 +325,27 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
let stv = node^"/"^aid^".state" in
let nstv = "N"^node^"/"^aid^".state" in
let st_eq_inact (st, _) =
- f_and
- (f_of_scope false td
- (node, aid^"."^st.st_name^".", st.body) assume_guarantees)
- (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until))
+ let st_scope = node, aid^"."^st.st_name^".", st.body in
+ let clock_scope, clock_eq = gen_clock td st_scope false in
+ f_and clock_eq
+ (f_and
+ (f_of_scope false td st_scope clock_scope assume_guarantees)
+ (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until)))
in
if active then
let st_eq_act (st, l) =
let act_eq =
- let st_eq = f_of_scope true td
- (node, aid^"."^st.st_name^".", st.body) assume_guarantees in
+ let st_scope = node, aid^"."^st.st_name^".", st.body in
+ let clock_scope, clock_eq = gen_clock td st_scope true in
+ let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in
let rec aux = function
| [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
| (c, (target, l), rst)::q ->
if rst then loc_error l error "Resetting transitions not supported.";
f_or
- (f_and (f_of_expr td (node, prefix) c)
+ (f_and (f_of_expr td (node, prefix, clock_scope) c)
(BEnumCons(E_EQ, nstv, EItem target)))
- (f_and (BNot (f_of_expr td (node, prefix) c)) (aux q))
+ (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q))
in f_and st_eq (aux st.until)
in
f_or
@@ -305,31 +357,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
else
f_and_list (List.map st_eq_inact states)
in
- let time_incr_eq =
- if active then
- f_and
- (if not (td.rp.no_time_scope (node^"/"))
- then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
- NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
- else BConst true)
- (if td.rp.init_scope (node^"/")
- then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
- else BConst true)
- else
- f_and
- (if not (td.rp.no_time_scope (node^"/"))
- then BRel(AST_EQ,
- NIdent("N"^node^"/"^prefix^"time"),
- NIdent(node^"/"^prefix^"time"))
- else BConst true)
- (if td.rp.init_scope (node^"/")
- then f_e_eq (EIdent("N"^node^"/"^prefix^"init"))
- (EIdent (node^"/"^prefix^"init"))
- else BConst true)
- in
- List.fold_left f_and
- time_incr_eq
- (List.map do_eq eqs)
+ f_and_list (List.map do_eq eqs)
and f_of_prog rp assume_guarantees =
let td = {
@@ -337,15 +365,34 @@ and f_of_prog rp assume_guarantees =
consts = I.consts rp;
} in
- f_of_scope true td td.rp.root_scope assume_guarantees
+ let clock_scope, clock_eq = gen_clock td rp.root_scope true in
+
+ f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees)
(*
Translate init state into a formula
*)
-let rec init_f_of_scope rp (node, prefix, eqs) =
+let gen_clock_init rp (node, prefix, _) =
+ let clock_scope = node^"/"^prefix in
+ let time_eq =
+ f_and
+ (if not (rp.no_time_scope clock_scope)
+ then
+ BRel(AST_EQ,
+ NIdent(clock_scope^"time"),
+ NIntConst 0)
+ else BConst true)
+ (if rp.init_scope clock_scope
+ then
+ f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
+ else BConst true)
+ in
+ clock_scope, time_eq
+
+let rec init_f_of_scope rp (node, prefix, eqs) clock_scope =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
- init_f_of_scope rp (node^"/"^id, "", eqs)
+ init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope
in
List.fold_left (fun x i -> f_and (instance_eq i) x)
(BConst true) (extract_instances rp.p e)
@@ -356,7 +403,9 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
| AST_activate (b, _) ->
let rec cond_eq = function
| AST_activate_body b ->
- init_f_of_scope rp (node, b.act_id^".", b.body)
+ let bscope = (node, b.act_id^".", b.body) in
+ let clock_scope, clock_eq = gen_clock_init rp bscope in
+ f_and clock_eq (init_f_of_scope rp bscope clock_scope)
| AST_activate_if(c, a, b) ->
f_and (expr_eq c)
(f_and (cond_eq a) (cond_eq b))
@@ -367,37 +416,27 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
let state_eq (st, _) =
let sc_f =
- init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body)
+ let st_scope = (node, aid^"."^st.st_name^".", st.body) in
+ let clock_scope, clock_eq = gen_clock_init rp st_scope in
+ f_and clock_eq (init_f_of_scope rp st_scope clock_scope)
in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until
in
List.fold_left f_and init_eq
(List.map state_eq states)
in
- let time_eq =
- f_and
- (if not (rp.no_time_scope (node^"/"))
- then
- BRel(AST_EQ,
- NIdent(node^"/"^prefix^"time"),
- NIntConst 0)
- else BConst true)
- (if rp.init_scope (node^"/")
- then
- f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true)
- else BConst true)
- in
- List.fold_left f_and time_eq (List.map do_eq eqs)
+ f_and_list (List.map do_eq eqs)
and init_f_of_prog rp =
- init_f_of_scope rp rp.root_scope
+ let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in
+ f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope)
(*
Get expressions for guarantee violation
*)
-let rec g_of_scope td (node, prefix, eqs) cond =
+let rec g_of_scope td (node, prefix, eqs) clock_scope cond =
let expr_g e =
let instance_g (_, id, eqs, args) =
- g_of_scope td (node^"/"^id, "", eqs) cond
+ g_of_scope td (node^"/"^id, "", eqs) clock_scope cond
in
List.fold_left (fun x i -> (instance_g i) @ x)
[] (extract_instances td.rp.p e)
@@ -406,21 +445,23 @@ let rec g_of_scope td (node, prefix, eqs) cond =
| AST_assign(_, e) | AST_assume(_, e) ->
expr_g e
| AST_guarantee((id, _), e) ->
- (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e)))
+ (id, f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e)))
:: (expr_g e)
| AST_activate (b, _) ->
let rec cond_g cond = function
| AST_activate_body b ->
- g_of_scope td (node, b.act_id^".", b.body) cond
+ let bscope = node, b.act_id^".", b.body in
+ g_of_scope td bscope (clock_scope_here bscope) cond
| AST_activate_if(c, a, b) ->
- (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @
- (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @
+ (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) c)) a) @
+ (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(c), snd c))) b) @
(expr_g c)
in
cond_g cond b
| AST_automaton (aid, states, _) ->
let st_g (st, _) =
- g_of_scope td (node, aid^"."^st.st_name^".", st.body)
+ let stscope = (node, aid^"."^st.st_name^".", st.body) in
+ g_of_scope td stscope (clock_scope_here stscope)
(f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name)))
in
List.flatten (List.map st_g states)
@@ -433,4 +474,4 @@ and guarantees_of_prog rp =
consts = I.consts rp;
} in
- g_of_scope td rp.root_scope (BConst true)
+ g_of_scope td rp.root_scope "" (BConst true)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-24 13:20:34 +0000