summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abstract/abs_domain.ml308
-rw-r--r--abstract/abs_interp.ml37
-rw-r--r--abstract/formula_printer.ml2
-rw-r--r--abstract/nonrelational.ml2
-rw-r--r--abstract/transform.ml63
-rw-r--r--frontend/ast_util.ml1
-rw-r--r--frontend/typing.ml71
-rw-r--r--libs/util.ml6
8 files changed, 418 insertions, 72 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index a7f5455..a30713a 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -4,6 +4,11 @@ open Num_domain
open Typing
open Util
+type disjunct_policy =
+ | DAlways
+ | DNever
+ | DSometimes
+
module type ENVIRONMENT_DOMAIN = sig
type t
type itv
@@ -21,6 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig
val forgetvar : t -> id -> t
val var_itv : t -> id -> itv
+ val set_disjunct : t -> id -> disjunct_policy -> t
(* set_theoretic operations *)
val join : t -> t -> t (* union *)
@@ -33,7 +39,7 @@ module type ENVIRONMENT_DOMAIN = sig
(* abstract operations *)
val apply_f : t -> bool_expr -> t
val apply_cl : t -> conslist -> t
- val assign : t -> (id * num_expr) list -> t
+ val assign : t -> (id * id) list -> t
(* pretty-printing *)
val print_vars : Format.formatter -> t -> id list -> unit
@@ -42,19 +48,13 @@ module type ENVIRONMENT_DOMAIN = sig
end
-module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
-
- type enum_valuation = (string * string) list
-
- module VMapKey = struct
- type t = enum_valuation VarMap.t
- let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b))
- end
- module VMap = Mapext.Make(VMapKey)
+module D_ignore_enum (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
+struct
type t = ND.t
type itv = ND.itv
+
let init = ND.init
let bottom = ND.bottom
let vbottom = ND.vbottom
@@ -66,6 +66,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let forgetvar = ND.forgetvar
let var_itv = ND.var_itv
+ let set_disjunct x _ _ = x
let join = ND.join
let meet = ND.meet
@@ -88,10 +89,295 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let apply_f x f = apply_cl x (conslist_of_f f)
- let assign = ND.assign
+ let assign x v = ND.assign x (List.map (fun (id, id2) -> id, NIdent id2) v)
let print_vars = ND.print_vars
let print_all = ND.print_all
let print_itv = ND.print_itv
+end
+
+module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+
+ module Valuation = struct
+ type t = string VarMap.t
+ let compare = VarMap.compare Pervasives.compare
+
+ let subset a b =
+ VarMap.for_all
+ (fun id v ->
+ try v = VarMap.find id b
+ with Not_found -> true)
+ a
+
+ let print fmt x =
+ let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x) in
+ let s = List.sort Pervasives.compare b in
+ let rec bl = function
+ | [] -> []
+ | (v, id)::q ->
+ begin match bl q with
+ | (vv, ids)::q when vv = v -> (v, id::ids)::q
+ | r -> (v, [id])::r
+ end
+ in
+ let sbl = bl s in
+ Format.fprintf fmt "@[<v 2>{ ";
+ List.iteri
+ (fun j (v, ids) ->
+ if j > 0 then Format.fprintf fmt "@ ";
+ Format.fprintf fmt "@[<hov 4>";
+ List.iteri
+ (fun i id ->
+ if i > 0 then Format.fprintf fmt ",@ ";
+ Format.fprintf fmt "%a" Formula_printer.print_id id)
+ ids;
+ Format.fprintf fmt " = %s@]" v)
+ sbl;
+ Format.fprintf fmt " }@]"
+
+ end
+ module VMap = Mapext.Make(Valuation)
+
+ type t = {
+ nvars : (id * bool) list;
+ evars : (id * string list) list;
+ nd_init : ND.t;
+ nd_bottom : ND.t;
+ value : ND.t VMap.t;
+ disj_v : id list;
+ nodisj_v : id list;
+ }
+ type itv =
+ | IN of ND.itv VMap.t
+ | IE of SSet.t
+
+
+ let init = {
+ nvars = []; evars = []; disj_v = []; nodisj_v = [];
+ nd_init = ND.init;
+ nd_bottom = ND.bottom;
+ value = VMap.singleton VarMap.empty ND.init;
+ }
+ let bottom = {
+ nvars = []; evars = []; disj_v = []; nodisj_v = [];
+ nd_init = ND.init;
+ nd_bottom = ND.bottom;
+ value = VMap.empty;
+ }
+ let vbottom x = { x with value = VMap.empty }
+
+ let is_bot x = VMap.is_empty x.value || VMap.for_all (fun _ v -> ND.is_bot v) x.value
+
+ let strict value =
+ VMap.filter (fun _ v -> not (ND.is_bot v)) value
+
+ let add_case 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
+ value
+ else
+ try VMap.add enum (ND.join num (VMap.find enum value)) value
+ with Not_found -> VMap.add enum num value
+ in { x with value = v }
+
+ let addvar x id ty = match ty with
+ | TInt | TReal ->
+ let is_real = (ty = TReal) in
+ { x with
+ nvars = (id, is_real)::(x.nvars);
+ nd_init = ND.addvar x.nd_init id is_real;
+ nd_bottom = ND.addvar x.nd_bottom id is_real;
+ value = VMap.map (fun v -> ND.addvar v id is_real) x.value
+ }
+ | TEnum options ->
+ { x with
+ evars = (id, options)::x.evars
+ }
+
+ let vars x =
+ List.map (fun (id, r) -> id, if r then TReal else TInt) x.nvars @
+ List.map (fun (id, o) -> id, TEnum o) x.evars
+
+ let forgetvar x id =
+ if List.mem_assoc id x.evars then
+ VMap.fold
+ (fun enum num value ->
+ let enum' = VarMap.remove id enum in
+ add_case value (enum', num))
+ x.value
+ { x with value = VMap.empty }
+ else
+ { x with value = strict @@ VMap.map (fun v -> ND.forgetvar v id) x.value }
+
+ let rmvar x id =
+ if List.mem_assoc id x.evars then
+ let y = forgetvar x id in
+ { y with
+ evars = List.remove_assoc id x.evars }
+ else
+ { x with
+ nvars = List.remove_assoc id x.nvars;
+ value = strict @@ VMap.map (fun v -> ND.rmvar v id) x.value }
+
+ let var_itv x id =
+ if List.mem_assoc id x.nvars
+ then IN (VMap.map (fun v -> ND.var_itv v id) x.value)
+ else not_implemented "var_itv for enum variable"
+
+ let set_disjunct x id p =
+ { x with
+ disj_v = (if p = DAlways then id::x.disj_v
+ else List.filter ((<>) id) x.disj_v);
+ nodisj_v = (if p = DNever then id::x.nodisj_v
+ else List.filter ((<>) id) x.nodisj_v);
+ }
+
+ let join x y =
+ VMap.fold
+ (fun enum num value -> add_case value (enum, num))
+ x.value
+ y
+ 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 }
+
+ (* Some cases of subset/equality not detected *)
+ let subset a b =
+ VMap.for_all
+ (fun enum num ->
+ VMap.exists
+ (fun enum_b num_b ->
+ Valuation.subset enum enum_b && ND.subset num num_b)
+ b.value)
+ a.value
+ let eq a b = subset a b && subset b a
+
+ (* Constraints ! *)
+ let apply_ec x (op, a, b) =
+ 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)
+ then add_case value (enum, num)
+ else value
+ with Not_found ->
+ if op = E_EQ
+ then add_case value (VarMap.add i u enum, num)
+ else (* MAKE A DISJUNCTION *)
+ List.fold_left
+ (fun value item ->
+ add_case value (VarMap.add i item enum, num))
+ value
+ (List.filter ((<>) u) (List.assoc i x.evars))
+ end
+ | EIdent 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)
+ then add_case value (enum, num)
+ else value
+ with Not_found (* J not found *) ->
+ add_case value (VarMap.add j x enum, num)
+ with Not_found (* I not found *) ->
+ try let y = VarMap.find j enum in
+ add_case value (VarMap.add i y enum, num)
+ with Not_found (* J not found *) ->
+ if op = E_EQ
+ then (* MAKE A DISJUNCTION ! *)
+ List.fold_left
+ (fun value item ->
+ let enum = VarMap.add i item enum in
+ let enum = VarMap.add j item enum in
+ add_case value (enum, num))
+ value
+ (List.assoc i x.evars)
+ else
+ add_case value (enum, num)
+ end)
+ x.value
+ { x with value = VMap.empty }
+
+ let apply_ecl x cons =
+ let f x = List.fold_left apply_ec x cons in
+ fix eq f x
+
+
+ let apply_ncl x econs =
+ { x with value = strict @@ VMap.map (fun x -> ND.apply_ncl x econs) x.value }
+
+ let rec apply_cl x (econs, ncons, rest) = match rest with
+ | CLTrue ->
+ let y = apply_ecl x econs in
+ let z = apply_ncl y ncons in
+ z
+ | CLFalse -> vbottom x
+ | CLAnd(a, b) ->
+ let y = apply_cl x (econs, ncons, a) in
+ apply_cl y (econs, ncons, b)
+ | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
+ let y = apply_cl x (econs@eca, ncons@ca, ra) in
+ let z = apply_cl x (econs@ecb, ncons@cb, rb) in
+ join y z
+
+ let apply_f x f = apply_cl x (conslist_of_f f)
+
+ let assign x e =
+ let ee, ne = List.partition (fun (id, id2) -> List.mem_assoc id x.evars) e in
+ let ne_e = List.map (fun (id, id2) -> id, NIdent id2) ne in
+
+ VMap.fold
+ (fun enum0 num value ->
+ let enum = List.fold_left
+ (fun enum (id, id2) ->
+ try let y = VarMap.find id2 enum0 in
+ VarMap.add id y enum
+ with Not_found ->
+ VarMap.remove id enum)
+ enum0 ee
+ in
+ add_case value (enum, ND.assign num ne_e))
+ x.value
+ { x with value = VMap.empty }
+
+ let print_all fmt x =
+ Format.fprintf fmt "@[<v 0>";
+ VMap.iter
+ (fun enum num ->
+ Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ "
+ Valuation.print enum ND.print_all num)
+ x.value;
+ Format.fprintf fmt "@]"
+
+ let print_vars fmt x idl = print_all fmt x (* TODO *)
+
+ let print_itv fmt = function
+ | IN x ->
+ Format.fprintf fmt "@[<v 0>";
+ VMap.iter
+ (fun enum i ->
+ Format.fprintf fmt "%a when %a@ "
+ ND.print_itv i Valuation.print enum)
+ x;
+ Format.fprintf fmt "@]"
+ | IE x ->
+ Format.fprintf fmt "@[<hov 2>{ ";
+ SSet.iter (fun x -> Format.fprintf fmt "%s@ " x) x;
+ Format.fprintf fmt "}@]"
end
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 7950144..7a53134 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -52,6 +52,7 @@ end = struct
guarantees;
Format.printf "@.";
+ let env = E.set_disjunct env "/exit" DNever in
let env = E.apply_f env init_f in
let cl = Formula.conslist_of_f f in
@@ -72,7 +73,7 @@ end = struct
let tr_assigns = List.fold_left
(fun q (_, id, _) ->
if id.[0] = 'N' then
- (String.sub id 1 (String.length id - 1), NIdent id)::q
+ (String.sub id 1 (String.length id - 1), id)::q
else
q)
[] vars
@@ -95,14 +96,10 @@ end = struct
(*
loop : st -> env -> env -> env
*)
- let loop st pnew stay =
+ let loop st acc0 =
- Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
- Formula_printer.print_conslist st.cl
- E.print_all pnew E.print_all stay;
-
- let add_stay = cycle st st.cl pnew in
- let acc0 = E.join stay add_stay in
+ Format.printf "Loop @[<hv>%a@]@.@."
+ Formula_printer.print_conslist st.cl;
let fsharp cl i =
Format.printf "Acc @[<hv>%a@]@." E.print_all i;
@@ -121,7 +118,7 @@ end = struct
let x = iter 0 acc0 in
let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *)
- let z = E.apply_cl y st.cl in
+ let z = E.apply_cl y st.cl in (* no more guarantee *)
y, z
(*
@@ -130,20 +127,14 @@ end = struct
let do_prog widen_delay rp =
let st = init_state widen_delay rp in
- let pnew = st.env in
- let pnew_c = E.apply_cl pnew st.cl in
-
- let stay, stay_c = loop st pnew (E.vbottom pnew) in
-
- Format.printf "@.@[<hov>New %a@]@.@."
- E.print_all pnew_c;
- Format.printf "@[<hov>Stay %a@]@.@."
- E.print_all stay_c;
-
- let final = E.join pnew_c stay_c in
+ let final, final_c = loop st st.env in
- Format.printf "@[<hov>Final %a@]@.@."
+ Format.printf "@[<hov>F %a@]@.@."
E.print_all final;
+ (*
+ Format.printf "@[<hov>F' %a@]@.@."
+ E.print_all final_c;
+ *)
let check_guarantee (id, f) =
let cl = Formula.conslist_of_f f in
@@ -162,9 +153,9 @@ end = struct
end;
if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
- Format.printf "Probes:@[<v>";
+ Format.printf "Probes: @[<v 0>";
List.iter (fun (p, id, _) ->
- if p then Format.printf " %a ∊ %a@ "
+ if p then Format.printf "%a ∊ %a@ "
Formula_printer.print_id id
E.print_itv (E.var_itv final id))
st.rp.all_vars;
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 44f2d39..0c7d65e 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -59,7 +59,7 @@ let rec print_num_expr fmt e = match e with
(* Enumeated expressions *)
let print_enum_expr fmt = function
- | EIdent id -> Format.fprintf fmt "%s" id
+ | EIdent id -> print_id fmt id
| EItem x -> Format.fprintf fmt "%s" x
let str_of_enum_op = function
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 492b547..bbdc875 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -188,7 +188,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
match env with
| Bot -> Format.fprintf fmt "⊥"
| Env env ->
- Format.fprintf fmt "@[<v 2>{ ";
let l = List.map (fun id -> (get_var env id, id)) ids in
let s = List.sort Pervasives.compare l in
let rec bl = function
@@ -201,6 +200,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
| _::q -> bl q
in
let sbl = bl s in
+ Format.fprintf fmt "@[<v 2>{ ";
List.iteri
(fun j (v, ids) ->
if j > 0 then Format.fprintf fmt "@ ";
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 708456e..64fd8d8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -70,11 +70,19 @@ let rec f_of_neexpr td (node, prefix) where expr =
| TEnum _ -> EE(EIdent x))
typ)
| AST_arrow(a, b) ->
- f_or
- (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
- (sub where a))
- (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
- (sub where b))
+ if List.mem (node^"/") td.rp.init_scope
+ then
+ f_or
+ (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true))
+ (sub where a))
+ (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false))
+ (sub where b))
+ else
+ f_or
+ (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+ (sub where a))
+ (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+ (sub where b))
(* other *)
| AST_if(c, a, b) ->
f_or
@@ -261,12 +269,33 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
in
let time_incr_eq =
if active then
- BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
- NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
+ f_and
+ (if not (List.mem (node^"/") td.rp.no_time_scope)
+ 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))
else
- BRel(AST_EQ,
- NIdent("N"^node^"/"^prefix^"time"),
- NIdent(node^"/"^prefix^"time"))
+ f_and
+ (if not (List.mem (node^"/") td.rp.no_time_scope)
+ then BRel(AST_EQ,
+ 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))
in
List.fold_left f_and
time_incr_eq
@@ -306,9 +335,17 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
| AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
in
let time_eq =
- BRel(AST_EQ,
- NIdent(node^"/"^prefix^"time"),
- NIntConst 0)
+ f_and
+ (if not (List.mem (node^"/") rp.no_time_scope)
+ then
+ BRel(AST_EQ,
+ NIdent(node^"/"^prefix^"time"),
+ NIntConst 0)
+ else BConst true)
+ (if List.mem (node^"/") rp.init_scope
+ 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)
diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml
index b3393a7..d229f2f 100644
--- a/frontend/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -6,7 +6,6 @@ open Util
let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
let no_variable e = error ("No such variable: " ^ e)
let type_error e = error ("Type error: " ^ e)
-let not_implemented e = error ("Not implemented: " ^ e)
let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
(* Utility : find declaration of a const / a node *)
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 1545a38..a4abfe0 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -30,11 +30,16 @@ type var = bool * id * typ
type scope = id * id * eqn ext list
type rooted_prog = {
- p : prog;
- root_node : node_decl;
- root_scope : scope;
- all_vars : var list;
- const_vars : var list;
+ 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;
+ root_scope : scope;
+ all_vars : var list;
+ const_vars : var list;
}
(* Typing *)
@@ -120,14 +125,14 @@ let node_vars p f nid =
- pre variables are not prefixed by scope
- next values for variables are prefixed by capital N
*)
-let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars =
+let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let vars_of_expr e =
List.flatten
(List.map
(fun (f, id, eqs, args) ->
- let nv = node_vars p f (node^"/"^id) in
- nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars)
- (extract_instances p e))
+ let nv = node_vars rp.p f (node^"/"^id) in
+ nv @ extract_all_vars rp (node^"/"^id, "", eqs) nv)
+ (extract_instances rp.p e))
@
List.flatten
(List.map
@@ -135,7 +140,7 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars =
let vd =
List.mapi
(fun i t -> false, id^"."^(string_of_int i), t)
- (type_expr_vl p n_vars const_vars node expr)
+ (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))
(extract_pre e))
@@ -147,36 +152,58 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars =
| AST_activate_body b ->
let bvars = vars_in_node node b.act_locals in
bvars @
- extract_all_vars p
+ extract_all_vars rp
(node, b.act_id^".", b.body)
(bvars@n_vars)
- const_vars
| AST_activate_if(c, a, b) ->
vars_of_expr c @ do_branch a @ do_branch b
in do_branch b
| AST_automaton _ -> not_implemented "extract_all vars automaton"
in
- (false, node^"/"^prefix^"time", TInt)::
- (false, "N"^node^"/"^prefix^"time", TInt)::
- (List.flatten (List.map vars_of_eq eqs))
+ let v = List.flatten (List.map vars_of_eq eqs) in
+ let v =
+ if not (List.mem (node^"/") rp.no_time_scope)
+ then
+ (false, node^"/"^prefix^"time", TInt)::
+ (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)::
+ (false, "N"^node^"/"^prefix^"init", bool_type)::v
+ else v in
+ v
(*
root_prog : prog -> id -> rooted_prog
*)
let root_prog p root =
- let (n, _) = find_node_decl p root in
- let root_scope = ("", "", n.body) in
+ let (root_node, _) = find_node_decl p root in
+ let root_scope = ("", "", root_node.body) in
let const_vars = List.map
(fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ))
(extract_const_decls p)
in
- let root_vars = vars_in_node "" (decls_of_node n) in
-
- { p; root_scope; root_node = n;
- const_vars = const_vars;
- all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars }
+ let root_vars = vars_in_node "" (decls_of_node root_node) in
+
+ let rp = {
+ p; root_scope; root_node;
+
+ no_time_scope = ["/"];
+ act_scope = [];
+ init_scope = ["/"];
+
+ const_vars;
+ all_vars = [] } in
+
+ { rp with all_vars = root_vars @ extract_all_vars rp root_scope root_vars }
diff --git a/libs/util.ml b/libs/util.ml
index 6931ed9..01b0c5c 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -25,6 +25,8 @@ let loc_error l f x =
| NoLocError e -> raise (LocError([l], e))
| LocError(q, e) -> raise (LocError(l::q, e))
+let not_implemented e = error ("Not implemented: " ^ e)
+
(* Varmaps *)
module VarMap = Mapext.Make(String)
@@ -33,6 +35,10 @@ let disjoint_union k a b = match a, b with
| None, Some y -> Some y
| _ -> error ("Duplicate name in disjoint union: " ^ k)
+module SSet = Set.Make(String)
+
+(* Fixpoint *)
+
let rec fix equal f s =
let fs = f s in
if equal fs s
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 16:18:46 +0000