summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 11:10:13 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 11:10:13 +0200
commit2cbaba6f00d40d5c6c9659678d0156f14b7e3780 (patch)
tree2e7638d943387581dda433a9b7ae58f91bcdaa50
parent8c8765721b5cb2907182a63c562677447df8caea (diff)
downloadscade-analyzer-2cbaba6f00d40d5c6c9659678d0156f14b7e3780.tar.gz
scade-analyzer-2cbaba6f00d40d5c6c9659678d0156f14b7e3780.zip
Use LAST instead of NEXT (only EDD implementation works at the moment)
-rw-r--r--abstract/abs_interp.ml7
-rw-r--r--abstract/abs_interp_edd.ml73
-rw-r--r--abstract/formula.ml3
-rw-r--r--abstract/transform.ml235
-rw-r--r--cmdline.ml8
-rw-r--r--frontend/typing.ml27
-rw-r--r--libs/util.ml2
-rw-r--r--main.ml7
8 files changed, 189 insertions, 173 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3db657..26b788b 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -2,17 +2,12 @@ open Ast
open Ast_util
open Formula
open Typing
+open Cmdline
open Util
open Num_domain
open Enum_domain
-type cmdline_opt = {
- widen_delay : int;
- disjunct : (id -> bool);
- verbose_ci : bool;
- vverbose_ci : bool;
-}
module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..c1fb905 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -2,10 +2,10 @@ open Ast
open Ast_util
open Formula
open Typing
+open Cmdline
open Util
open Num_domain
-open Abs_interp
@@ -592,9 +592,12 @@ end = struct
rp : rooted_prog;
opt : cmdline_opt;
+ last_vars : (bool * id * typ) list;
+ all_vars : (bool * id * typ) list;
ve : varenv;
(* program expressions *)
+ init_f : bool_expr;
cl : conslist;
cl_g : conslist;
guarantees : (id * bool_expr) list;
@@ -602,7 +605,6 @@ end = struct
(* abstract interpretation *)
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
- mutable data : edd_v;
}
@@ -924,20 +926,33 @@ 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
+ 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
+ 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
+ let last_vars = List.map
+ (fun id ->
+ let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+ in false, id, ty)
+ last_vars in
+ let all_vars = last_vars @ rp.all_vars in
+
Format.printf "Vars: @[<hov>%a@]@.@."
(print_list Ast_printer.print_typed_var ", ")
- rp.all_vars;
+ all_vars;
let num_vars, enum_vars = List.fold_left
(fun (nv, ev) (_, id, t) -> match t with
| TEnum ch -> nv, (id, ch)::ev
| TInt -> (id, false)::nv, ev
| TReal -> (id, true)::nv, ev)
- ([], []) rp.all_vars in
-
- let init_f = Transform.init_f_of_prog rp in
- Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
- let init_cl = conslist_of_f init_f in
+ ([], []) all_vars in
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
@@ -946,19 +961,10 @@ end = struct
guarantees;
Format.printf "@.";
- let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
- let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
- 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
- Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
-
(* calculate order for enumerated variables *)
let evars = List.map fst enum_vars in
- let lv = extract_linked_evars_root init_cl
- @ extract_linked_evars_root cl_g in
+ let lv = extract_linked_evars_root cl_g in
let lv = uniq_sorted
(List.sort Pervasives.compare (List.map ord_couple lv)) in
@@ -995,25 +1001,17 @@ end = struct
(* calculate cycle variables and forget variables *)
let cycle = List.fold_left
(fun q (_, id, ty) ->
- if id.[0] = 'N' then
- (String.sub id 1 (String.length id - 1), id, ty)::q
+ if id.[0] = 'L' then
+ (id, String.sub id 1 (String.length id - 1), ty)::q
else q)
- [] rp.all_vars
- in
- let forget = List.map (fun (_, id, ty) -> (id, ty))
- (List.filter
- (fun (_, id, _) ->
- not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
- rp.all_vars)
+ [] last_vars
in
+ let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
- (* calculate initial environment *)
- let data = edd_apply_cl (edd_top ve) init_cl in
- Format.printf "Init: @[<hov>%a@]@." edd_print data;
- { rp; opt; ve;
- cl; cl_g; guarantees;
- cycle; forget; data }
+ { rp; opt; ve; last_vars; all_vars;
+ init_f; cl; cl_g; guarantees;
+ cycle; forget }
@@ -1094,7 +1092,8 @@ end = struct
end
in
- let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+ 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
(* Dump final state *)
let acc = ch_it 0 init_acc in
@@ -1124,13 +1123,13 @@ end = struct
end;
(* Examine probes *)
- if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+ if List.exists (fun (p, _, _) -> p) e.all_vars then begin
let final_flat = edd_forget_vars final
(List.fold_left
(fun l (_, id, ty) -> match ty with
| TInt | TReal -> l
| TEnum _ -> id::l)
- [] e.rp.all_vars) in
+ [] e.all_vars) in
let final_flat = match final_flat.root with
| DTop -> ND.top e.ve.nvars
| DBot -> ND.bottom e.ve.nvars
@@ -1146,7 +1145,7 @@ end = struct
ND.print_itv (ND.project final_flat id)
| TEnum _ -> Format.printf "%a : enum variable@."
Formula_printer.print_id id)
- e.rp.all_vars;
+ e.all_vars;
Format.printf "@]@."
end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 01f6655..9c0ff71 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -51,7 +51,8 @@ type bool_expr =
| BNot of bool_expr
let f_and a b = match a, b with
- | BConst false, _ | _, BConst false -> BConst false
+ | BConst false, _ | _, BConst false
+ | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false
| BConst true, b -> b
| a, BConst true -> a
| a, b -> BAnd(a, b)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index dcb4049..1cbc27d 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,14 @@ open Typing
open Interpret (* used for constant evaluation ! *)
-(* Transform SCADE program to logical formula. *)
+(* Transform SCADE program to logical formula.
+
+ Convention : to access the last value of a variable,
+ access the variable with the same name prefixed by "L".
+ A pre-processing pass will extract the variables that are
+ referenced in such a way so that they are taken into
+ account when calculating the memory.
+*)
(* node * prefix * equations *)
type scope = id * id * eqn ext list
@@ -72,7 +79,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
let typ = type_expr td.rp node expr in
where
(List.mapi
- (fun i t -> let x = id^"."^(string_of_int i) in
+ (fun i t -> let x = "L"^id^"."^(string_of_int i) in
match t with
| TInt -> NE(NIdent x, false)
| TReal -> NE(NIdent x, true)
@@ -190,40 +197,56 @@ and f_of_expr td (node, prefix, clock_scope) expr =
Translate program into one big formula
*)
+let reset_cond rst_exprs =
+ List.fold_left f_or (BConst false) rst_exprs
+let no_reset_cond rst_exprs =
+ List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs
+
let clock_scope_here (node, prefix, _) =
node^"/"^prefix
-let gen_clock td (node, prefix, _) active =
+let gen_clock td (node, prefix, _) active rst_exprs =
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"), false),
- false)
- 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"), false)
- 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)
+ f_or
+ (f_and (reset_cond rst_exprs)
+ (f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
+ else BConst true)))
+ (f_and (no_reset_cond rst_exprs)
+ (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 f_e_eq (EIdent(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(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
- clock_scope, clock_eq
+ (clock_scope, rst_exprs), clock_eq
-let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
+let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
- let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
+ let eq = f_of_scope active td (node^"/"^id, "", eqs)
+ cs assume_guarantees in
if active then
let arg_eq ((_,argname,ty), expr) =
f_of_neexpr td (node, prefix, clock_scope) (function
@@ -247,7 +270,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
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
+ (fun i v -> let x = (id^"."^(string_of_int i)) in
match v with
| NE (v, r) -> BRel(AST_EQ, NIdent x, v, r)
| EE v -> f_e_eq (EIdent x) v)
@@ -257,11 +280,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let typ = type_expr td.rp node expr in
list_fold_op f_and
(List.mapi
- (fun i t -> let x = string_of_int i in
+ (fun i t -> let id_x = id ^ "." ^ string_of_int i in
match t with
- | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false)
- | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true)
- | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
+ | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false)
+ | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true)
+ | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x)))
typ)
in
let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
@@ -323,8 +346,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let rec do_tree_act = function
| AST_activate_body b ->
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)
+ let cs2, clock_eq = gen_clock td b_scope true rst_exprs in
+ f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees)
| AST_activate_if(c, a, b) ->
f_or
(f_and (f_of_expr td (node, prefix, clock_scope) c)
@@ -334,29 +357,37 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
and do_tree_inact = function
| AST_activate_body b ->
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)
+ let cs2, clock_eq = gen_clock td b_scope false rst_exprs in
+ f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees)
| AST_activate_if(_, a, b) ->
f_and (do_tree_inact a) (do_tree_inact b)
in
f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
| AST_automaton (aid, states, _) ->
+ let (init_st, _) = List.find (fun (st, _) -> st.initial) states in
+ let lnstv = "L"^node^"/"^aid^".next_state" in
+ let nstv = node^"/"^aid^".next_state" in
let stv = node^"/"^aid^".state" in
- let nstv = "N"^node^"/"^aid^".state" in
+ let st_choice_eq =
+ f_or
+ (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name)))
+ (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
+ in
+
let st_eq_inact (st, _) =
let st_scope = node, aid^"."^st.st_name^".", st.body in
- let clock_scope, clock_eq = gen_clock td st_scope false in
+ let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in
f_and clock_eq
(f_and
- (f_of_scope false td st_scope clock_scope assume_guarantees)
+ (f_of_scope false td st_scope cs 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_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 cs2, clock_eq = gen_clock td st_scope true rst_exprs in
+ let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in
let rec aux = function
| [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
| (c, (target, l), rst)::q ->
@@ -372,9 +403,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
(f_and (BEnumCons(E_NE, stv, EItem st.st_name))
(st_eq_inact (st, l)))
in
- f_and_list (List.map st_eq_act states)
+ f_and st_choice_eq
+ (f_and_list (List.map st_eq_act states))
else
- f_and_list (List.map st_eq_inact states)
+ f_and st_choice_eq
+ (f_and_list (List.map st_eq_inact states))
in
f_and_list (List.map do_eq eqs)
@@ -384,77 +417,32 @@ and f_of_prog rp assume_guarantees =
consts = I.consts rp;
} in
- let clock_scope, clock_eq = gen_clock td rp.root_scope true in
-
- let scope_f =
- f_of_scope
- true
- td td.rp.root_scope
- clock_scope
- assume_guarantees in
- f_and clock_eq scope_f
-
+ let prog_normal =
+ let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in
-(*
- Translate init state into a formula
-*)
-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, false)
- 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 scope_f =
+ f_of_scope
+ true
+ td td.rp.root_scope
+ clock_scope
+ assume_guarantees in
+ f_and clock_eq scope_f
+ in
+ let prog_init =
+ let clock_scope, clock_eq =
+ gen_clock td rp.root_scope true [BConst true] in
-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) clock_scope
+ let scope_f =
+ f_of_scope
+ true
+ td td.rp.root_scope
+ clock_scope
+ assume_guarantees in
+ f_and clock_eq scope_f
in
- List.fold_left (fun x i -> f_and (instance_eq i) x)
- (BConst true) (extract_instances rp.p e)
- in
- let do_eq eq = match fst eq with
- | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
- expr_eq e
- | AST_activate (b, _) ->
- let rec cond_eq = function
- | AST_activate_body b ->
- 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))
- in
- cond_eq b
- | AST_automaton (aid, states, _) ->
- let (st, _) = List.find (fun (st, _) -> st.initial) states in
- let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
- let state_eq (st, _) =
- let sc_f =
- 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
- f_and_list (List.map do_eq eqs)
+ prog_init, prog_normal
+
-and init_f_of_prog rp =
- 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
@@ -502,3 +490,30 @@ and guarantees_of_prog rp =
g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true)
+
+
+(*
+ Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+ | BRel(_, a, b, _) ->
+ elv_ne a @ elv_ne b
+ | BEnumCons c ->
+ elv_ec c
+ | BAnd(a, b) | BOr (a, b) ->
+ extract_last_vars a @ extract_last_vars b
+ | BNot(e) -> extract_last_vars e
+ | _ -> []
+
+and elv_ne = function
+ | NIdent i when i.[0] = 'L' -> [i]
+ | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+ | NUnary (_, a, _) -> elv_ne a
+ | _ -> []
+
+and elv_ec (_, v, q) =
+ (if v.[0] = 'L' then [v] else []) @
+ (match q with
+ | EIdent i when i.[0] = 'L' -> [i]
+ | _ -> [])
diff --git a/cmdline.ml b/cmdline.ml
new file mode 100644
index 0000000..b8f8ea8
--- /dev/null
+++ b/cmdline.ml
@@ -0,0 +1,8 @@
+open Ast
+
+type cmdline_opt = {
+ widen_delay : int;
+ disjunct : (id -> bool);
+ verbose_ci : bool;
+ vverbose_ci : bool;
+}
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 2859230..d814bbe 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -129,15 +129,12 @@ let clock_vars rp (node, prefix, _) =
let v =
if not (rp.no_time_scope (node^"/"^prefix))
then
- [
- false, node^"/"^prefix^"time", TInt;
- false, "N"^node^"/"^prefix^"time", TInt]
+ [false, node^"/"^prefix^"time", TInt]
else [] in
let v =
if rp.init_scope (node^"/"^prefix)
then
- (false, node^"/"^prefix^"init", bool_type)::
- (false, "N"^node^"/"^prefix^"init", bool_type)::v
+ (false, node^"/"^prefix^"init", bool_type)::v
else v in
v
@@ -145,9 +142,7 @@ let clock_vars rp (node, prefix, _) =
extract_all_vars : rooted_prog -> scope -> var list
Extracts all variables with names given according to
- naming convention used here and in transform.ml :
- - pre variables are not prefixed by scope
- - next values for variables are prefixed by capital N
+ naming convention used here and in transform.ml
*)
let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let vars_of_expr e =
@@ -162,12 +157,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(List.map
(fun (id, expr) ->
let id = node^"/"^id in
- let vd =
- List.mapi
- (fun i t -> false, id^"."^(string_of_int i), t)
- (type_expr_vl rp.p n_vars rp.const_vars node expr)
- in
- vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+ List.mapi
+ (fun i t -> false, id^"."^(string_of_int i), t)
+ (type_expr_vl rp.p n_vars rp.const_vars node expr))
(extract_pre e))
in
let vars_of_eq e = match fst e with
@@ -206,14 +198,14 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let st_scope = (node, aid^"."^st.st_name^".", st.body) in
let svars = vars_in_node node st.st_locals in
(if st.i_rst || st.o_rst then
- [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type]
+ [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
else [])
@ svars @ tvars @ clock_vars rp st_scope @
extract_all_vars rp st_scope (tvars@n_vars)
in
let st_ids = List.map (fun (st, _) -> st.st_name) states in
(false, node^"/"^aid^".state", TEnum st_ids)::
- (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+ (false, node^"/"^aid^".next_state", TEnum st_ids)::
(List.flatten (List.map do_state states))
in
let v = List.flatten (List.map vars_of_eq eqs) in
@@ -247,6 +239,7 @@ let root_prog p root no_time_scope init_scope =
let root_vars = 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 @ root_vars @ extract_all_vars rp root_scope root_vars }
+ { rp with all_vars = root_clock_vars @
+ root_vars @ extract_all_vars rp root_scope root_vars }
diff --git a/libs/util.ml b/libs/util.ml
index 940fe3e..6e8dc59 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -13,7 +13,7 @@ let rec uniq_sorted = function
(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *)
let rec list_fold_op op = function
- | [] -> invalid_arg "list_fold_opt on empty list"
+ | [] -> invalid_arg "list_fold_op on empty list"
| [a] -> a
| x::q -> op x (list_fold_op op q)
diff --git a/main.ml b/main.ml
index 5e9f087..a02820c 100644
--- a/main.ml
+++ b/main.ml
@@ -1,16 +1,19 @@
+open Cmdline
+
open Ast
open Num_domain
open Nonrelational
open Apron_domain
-open Abs_interp
module Interpret = Interpret.I
module ItvND = Nonrelational.ND(Intervals_domain.VD)
+(*
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
+*)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
@@ -123,8 +126,10 @@ let () =
vverbose_ci = !ai_vvci;
} in
+ (*
if !ai_itv then AI_Itv.do_prog opt rp;
if !ai_rel then AI_Rel.do_prog opt rp;
+ *)
if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;