Commit f30072cb authored by mcolange's avatar mcolange

Add Priced Zones, and update common Dbm interface.

parent 3811c218
......@@ -5,6 +5,7 @@ sig
type fed_t
val create : int -> t
val set_zero : t -> unit
val set_init : t -> unit
val copy : t -> t
val hash : t -> int
......@@ -18,7 +19,7 @@ sig
val constrain : t -> Udbml.Basic_types.clock_constraint_t -> unit
val up : t -> fed_t
val update_value : t -> Udbml.Basic_types.cindex_t -> Udbml.Basic_types.bound_t -> fed_t
val intersect : t -> t -> unit
val intersect : t -> Udbml_unpriced.Dbm.t -> unit
val to_string : t -> string
end
......@@ -38,8 +39,7 @@ sig
val up : t -> unit
val update_value : t -> Udbml.Basic_types.cindex_t -> Udbml.Basic_types.bound_t -> unit
val intersect : t -> t -> unit
val intersect : t -> dbm_t -> unit
val intersect : t -> Udbml_unpriced.Dbm.t -> unit
end
module type BIG_IDBM =
......@@ -54,17 +54,17 @@ sig
module Fed : FED
end
module UDbm : BIG_IDBM with type dbm_t = Udbml.Dbm.t =
module UDbm : BIG_IDBM with type dbm_t = Udbml_unpriced.Dbm.t =
struct
type dbm_t = Udbml.Dbm.t
type fed_t = Udbml.Fed.t
type dbm_t = Udbml_unpriced.Dbm.t
type fed_t = Udbml_unpriced.Fed.t
module type DBM = IDBM with type t = dbm_t and type fed_t := fed_t
module type FED = IFED with type t = fed_t and type dbm_t := dbm_t
module rec Dbm : DBM =
struct
include Udbml.Dbm
include Udbml_unpriced.Dbm
let to_fed z = Fed.from_dbm z
......@@ -80,7 +80,7 @@ struct
end
and Fed : FED =
struct
include Udbml.Fed
include Udbml_unpriced.Fed
let to_dbm t =
let res = ref [] in
......@@ -91,21 +91,40 @@ struct
end
end
(*
module PDbm : BIG_IDBM =
module PDbm : BIG_IDBM with type dbm_t = Udbml_priced.PDbm.t =
struct
type dbm_t = Udbml.PDbm.t
type fed_t = Udbml.PFed.t
type dbm_t = Udbml_priced.PDbm.t
type fed_t = Udbml_priced.PFed.t
module type DBM = IDBM with type t := dbm_t and type fed_t := fed_t
module type FED = IFED with type t := fed_t and type dbm_t := dbm_t
module type DBM = IDBM with type t = dbm_t and type fed_t := fed_t
module type FED = IFED with type t = fed_t and type dbm_t := dbm_t
module rec Dbm : DBM =
struct
include Udbml_priced.PDbm
let to_fed z = Fed.from_dbm z
let up z =
let f = to_fed z in
Fed.up f;
f
let update_value z c b =
let f = to_fed z in
Fed.update_value f c b;
f
end
and Fed : FED =
struct
include Udbml_priced.PFed
let to_dbm t =
let res = ref [] in
iter t (fun z -> res := z :: !res);
!res
let intersect t z = intersect_dbm t z
end
end
*)
......@@ -2,7 +2,7 @@ open Reachability
open TimedAutomaton
open Dbm
module Uautomaton : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t
module Uautomaton : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t
= GenericUAutomaton(UDbm)
type ta_discrete = Uautomaton.timed_automaton * Uautomaton.discrete_state
......
......@@ -60,7 +60,7 @@ end
(** LU abstraction
*)
module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t) :
module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) :
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.MDbm.Dbm.t =
struct
......@@ -70,7 +70,7 @@ struct
let extrapolate zone (ta, loc) =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
Udbml.Dbm.extrapolate_lu_bounds zone lbounds ubounds
Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds
end
......@@ -106,7 +106,7 @@ end
* and Z'_{x,y} < Z_{x,y}
* and Z'_{x,y} + (<, - L_y) < Z_{x,0}
*)
module Sri (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t) :
module Sri (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) :
INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.MDbm.Dbm.t =
struct
......@@ -116,7 +116,7 @@ struct
let inclusion (ta, loc) z1 z2 =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
Udbml.Dbm.closure_leq lbounds ubounds z1 z2
Udbml_unpriced.Dbm.closure_leq lbounds ubounds z1 z2
end
(** An abstract type for the walk order of a graph *)
......
......@@ -20,9 +20,9 @@ sig
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
val transitions_from : timed_automaton -> discrete_state -> transition list
val transition_fields : timed_automaton -> transition ->
(discrete_state * MDbm.Dbm.t * ClockSet.t * discrete_state)
val guard_of_transition : timed_automaton -> transition -> MDbm.Dbm.t
val invariant_of_discrete_state : timed_automaton -> discrete_state -> MDbm.Dbm.t
(discrete_state * UDbm.Dbm.t * ClockSet.t * discrete_state)
val guard_of_transition : timed_automaton -> transition -> UDbm.Dbm.t
val invariant_of_discrete_state : timed_automaton -> discrete_state -> UDbm.Dbm.t
val is_urgent_or_committed : timed_automaton -> discrete_state -> bool
val is_target : timed_automaton -> discrete_state -> bool
val lu_bounds : timed_automaton -> discrete_state -> int array -> int array -> unit
......@@ -142,8 +142,8 @@ struct
mutable query : query;
mutable lowerLU : int array array array;
mutable upperLU : int array array array;
guards_tbl : (_succinct_transition,Dbm.t) Hashtbl.t;
invars_tbl : Dbm.t LocHashtbl.t;
guards_tbl : (_succinct_transition,UDbm.Dbm.t) Hashtbl.t;
invars_tbl : UDbm.Dbm.t LocHashtbl.t;
}
......@@ -381,25 +381,25 @@ struct
let _guard_to_dbm ta state g =
let nclocks = VarContext.size ta.clocks in
let dbm = Dbm.create nclocks in
Dbm.set_init dbm;
let dbm = UDbm.Dbm.create nclocks in
UDbm.Dbm.set_init dbm;
let aux = function
| GuardLeq(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
UDbm.Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
| GuardLess(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_STRICT))
UDbm.Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_STRICT))
| GuardGeq(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_WEAK))
UDbm.Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_WEAK))
| GuardGreater(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_STRICT))
UDbm.Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_STRICT))
| GuardEqual(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_WEAK));
Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
UDbm.Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_WEAK));
UDbm.Dbm.constrain dbm (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
| _ as e -> failwith (sprintf "Bad Guard: %s" (string_of_guard ta [e]))
in
List.iter aux g;
......@@ -463,22 +463,8 @@ struct
let initial_extended_state ta =
let dim = (VarContext.size (clocks ta)) in
let z = Dbm.create dim in
Dbm.set_init z;
(try
for i = 0 to dim - 1 do
Dbm.constrain z (i, 0, (0, Udbml.Basic_types.DBM_WEAK));
Dbm.constrain z (0, i, (0, Udbml.Basic_types.DBM_WEAK));
done;
let lz = BDbm.Fed.to_dbm (Dbm.up z) in
match lz with
| [upz] ->
let inv = (invariant_of_discrete_state ta ta.init) in
Dbm.intersect upz inv;
assert(not (Dbm.is_empty upz));
(ta.init, upz)
| _ -> failwith "cannot happen"
with _ as e -> raise e
)
Dbm.set_zero z;
(ta.init, z)
let transitions_from ta state =
let committed = is_committed state in
......@@ -534,7 +520,7 @@ struct
_apply_edge ta state e2 state';
let g1 = _guard_to_dbm ta state.stateVars e1.edgeGuard in
let g2 = _guard_to_dbm ta state.stateVars e2.edgeGuard in
Dbm.intersect g1 g2;
UDbm.Dbm.intersect g1 g2;
(state, g1, (ClockSet.union e1.edgeReset e2.edgeReset), state')
let guard_of_transition ta tr =
......@@ -554,7 +540,7 @@ struct
| SyncTrans(state,e1,e2) ->
let g1 = _guard_to_dbm ta state.stateVars e1.edgeGuard in
let g2 = _guard_to_dbm ta state.stateVars e2.edgeGuard in
Dbm.intersect g1 g2;
UDbm.Dbm.intersect g1 g2;
Hashtbl.add ta.guards_tbl str g1;
g1
)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment