functor (A : Model.S) ->
functor (Mark : Util.Print.PRINTABLE_TYPE) ->
sig
type t
val print : Format.formatter -> t -> unit
module Vertex :
sig
type t
val print : Format.formatter -> t -> unit
val location : t -> A.Automaton.Location.t
val region : t -> A.Semantics.Region.t
val mark : t -> Mark.t
val refine : t -> A.Semantics.Region.t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
end
module Edge :
sig
type t =
Init of A.Semantics.Region.t
| Child of
(ReachabilityTree.Make.Vertex.t * A.Automaton.Transition.t)
val print : Format.formatter -> t -> unit
end
val edge :
t -> ReachabilityTree.Make.Vertex.t -> ReachabilityTree.Make.Edge.t
val parent :
t ->
ReachabilityTree.Make.Vertex.t ->
ReachabilityTree.Make.Vertex.t option
val ancestor :
t ->
ReachabilityTree.Make.Vertex.t ->
ReachabilityTree.Make.Vertex.t -> bool
val create : unit -> t
val add_vertex :
t ->
A.Automaton.Location.t ->
A.Semantics.Region.t ->
Mark.t ->
ReachabilityTree.Make.Edge.t -> ReachabilityTree.Make.Vertex.t
val del_vertex : t -> ReachabilityTree.Make.Vertex.t -> unit
val mem_vertex : t -> ReachabilityTree.Make.Vertex.t -> bool
val depth : t -> ReachabilityTree.Make.Vertex.t -> int
val has_children : t -> ReachabilityTree.Make.Vertex.t -> bool
val nb_vertices : t -> int
val add_covering :
t ->
ReachabilityTree.Make.Vertex.t ->
ReachabilityTree.Make.Vertex.t -> unit
val del_covering :
t ->
ReachabilityTree.Make.Vertex.t ->
ReachabilityTree.Make.Vertex.t -> unit
val clr_coverees : t -> ReachabilityTree.Make.Vertex.t -> unit
val clr_coverers : t -> ReachabilityTree.Make.Vertex.t -> unit
val has_coverees : t -> ReachabilityTree.Make.Vertex.t -> bool
val has_coverers : t -> ReachabilityTree.Make.Vertex.t -> bool
val active : t -> ReachabilityTree.Make.Vertex.t -> bool
val iter_vertices :
(ReachabilityTree.Make.Vertex.t -> unit) ->
(ReachabilityTree.Make.Vertex.t -> unit) ->
t -> ReachabilityTree.Make.Vertex.t option -> unit
val fold_vertices :
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
t -> ReachabilityTree.Make.Vertex.t option -> 'a -> 'a
val iter_location :
(ReachabilityTree.Make.Vertex.t -> unit) ->
t -> A.Automaton.Location.t -> unit
val fold_location :
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
t -> A.Automaton.Location.t -> 'a -> 'a
val iter_children :
(ReachabilityTree.Make.Vertex.t -> unit) ->
t -> ReachabilityTree.Make.Vertex.t option -> unit
val fold_children :
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
t -> ReachabilityTree.Make.Vertex.t option -> 'a -> 'a
val iter_coverees :
(ReachabilityTree.Make.Vertex.t -> unit) ->
t -> ReachabilityTree.Make.Vertex.t -> unit
val fold_coverees :
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
t -> ReachabilityTree.Make.Vertex.t -> 'a -> 'a
val iter_coverers :
(ReachabilityTree.Make.Vertex.t -> unit) ->
t -> ReachabilityTree.Make.Vertex.t -> unit
val fold_coverers :
(ReachabilityTree.Make.Vertex.t -> 'a -> 'a) ->
t -> ReachabilityTree.Make.Vertex.t -> 'a -> 'a
end
Loading...