summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-20 17:26:10 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-20 17:26:10 +0200
commit6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4 (patch)
tree82f15798a28e557538b061bb90e37644b51261e5
parentdd7b7d30adddfa0258aa5b3819a0a58d6b5d8705 (diff)
downloadscade-analyzer-6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4.tar.gz
scade-analyzer-6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4.zip
Not much. Still does not work very well.
-rw-r--r--abstract/abs_domain.ml49
-rw-r--r--abstract/abs_interp.ml4
-rw-r--r--abstract/formula.ml10
-rw-r--r--abstract/formula_printer.ml2
-rw-r--r--abstract/nonrelational.ml6
-rw-r--r--abstract/transform.ml44
-rw-r--r--frontend/ast_printer.ml2
-rw-r--r--frontend/typing.ml19
-rw-r--r--main.ml25
-rw-r--r--tests/source/updown.scade2
-rw-r--r--tests/source/uturn.scade76
11 files changed, 160 insertions, 79 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index 64eefc7..d6ff489 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -131,7 +131,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
if i > 0 then Format.fprintf fmt ",@ ";
Format.fprintf fmt "%a" Formula_printer.print_id id)
ids;
- Format.fprintf fmt " = %s@]" v)
+ Format.fprintf fmt " ≡ %s@]" v)
sbl;
Format.fprintf fmt " }@]"
@@ -171,16 +171,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let strict value =
VMap.filter (fun _ v -> not (ND.is_bot v)) value
- let add_case x (enum, num) =
+ let add_case_w widen x (enum, num) =
let value = x.value in
let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in
let v =
- if VMap.exists (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) value || ND.is_bot num then
+ if VMap.exists
+ (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0)
+ value
+ || ND.is_bot num
+ then
value
else
- try VMap.add enum (ND.join num (VMap.find enum value)) value
+ try VMap.add enum
+ ((if widen then ND.widen else ND.join) (VMap.find enum value) num)
+ value
with Not_found -> VMap.add enum num value
in { x with value = v }
+ let add_case = add_case_w false
let addvar x id ty = match ty with
| TInt | TReal ->
@@ -252,18 +259,18 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let join x y =
VMap.fold
(fun enum num value -> add_case value (enum, num))
- x.value
- y
+ y.value
+ x
let meet x y = not_implemented "meet for enum+num domain"
let widen x y =
- { x with
- value = VMap.merge
- (fun _ a b -> match a, b with
- | None, Some a -> Some a
- | Some a, None -> Some a
- | Some a, Some b -> Some (ND.widen a b)
- | _ -> assert false)
- x.value y.value }
+ let value = VMap.merge
+ (fun _ a b -> match a, b with
+ | Some x, None -> Some x
+ | None, Some y -> Some y
+ | Some x, Some y -> Some (ND.widen x y)
+ | _ -> None)
+ x.value y.value
+ in { x with value = value }
(* Some cases of subset/equality not detected *)
let subset a b =
@@ -281,13 +288,9 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
VMap.fold
(fun enum num value ->
match a, b with
- | EItem x, EItem y ->
- if (x = y && op = E_EQ) || (x <> y && op = E_NE)
- then add_case value (enum, num)
- else value
- | EItem u, EIdent i | EIdent i, EItem u ->
- begin try let y = VarMap.find i enum in
- if (u = y && op = E_EQ) || (u <> y && op = E_NE)
+ | i, EItem u ->
+ begin try let v = VarMap.find i enum in
+ if (if op = E_EQ then u = v else u <> v)
then add_case value (enum, num)
else value
with Not_found ->
@@ -300,11 +303,11 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
value
(List.filter ((<>) u) (List.assoc i x.evars))
end
- | EIdent i, EIdent j ->
+ | i, EIdent j ->
begin
try let x = VarMap.find i enum in
try let y = VarMap.find j enum in
- if (x = y && op = E_EQ) || (x <> y && op = E_NE)
+ if (if op = E_EQ then x = y else x <> y)
then add_case value (enum, num)
else value
with Not_found (* J not found *) ->
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 383a69c..a610843 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -111,14 +111,14 @@ end = struct
let rec iter n i =
let i' =
if n < st.widen_delay
- then E.join i (fsharp st.cl_g i)
+ then E.join i (fsharp st.cl i)
else E.widen i (fsharp st.cl_g i)
in
if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 acc0 in
- let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *)
+ let y = fix E.eq (fsharp st.cl) x in (* decreasing iteration *)
let z = E.apply_cl y st.cl in (* no more guarantee *)
y, z
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 62acb28..cb7a4c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -34,7 +34,7 @@ type enum_expr =
type enum_op =
| E_EQ | E_NE
-type enum_cons = enum_op * enum_expr * enum_expr
+type enum_cons = enum_op * id * enum_expr
type bool_expr =
(* constants *)
@@ -62,10 +62,10 @@ let f_or a b = match a, b with
| a, BConst false -> a
| a, b -> BOr(a, b)
-let f_e_eq a b = match a, b with
- | EItem u, EItem v -> BConst (u = v)
- | _ -> BEnumCons(E_EQ, 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)
+ | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
+let f_e_eq = f_e_op E_EQ
(* Write all formula without using the NOT operator *)
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 0c7d65e..383500c 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -68,7 +68,7 @@ let str_of_enum_op = function
let print_econs fmt (op, a, b) =
Format.fprintf fmt "%a %s %a"
- print_enum_expr a (str_of_enum_op op) print_enum_expr b
+ print_id a (str_of_enum_op op) print_enum_expr b
(* Print boolean form of formula *)
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index bbdc875..6497760 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -104,11 +104,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
let eq a b = match a, b with
| Bot, Bot -> true
| Env m, Env n ->
- VarMap.for_all2o
- (fun _ _ -> false)
- (fun _ _ -> false)
- (fun _ a b -> a = b)
- m n
+ VarMap.equal (=) m n
| _ -> false
(* Apply some formula to the environment *)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 6fa1277..b6781a8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -136,7 +136,7 @@ and f_of_bexpr td (node, prefix) where expr =
| AST_EQ -> E_EQ
| AST_NE -> E_NE
| _ -> type_error "Invalid operator on enumerated values."
- in BEnumCons(eop, x, y)
+ in f_e_op eop x y
| _ -> invalid_arity "Binary operator")
(AST_tuple [a; b], snd expr))
(* Temporal *)
@@ -233,12 +233,18 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
BConst true
in
f_and (expr_eq e) assume_eq
- | AST_guarantee (_, e) ->
+ | AST_guarantee ((id, _), e) ->
+ let gn = node^"/g_"^id in
let guarantee_eq =
if active && assume_guarantees then
- f_of_expr td (node, prefix) e
+ f_and (f_of_expr td (node, prefix) e)
+ (BEnumCons(E_EQ, gn, EItem bool_true))
else
- BConst true
+ f_or
+ (f_and (f_of_expr td (node, prefix) e)
+ (BEnumCons(E_EQ, gn, EItem bool_true)))
+ (f_and (BNot (f_of_expr td (node, prefix) e))
+ (BEnumCons(E_EQ, gn, EItem bool_false)))
in
f_and (expr_eq e) guarantee_eq
| AST_activate (b, _) ->
@@ -265,8 +271,8 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
in
f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
| AST_automaton (aid, states, _) ->
- let stv = EIdent (node^"/"^aid^".state") in
- let nstv = EIdent ("N"^node^"/"^aid^".state") in
+ 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
@@ -304,13 +310,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
else BConst true)
- (f_and
- (if List.mem (node^"/") td.rp.act_scope
- then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true)
- else BConst true)
- (if List.mem (node^"/") td.rp.init_scope
- then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
- else BConst true))
+ (if List.mem (node^"/") td.rp.init_scope
+ then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
+ else BConst true)
else
f_and
(if not (List.mem (node^"/") td.rp.no_time_scope)
@@ -318,14 +320,10 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
NIdent("N"^node^"/"^prefix^"time"),
NIdent(node^"/"^prefix^"time"))
else BConst true)
- (f_and
- (if List.mem (node^"/") td.rp.act_scope
- then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false)
- else BConst true)
- (if List.mem (node^"/") td.rp.init_scope
- then f_e_eq (EIdent("N"^node^"/"^prefix^"init"))
- (EIdent (node^"/"^prefix^"init"))
- else BConst true))
+ (if List.mem (node^"/") td.rp.init_scope
+ 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
@@ -364,7 +362,7 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
cond_eq b
| AST_automaton (aid, states, _) ->
let (st, _) = List.find (fun (st, _) -> st.initial) states in
- let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in
+ 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)
@@ -421,7 +419,7 @@ let rec g_of_scope td (node, prefix, eqs) cond =
| AST_automaton (aid, states, _) ->
let st_g (st, _) =
g_of_scope td (node, aid^"."^st.st_name^".", st.body)
- (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name)))
+ (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name)))
in
List.flatten (List.map st_g states)
in
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index ac30fe9..b6c06fb 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -264,7 +264,7 @@ let print_prog fmt p =
let print_type fmt = function
| TInt -> Format.fprintf fmt "int"
| TReal -> Format.fprintf fmt "real"
- | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e
+ | TEnum e -> Format.fprintf fmt "enum @[<h>{ %a }@]" (print_list print_id ", ") e
let print_typed_var fmt (p, id, t) =
Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 564d91e..0417d27 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -33,7 +33,6 @@ type rooted_prog = {
p : prog;
no_time_scope : id list; (* scopes in which not to introduce time variable *)
- act_scope : id list; (* scopes in which to introduce act variable *)
init_scope : id list; (* scopes in which to introduce init variable *)
root_node : node_decl;
@@ -146,7 +145,10 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(extract_pre e))
in
let vars_of_eq e = match fst e with
- | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
+ | AST_assign(_, e) | AST_assume(_, e) -> vars_of_expr e
+ | AST_guarantee((id, _), e) ->
+ let gn = node^"/g_"^id in
+ (false, gn, bool_type)::vars_of_expr e
| AST_activate (b, _) ->
let rec do_branch = function
| AST_activate_body b ->
@@ -183,10 +185,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(false, "N"^node^"/"^prefix^"time", TInt)::v
else v in
let v =
- if List.mem (node^"/") rp.act_scope
- then (false, node^"/"^prefix^"act", bool_type)::v
- else v in
- let v =
if List.mem (node^"/") rp.init_scope
then
(false, node^"/"^prefix^"init", bool_type)::
@@ -196,9 +194,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(*
- root_prog : prog -> id -> rooted_prog
+ root_prog : prog -> id -> string list -> string list -> rooted_prog
*)
-let root_prog p root =
+let root_prog p root no_time_scope init_scope =
let (root_node, _) = find_node_decl p root in
let root_scope = ("", "", root_node.body) in
@@ -212,9 +210,8 @@ let root_prog p root =
let rp = {
p; root_scope; root_node;
- no_time_scope = ["/"];
- act_scope = [];
- init_scope = ["/"];
+ no_time_scope;
+ init_scope;
const_vars;
all_vars = [] } in
diff --git a/main.ml b/main.ml
index 72c43b0..3cef6bd 100644
--- a/main.ml
+++ b/main.ml
@@ -19,6 +19,8 @@ let ai_itv = ref false
let ai_rel = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 3
+let ai_no_time_scopes = ref ""
+let ai_init_scopes = ref ""
let ifile = ref ""
let usage = "usage: analyzer [options] file.scade"
@@ -26,16 +28,18 @@ let usage = "usage: analyzer [options] file.scade"
let options = [
"--dump", Arg.Set dump, "Dump program source.";
"--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
- "--vtest", Arg.Set vtest, "Verbose testing.";
- "--test", Arg.Set test, "Simple testing.";
+ "--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
+ "--test", Arg.Set test, "Simple testing (direct interpret).";
"--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
"--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
- "--ai-root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
- "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
+ "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
+ "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
+ "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis.";
+ "--init", Arg.Set_string ai_init_scopes, "Scopes for which to introduce a 'init' variable in analysis.";
]
let do_test_interpret prog verbose =
- let s0 = Interpret.init_state (Typing.root_prog prog "test") in
+ let s0 = Interpret.init_state (Typing.root_prog prog "test" [] []) in
if verbose then begin
Format.printf "Init state:@.";
Interpret.print_state Format.std_formatter s0;
@@ -79,8 +83,15 @@ let () =
let prog = Rename.rename_prog prog in
if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
- if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
- if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
+ if !ai_itv || !ai_rel then begin
+ let comma_split = Str.split (Str.regexp ",") in
+ let rp = Typing.root_prog prog !ai_root
+ (comma_split !ai_no_time_scopes)
+ (comma_split !ai_init_scopes) in
+
+ if !ai_itv then AI_Itv.do_prog !ai_widen_delay rp;
+ if !ai_rel then AI_Rel.do_prog !ai_widen_delay rp;
+ end;
if !vtest then do_test_interpret prog true
else if !test then do_test_interpret prog false;
diff --git a/tests/source/updown.scade b/tests/source/updown.scade
index 089293a..c736dd8 100644
--- a/tests/source/updown.scade
+++ b/tests/source/updown.scade
@@ -4,7 +4,6 @@ node updown() returns(probe x: int)
var last_x: int;
let
last_x = 0 -> pre x;
- guarantee x_bounded: x >= -bound and x <= bound;
automaton
initial state UP
let x = last_x + 1; tel
@@ -15,6 +14,7 @@ let
until if x <= -bound resume UP;
returns x;
+ guarantee x_bounded: x >= -bound and x <= bound;
tel
node test(i: int) returns(a, b, c: int; exit: bool)
diff --git a/tests/source/uturn.scade b/tests/source/uturn.scade
new file mode 100644
index 0000000..84c9b51
--- /dev/null
+++ b/tests/source/uturn.scade
@@ -0,0 +1,76 @@
+-- U turn system for a subway
+-- See paper HLR-lustre.tse.ps
+
+
+node edge(X: bool) returns (EDGE: bool)
+let
+ EDGE = X -> (X and not pre X);
+tel
+
+node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)
+ returns (grant_access, grant_exit, do_AB, do_BC: bool)
+var empty_section, only_on_B: bool;
+let
+ grant_access = empty_section and ack_AB;
+ grant_exit = only_on_B and ack_BC;
+ do_AB = (not ack_AB) and empty_section;
+ do_BC = (not ack_BC) and only_on_B;
+ empty_section = not (on_A or on_B or on_C);
+ only_on_B = on_B and not (on_C or on_A);
+tel
+
+node always_from_to(B, A, C: bool) returns (X: bool)
+let
+ X = implies(after(A), always_since(B, A) or once_since(C, A));
+tel
+
+node implies(A, B: bool) returns (AimpliesB: bool)
+let
+ AimpliesB = (not A) or B;
+tel
+
+node after(A: bool) returns (afterA: bool)
+let
+ afterA = false -> pre(A or afterA);
+tel
+
+node always_since(B, A: bool) returns (alwaysBsinceA: bool)
+let
+ alwaysBsinceA = if A then B
+ else if after(A) then B and pre alwaysBsinceA
+ else true;
+tel
+
+node once_since(C, A: bool) returns (onceCsinceA: bool)
+let
+ onceCsinceA = if A then C
+ else if after(A) then C or pre onceCsinceA
+ else true;
+tel
+
+node UMS_verif(on_A, on_B, on_C, ack_AB, ack_BC: bool)
+ returns()
+var
+ grant_access, grant_exit: bool;
+ do_AB, do_BC: bool;
+ empty_section, only_on_B: bool;
+let
+ empty_section = not (on_A or on_B or on_C);
+ only_on_B = on_B and not(on_A or on_C);
+
+ assume h1: not(ack_AB and ack_BC);
+ assume h2: always_from_to(ack_AB, ack_AB, do_BC)
+ and always_from_to(ack_BC, ack_BC, do_AB);
+ assume h3: empty_section -> true;
+ assume h4: true -> implies(edge(not empty_section), pre grant_access);
+ assume h5: true -> implies(edge(on_C), pre grant_exit);
+ assume h6: implies(edge(not on_A), on_B);
+ assume h7: implies(edge(not on_B), on_A or on_C);
+
+ grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC);
+
+ guarantee no_collision: implies(grant_access, empty_section);
+ guarantee exclusive_req: not(do_AB and do_BC);
+ guarantee no_derail_AB: always_from_to(ack_AB, grant_access, only_on_B);
+ guarantee no_derail_BC: always_from_to(ack_BC, grant_exit, empty_section);
+tel