Module ReachabilityTree.Make.Vertex
module Vertex:Module to manage vertices. Each vertex may belong to at most one tree.sig..end
include Print.PRINTABLE_TYPE
The printable type of vertices.
val location : t -> A.Automaton.Location.tlocation u returns the location of the vertex u.val region : t -> A.Semantics.Region.tregion u returns the region of the vertex u.val mark : t -> Mark.tmark u returns the mark of the vertex u.val refine : t -> A.Semantics.Region.t -> unitrefine u reg replaces the region of u by reg.
Precondition
reg is contained in the region of u.Vertices are ordered (see
Set.OrderedType or Map.OrderedType) and
hashable (see Hashtbl.HashedType).val compare : t -> t -> int
Total ordering over vertices (creation order).
val equal : t -> t -> bool
Equality predicate on vertices.
val hash : t -> int
Hashing function on vertices.