Commit a6c391bc authored by mcolange's avatar mcolange

Better Dbm interface.

parent fdc1114b
module type IDBM =
sig
type t
type fed_t
val create : int -> t
val set_init : t -> unit
val copy : t -> t
val hash : t -> int
val infty : int
val is_empty : t -> bool
val leq : t -> t -> bool
val to_fed : t -> fed_t
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 to_string : t -> string
end
module type IFED =
sig
type t
type dbm_t
val from_dbm : dbm_t -> t
val hash : t -> int
val is_empty : t -> bool
(* TODO replace this with an iterator *)
val to_dbm : t -> dbm_t list
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
end
module type BIG_IDBM =
sig
type dbm_t
type 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 Dbm : DBM
module Fed : FED
end
module UDbm : BIG_IDBM with type dbm_t = Udbml.Dbm.t =
struct
type dbm_t = Udbml.Dbm.t
type fed_t = Udbml.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
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.Fed
let to_dbm t =
let res = ref [] in
iter t (fun z -> res := z :: !res);
!res
let intersect t z =
let f = from_dbm z in
intersect t f
end
end
(*
module PDbm : BIG_IDBM =
struct
type dbm_t = Udbml.PDbm.t
type fed_t = Udbml.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 rec Dbm : DBM =
struct
end
and Fed : FED =
struct
end
end
*)
open Batteries
open Common
open Printf
open Udbml
open Dbm
open Uta
module type GEN_IDBM = Udbml.IDBM with type cindex_t = int and type bound_t = int
module type TIMED_AUTOMATON =
sig
module Dbm : GEN_IDBM
module Dbm : IDBM
type timed_automaton
type discrete_state
......@@ -43,10 +41,10 @@ sig
val is_controllable : timed_automaton -> edge -> bool
end
module GenericUAutomaton (Dbm : GEN_IDBM) =
module GenericUAutomaton (BDbm : BIG_IDBM) =
struct
module Dbm = Dbm
module Dbm = BDbm.Dbm
(** In contrast with Uta.expression used in the parser, the variables here are indexed
* by unique integer identifiers.
......@@ -387,20 +385,20 @@ struct
let aux = function
| GuardLeq(Clock(c), e) ->
let k = eval_disc_exp ta state e in
Dbm.constrain dbm (c, 0, (k, Dbm.DBM_WEAK))
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, Dbm.DBM_STRICT))
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, Dbm.DBM_WEAK))
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, Dbm.DBM_STRICT))
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, Dbm.DBM_WEAK));
Dbm.constrain dbm (c, 0, (k, Dbm.DBM_WEAK))
Dbm.constrain dbm (0, c, (-k, Udbml.Basic_types.DBM_WEAK));
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;
......@@ -467,16 +465,19 @@ struct
Dbm.set_init z;
(try
for i = 0 to dim - 1 do
Dbm.constrain z (i, 0, (0, Dbm.DBM_WEAK));
Dbm.constrain z (0, i, (0, Dbm.DBM_WEAK));
Dbm.constrain z (i, 0, (0, Udbml.Basic_types.DBM_WEAK));
Dbm.constrain z (0, i, (0, Udbml.Basic_types.DBM_WEAK));
done;
Dbm.up z;
let inv = (invariant_of_discrete_state ta ta.init) in
Dbm.intersect z inv;
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
);
assert(not (Dbm.is_empty z));
(ta.init, z)
)
let transitions_from ta state =
let committed = is_committed state in
......@@ -1083,5 +1084,3 @@ struct
end
module Uautomaton = GenericUAutomaton(Dbm)
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