WeakTopologicalOrder (infer.IR.WeakTopologicalOrder)

module F = Stdlib.Format

A hierarchical ordering of a set is a well-parenthesized permutation of its elements without two consecutive "(". I defines a total order <= over its elements. The elements between two matching parentheses are called a Component. The first element of a Component is called the head. Let denote by H(v) the set of head of the nested components containing v.

module Partition : sig ... end

module type PreProcCfg = sig ... end

A weak topological ordering (WTO) of a directed graph is a hierarchical ordering of its vertices such that for every edge u -> v,

u < v and v is not in H(u) (forward edge)

v <= u and v is in H(u) (feedback edge)

where H(u) is the set of heads of the nested components containing u.

A WTO of a directed graph is such that the head v of every feedback edge u -> v is the head of a component containing its tail u.

module type S = sig ... end

module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG

module Bourdoncle_SCC : Make

Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly connected components and subcomponents". See Bou Figure 4, page 10.