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.t
location u
returns the location of the vertex u
.val region : t -> A.Semantics.Region.t
region u
returns the region of the vertex u
.val mark : t -> Mark.t
mark u
returns the mark of the vertex u
.val refine : t -> A.Semantics.Region.t -> unit
refine 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.