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) ->
        (ReachabilityTree.Make.Vertex.t -> '-> 'a) ->
        t -> ReachabilityTree.Make.Vertex.t option -> '-> 'a
      val iter_location :
        (ReachabilityTree.Make.Vertex.t -> unit) ->
        t -> A.Automaton.Location.t -> unit
      val fold_location :
        (ReachabilityTree.Make.Vertex.t -> '-> 'a) ->
        t -> A.Automaton.Location.t -> '-> 'a
      val iter_children :
        (ReachabilityTree.Make.Vertex.t -> unit) ->
        t -> ReachabilityTree.Make.Vertex.t option -> unit
      val fold_children :
        (ReachabilityTree.Make.Vertex.t -> '-> 'a) ->
        t -> ReachabilityTree.Make.Vertex.t option -> '-> 'a
      val iter_coverees :
        (ReachabilityTree.Make.Vertex.t -> unit) ->
        t -> ReachabilityTree.Make.Vertex.t -> unit
      val fold_coverees :
        (ReachabilityTree.Make.Vertex.t -> '-> 'a) ->
        t -> ReachabilityTree.Make.Vertex.t -> '-> 'a
      val iter_coverers :
        (ReachabilityTree.Make.Vertex.t -> unit) ->
        t -> ReachabilityTree.Make.Vertex.t -> unit
      val fold_coverers :
        (ReachabilityTree.Make.Vertex.t -> '-> 'a) ->
        t -> ReachabilityTree.Make.Vertex.t -> '-> 'a
    end