Module Graph__WeakTopological
Weak topological ordering of the vertices of a graph, as described by François Bourdoncle.
Weak topological ordering is an extension of topological ordering for potentially cyclic graphs.
A hierarchical ordering of a set is a well-parenthesized permutation of its elements with no consecutive (
. The elements between two parentheses are called a component, and the first elements of a component is called the head. A weak topological ordering of a graph is a hierarchical ordering of its vertices such that for every edge u -> v
of the graph, either u
comes (strictly) before v
, or v
is the head of a component containing u
.
One may notice that :
- For an acyclic graph, every topological ordering is also a weak topological ordering.
- For any graph with the vertices
v1, ..., vN
, the following trivial weak topological ordering is valid :(v1 (v2 (... (vN))...))
.
Weak topological ordering are useful for fixpoint computation (see ChaoticIteration
). This module aims at computing weak topological orderings which improve the precision and the convergence speed of these analyses.
- author
- Thibault Suzanne
- see Efficient chaotic iteration strategies with widenings
, François Bourdoncle, Formal Methods in Programming and their Applications, Springer Berlin Heidelberg, 1993
module type G = sig ... end
Minimal graph signature for the algorithm
type 'a element
=
|
Vertex of 'a
|
Component of 'a * 'a t
The type of the elements of a weak topological ordering over a set of
'a
.Vertex v
represents a single vertex.Component (head, cs)
is a component of the wto, that is a sequence of elements between two parentheses.head
is the head of the component, that is the first element, which is guaranteed to be a vertex by definition.cs
is the rest of the component.
and 'a t
The type of a sequence of outermost elements in a weak topological ordering. This is also the type of a weak topological ordering over a set of
'a
.
val fold_left : ('a -> 'b element -> 'a) -> 'a -> 'b t -> 'a
Folding over the elements of a weak topological ordering. They are given to the accumulating function according to their order.
Note that as
element
s present in an ordering of typet
can contain values of typet
itself due to theComponent
variant, this function should be used by defining a recursive functionf
, which will callfold_left
withf
used to define the first parameter.