summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 16:21:45 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 16:21:45 +0200
commitb1cdf90995c8f70e4a450b3319a136f0d50515d0 (patch)
tree9074c54967f384fac8d41359a503774158081ac9
parent1445a2be1e1bd81efa552230a0f11672aa20a92c (diff)
downloadscade-analyzer-b1cdf90995c8f70e4a450b3319a136f0d50515d0.tar.gz
scade-analyzer-b1cdf90995c8f70e4a450b3319a136f0d50515d0.zip
New example ; minor fixes.
-rw-r--r--abstract/abs_interp_edd.ml11
-rw-r--r--abstract/transform.ml6
-rw-r--r--frontend/lexer.mll6
-rw-r--r--main.ml2
-rw-r--r--tests/source/NestedControl.scade8
-rw-r--r--tests/source/counters.scade38
-rw-r--r--tests/source/test5.scade4
7 files changed, 63 insertions, 12 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
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index ef40aa7..837ee75 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -88,6 +88,7 @@ rule token = parse
| const_real as c { REALVAL c }
(* spaces, comments *)
| "(*" { comment lexbuf; token lexbuf }
+ | "/*" { cppcomment lexbuf; token lexbuf }
| "--" [^ '\n' '\r']* { token lexbuf }
| newline { new_line lexbuf; token lexbuf }
| space { token lexbuf }
@@ -98,3 +99,8 @@ and comment = parse
| "*)" { () }
| [^ '\n' '\r'] { comment lexbuf }
| newline { new_line lexbuf; comment lexbuf }
+
+and cppcomment = parse
+ | "*/" { () }
+ | [^ '\n' '\r'] { cppcomment lexbuf }
+ | newline { new_line lexbuf; cppcomment lexbuf }
diff --git a/main.ml b/main.ml
index a02820c..6cb2c50 100644
--- a/main.ml
+++ b/main.ml
@@ -29,7 +29,7 @@ let ai_rel = ref false
let ai_itv_edd = ref false
let ai_rel_edd = ref false
let ai_root = ref "test"
-let ai_widen_delay = ref 3
+let ai_widen_delay = ref 5
let ai_no_time_scopes = ref ""
let ai_init_scopes = ref ""
let ai_disj_v = ref ""
diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade
index 2551eb6..af4fdab 100644
--- a/tests/source/NestedControl.scade
+++ b/tests/source/NestedControl.scade
@@ -1,13 +1,13 @@
node root(In : int; C : bool) returns (Out, Out1 : int)
var last_Out, last_Out1: int;
- isp, isn: bool;
+ disj, disj2: bool;
let
last_Out = 0 -> pre Out;
last_Out1 = 0 -> pre Out1;
- isp = In > 0;
- isn = In < 0;
- assume C_in_not_null: (not C) or isp or isn;
+ disj = In > 0;
+ disj2 = In < 0;
+ assume C_in_not_null: (not C) or disj or disj2;
automaton SM1
initial state State1
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
new file mode 100644
index 0000000..334bca1
--- /dev/null
+++ b/tests/source/counters.scade
@@ -0,0 +1,38 @@
+/*
+ x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0 | 1 | 2 | ... | 10 | ...
+ y = 0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0 | ...
+
+ b1 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+ b2 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+
+ eq* = t | t | t | t | t | t | ... | t | t | t | ... | t | ...
+*/
+
+
+-- type t2 = subrange [0,10] of int;
+
+const bound: int = 1000;
+
+node counters(z: bool) returns (eq_nind : bool ; probe x, probe y : int)
+var
+ b1, b2 : bool;
+ a, b : bool;
+let
+
+ a = false -> (if pre a then pre x < bound else pre x <= 0);
+ --a = false -> pre(if a then x < bound else x <= 0);
+ x = bound -> (if a then pre x + 1 else pre x - 1);
+
+ b = true -> (if pre b then pre y < bound else pre y <= 0);
+ --b = true -> pre(if b then y < bound else y <= 0);
+ y = 0 -> (if b then pre y + 1 else pre y - 1);
+
+ b1 = x=bound;
+ b2 = y=0;
+
+
+ guarantee xy : x+y = bound;
+ guarantee bb : b1 = b2;
+ guarantee rp : -bound <= (x-y) and (x-y) <= bound;
+
+tel
diff --git a/tests/source/test5.scade b/tests/source/test5.scade
index 1de390d..566acf0 100644
--- a/tests/source/test5.scade
+++ b/tests/source/test5.scade
@@ -1,8 +1,8 @@
-node test(i: int) returns(probe a, b, c: int; exit: bool)
+node test(i: int) returns(probe a, probe b, probe c: int; exit: bool)
let
b = 0 -> pre a;
a = if b > 4 then 0 else b + 1;
- c = 0;
+ c = i;
exit = i >= 10;
tel