Module Scc

Module Scc

The file contains an implementation of ``Tarjan's algorithm'' to compute the strongly connected components of a graph. The algorithm is modelled similar to the one of CLR 90.

Graphs are ``doubly-linked'', i.e., each node knows the list of successors (the normal adjacency list) as well as the the predecessors. These are computed ``on-the-fly'', therefore the type dgraph for ``dynamic graph''.
type a dgraph = Graph of ((a ® a list) × (a ® a list))

dfs-collect finds by df-traversal all nodes for which the predicate holds. Additionally it give back the finishing time. The real work is done in the local search procedure.

l is the list of known but not yet finished nodes. Since the algorithm works on-the-fly, it doesn't contain all nodes at the beginning. A node is white, when it has not been treated and checked, grey when it has been checked, and black, when it has been finished. Since we are interested in the order in which the nodes are finished, we keep a separate list where we collect the finished nodes in the required order.
The returned list is ordered with the decreasing finishing times. It assumes that all nodes of the graph can be reached from the intial list.
One application of dfs_visit takes an entry node and calculates the list of reachable states (the black ones) in the reversed order of ``finishing'' times. Nodes listed in old_blacks are ignored.
type a color = White of a | Grey of a

type direction = Forward | Backward

let dfs_visit_f
     (g: a dgraph)
     (d: direction)
     (start: a) (* start node for current descend *)
     (old_blacks: a list list) (* treated at previous dfs-descends *)
     : a list =
   let list_cmem (e: a) (l: a color list) : bool =
     List.exists (fun (e2: a color) ® (Grey e = e2)) l (* white doesn't count! *)
   in match g with Graph (succ, pred) ®
     let f_neighbor = (
       match d with
         Forward ® succ
       | Backward ® pred)
     in
     let rec search
         (l: (a color) list)
         (black: a list)
         : (a list) =
       match l with
         [ ] ® black (* that's it *)
       | (White e):: l' ®
           let nextnodes = (List.map (fun x ® White x) (f_neighbor e))
           in
           if
             (list_cmem e l') or
             (List.mem e black) or
             List.exists (fun (bl: a list) ® (List.mem e bl)) old_blacks
           then search l' black
           else search (nextnodes @ ((Grey e) :: l')) black
       | (Grey e) :: l' ® (search l' (e::black))
     in search [White start] [ ]

The function dfs_visit_iter iterates the previous function, collecting the ``black'' nodes of the recursive descends.

let dfs_visit_iter (g: a dgraph)
     (d: direction)
     (startnodes: a list) (* they are considered a white *)
     : a list list = (* collection of reached nodes *)
   let rec f_iter
       (startnodes: a list)
       (blacks: a list list)
       =
     match startnodes with
       [ ] ® (blacks)
     | i::startnodes' ®
         let new_blacks = dfs_visit_f g d i blacks
         in match new_blacks with
           [ ] ® f_iter startnodes' blacks (* we don't count that *)
         | _ ® f_iter startnodes' (new_blacks :: blacks)
   in (f_iter startnodes [ ])

The ssc gives back the list of ssc's, each a list of nodes. The algorithm works by traversing two times the graph in a depth-first manner, one in forward, and one in backward direction, where the second traversal starts the df-searches in decreasing order of the finishing times of the forward run.
let scc (g: a dgraph) (start: a list) : (a list) list =
   dfs_visit_iter g Backward (List.flatten (dfs_visit_iter g Forward start))

January 31, 2002