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.t
edge 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 option
parent 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 -> bool
ancestor 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 -> t
create ()
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.t
add_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 -> unit
del_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 -> bool
mem_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 -> int
depth t u
returns the depth of u
in the tree t
.
Precondition
u
is contained in t
.val has_children : t -> Vertex.t -> bool
has_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 -> int
nb_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 -> unit
add_covering t v w
adds the covering pair v
◅ w
to the tree t
.val del_covering : t -> Vertex.t -> Vertex.t -> unit
del_covering t v w
removes the covering pair v
◅ w
from the tree t
.val clr_coverees : t -> Vertex.t -> unit
clr_coverees t w
removes all covering pairs · ◅ w
from the tree t
.val clr_coverers : t -> Vertex.t -> unit
clr_coverers t v
removes all covering pairs v
◅ · from the tree t
.val has_coverees : t -> Vertex.t -> bool
has_coverees t w
returns true
iff there exists a covering pair · ◅ w
in the tree t
.val has_coverers : t -> Vertex.t -> bool
has_coverers t v
returns true
iff there exists a covering pair v
◅ ·
in the tree t
.val active : t -> Vertex.t -> bool
active 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 -> unit
iter_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 -> 'a
fold_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 -> unit
iter_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 -> 'a
fold_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 -> unit
iter_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 -> 'a
fold_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 -> unit
iter_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 -> 'a
fold_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 -> unit
iter_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 -> 'a
fold_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
.