Functor ReachabilityTree.Make


module Make: 
functor (A : Model.S) ->
functor (Mark : Util.Print.PRINTABLE_TYPE) -> sig .. end
Parameters:
A : Model.S
Mark : Util.Print.PRINTABLE_TYPE


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 vw to the tree t.
val del_covering : t -> Vertex.t -> Vertex.t -> unit
del_covering t v w removes the covering pair vw 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.