Functor Search.Make
module Make:Functor providing a printable type for paths together with graph exploration functions for a given multi-graph implementation.
Parameters: |
|
module Path:Print.PRINTABLE_TYPE
with type t = G.Edge.t list
The printable type of paths.
type
traversal =
| |
Forward_path of |
(* | forward path, verifying G.Edge.tgt e = G.Edge.src e' for any two
consecutive edges e and e' . | *) |
| |
Backward_path of |
(* | backward path, verifying G.Edge.tgt e' = G.Edge.src e for any two
consecutive edges e and e' . | *) |
| |
Forward_reach of |
(* | forward reachability set, closed under successor. | *) |
| |
Backward_reach of |
(* | backward reachability set, closed under predecessor. | *) |
Type of possible results of the graph exploration functions provided by
this module.
Forward_path p
: the pathp
verifiesG.Edge.tgt e = G.Edge.src e'
for any two consecutive edgese
ande'
inp
.Backward_path p
: the pathp
verifiesG.Edge.tgt e' = G.Edge.src e
for any two consecutive edgese
ande'
inp
.Forward_reach s
: the sets
of vertices (given as a list) contains all its successors.Backward_reach s
: the sets
of vertices (given as a list) contains all its predecessors.
Note that if the traversal result is Backward_path p
then the path p
must be reversed (e.g. with List.rev p
) to get it in the proper order.
The following graph exploration functions look for a path from a vertex in a given list
initial
of vertices to a vertex in a given list final
of
vertices. The lists initial
and final
are assumed to be disjoint.
Each exploration function returns:
- either
*_path p
if a pathp
was found, - or
*_reach s
otherwise, wheres
is the list of reachable vertices (s
is the list of all visited vertices).
Forward exploration functions return only Forward_*
results and backward
exploration functions return only Backward_*
results.
To simply compute the forward (resp. backward) reachability set of a given
list of initial (resp. final) vertices, use an empty list of final (resp.
initial) vertices.
val fwd_dfs : Search.G.t ->
Search.G.Vertex.t list -> Search.G.Vertex.t list -> traversal
fwd_dfs g initial final
looks for a path from initial
to final
, by a
forward depth-first exploration of the multi-graph g
.
Precondition
initial
and final
are disjoint, and they are both
contained in g
.val fwd_bfs : Search.G.t ->
Search.G.Vertex.t list -> Search.G.Vertex.t list -> traversal
fwd_bfs g initial final
looks for a path from initial
to final
, by a
forward breadth-first exploration of the multi-graph g
.
Precondition
initial
and final
are disjoint, and they are both
contained in g
.val bwd_dfs : Search.G.t ->
Search.G.Vertex.t list -> Search.G.Vertex.t list -> traversal
bwd_dfs g initial final
looks for a path from initial
to final
, by a
backward depth-first exploration of the multi-graph g
.
Precondition
initial
and final
are disjoint, and they are both
contained in g
.val bwd_bfs : Search.G.t ->
Search.G.Vertex.t list -> Search.G.Vertex.t list -> traversal
bwd_bfs g initial final
looks for a path from initial
to final
, by a
backward breadth-first exploration of the multi-graph g
.
Precondition
initial
and final
are disjoint, and they are both
contained in g
.