Commit abbf279e authored by mcolange's avatar mcolange

Timed automaton now export the type of their discrete states as a hashed type...

Timed automaton now export the type of their discrete states as a hashed type (for use in hashtable).
parent 15a486c0
......@@ -11,9 +11,10 @@ sig
type discrete_state
type transition
module DS : Hashtbl.HashedType with type t = discrete_state
val clocks : timed_automaton -> string VarContext.t
val is_state_equal : discrete_state -> discrete_state -> bool
val hash_discrete_state : discrete_state -> int
val initial_discrete_state : timed_automaton -> discrete_state
(* does it belong here? If so, so does type for extended_state... *)
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
......@@ -485,6 +486,12 @@ struct
&&
(aux_var s.stateVars t.stateVars (Array.length s.stateVars - 1))
module DS = struct
type t = discrete_state
let equal = is_state_equal
let hash = hash_discrete_state
end
let initial_discrete_state ta = ta.init
let invariant_of_discrete_state ta state =
......
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