Functor ReachabilityTree.Make
module Make:
| Parameters: |
|
Reachability Tree Structure
include Print.PRINTABLE_TYPE
The printable type of reachability trees.
module Vertex:sig..end
Module to manage vertices.
module Edge:sig..end
The printable type of possible inbound edges for a vertex.
val edge : t -> Vertex.t -> Edge.tedge t u returns the inbound edge of the vertex u in the tree t.
Precondition
u is contained in t.val parent : t -> Vertex.t -> Vertex.t optionparent t u returns the parent of the vertex u in the tree t (if any).
Precondition
u is contained in t.val ancestor : t -> Vertex.t -> Vertex.t -> boolancestor t u v is true iff u is an ancestor of v in the tree t.
Precondition
u and v are contained in t.val create : unit -> tcreate () creates a new, empty reachability tree. The tree initially
contains no vertex (it only has a virtual root).val add_vertex : t ->
A.Automaton.Location.t ->
A.Semantics.Region.t ->
Mark.t -> Edge.t -> Vertex.tadd_vertex t loc reg m e creates a new vertex u with location loc,
region reg and mark m, and adds u to the tree t, with inbound edge
e. If the edge e is an initial region, then u is added as a child of
the root. Returns this new vertex u.
Precondition If the inbound edge
e is Child (p, tra) then p is
contained in t, tra's source is equal to p's location, and tra's
target is equal to loc.val del_vertex : t -> Vertex.t -> unitdel_vertex t u removes the vertex u, as well as its subtree, from the
tree t. All covering pairs involving a vertex in the subtree rooted in
u are removed from the covering relation of t. Deletion of a vertex is
permanent (i.e., vertices cannot be undeleted).
Precondition
u is contained in t.val mem_vertex : t -> Vertex.t -> boolmem_vertex t u tests whether the tree t contains the vertex u. Note
that each vertex may belong to at most one tree.val depth : t -> Vertex.t -> intdepth t u returns the depth of u in the tree t.
Precondition
u is contained in t.val has_children : t -> Vertex.t -> boolhas_children t u returns true iff the vertex u has at least one child
in the tree t.
Precondition
u is contained in t.Size Functions
val nb_vertices : t -> intnb_vertices t returns the number of vertices in the tree t.Covering Structure
The following functions manage covering relations. Each function has an implicit precondition over its arguments requiring that the given reachability tree contains the given vertices.
val add_covering : t -> Vertex.t -> Vertex.t -> unitadd_covering t v w adds the covering pair v ◅ w to the tree t.val del_covering : t -> Vertex.t -> Vertex.t -> unitdel_covering t v w removes the covering pair v ◅ w from the tree t.val clr_coverees : t -> Vertex.t -> unitclr_coverees t w removes all covering pairs · ◅ w from the tree t.val clr_coverers : t -> Vertex.t -> unitclr_coverers t v removes all covering pairs v ◅ · from the tree t.val has_coverees : t -> Vertex.t -> boolhas_coverees t w returns true iff there exists a covering pair · ◅ w
in the tree t.val has_coverers : t -> Vertex.t -> boolhas_coverers t v returns true iff there exists a covering pair v ◅ ·
in the tree t.val active : t -> Vertex.t -> boolactive t u returns true iff the vertex u is active in the tree t.Iterators
The following iterators apply a given function
f to some vertices of a
given reachability tree. Recall that the root is not considered to be
a vertex. Each vertex is passed at most once to the function f.
For added flexibility, tree traversal iterators apply two functions instead
of a single one: a pre-order operator and a post-order operator.Global Iterators
val iter_vertices : (Vertex.t -> unit) ->
(Vertex.t -> unit) ->
t -> Vertex.t option -> unititer_vertices pre post t u traverses the subtree of t rooted in u,
applying the pre-order operation pre and the post-order operation post
to all visited vertices. More precisely, iter_vertices pre post t u is
equivalent to begin
pre u ;
iter_children (iter_vertices pre post t) t u ;
post u
end.
If u is None, then u stands for the (virtual) root of the tree.val fold_vertices : (Vertex.t -> 'a -> 'a) ->
(Vertex.t -> 'a -> 'a) ->
t -> Vertex.t option -> 'a -> 'afold_vertices pre post t u a is similar to iter_vertices pre post t u,
but returns a value. More precisely, fold_vertices pre post t u a is
equivalent to begin
post u
(fold_children
(fold_vertices pre post t) t u
(pre u a))
end.
If u is None, then u stands for the (virtual) root of the tree.val iter_location : (Vertex.t -> unit) ->
t -> A.Automaton.Location.t -> unititer_location f t loc applies f in turn to all vertices of t with
location loc, in increasing order.val fold_location : (Vertex.t -> 'a -> 'a) ->
t -> A.Automaton.Location.t -> 'a -> 'afold_location f t loc a returns (f uN ... (f u2 (f u1 a))...), where
u1, ..., uN are the vertices of t with location loc, in increasing
order.Local Iterators
val iter_children : (Vertex.t -> unit) ->
t -> Vertex.t option -> unititer_children f t u applies f in turn to all children of u in t, in
increasing order.
If u is None, then u stands for the (virtual) root of the tree.
Precondition
u is a vertex contained in t.val fold_children : (Vertex.t -> 'a -> 'a) ->
t -> Vertex.t option -> 'a -> 'afold_children f t u a returns (f vN ... (f v2 (f v1 a))...), where v1,
..., vN are the children of u in t, in increasing order.
If u is None, then u stands for the (virtual) root of the tree.
Precondition
u is a vertex contained in t.Covering Iterators
val iter_coverees : (Vertex.t -> unit) ->
t -> Vertex.t -> unititer_coverees f t u applies f in turn to all coverees of u in t, in
increasing order.
Precondition
u is a vertex contained in t.val fold_coverees : (Vertex.t -> 'a -> 'a) ->
t -> Vertex.t -> 'a -> 'afold_coverees f t u a returns (f vN ... (f v2 (f v1 a))...), where v1,
..., vN are the coverees of u in t, in increasing order.
Precondition
u is a vertex contained in t.val iter_coverers : (Vertex.t -> unit) ->
t -> Vertex.t -> unititer_coverers f t u applies f in turn to all coverers of u in t, in
increasing order.
Precondition
u is a vertex contained in t.val fold_coverers : (Vertex.t -> 'a -> 'a) ->
t -> Vertex.t -> 'a -> 'afold_coverers f t u a returns (f vN ... (f v2 (f v1 a))...), where v1,
..., vN are the coverers of u in t, in increasing order.
Precondition
u is a vertex contained in t.