bundles/menhirLib/menhir-20120123/src/tarjan.ml

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  Menhir                                                                *)
   4 (*                                                                        *)
   5 (*  François Pottier, INRIA Rocquencourt                                  *)
   6 (*  Yann Régis-Gianas, PPS, Université Paris Diderot                      *)
   7 (*                                                                        *)
   8 (*  Copyright 2005-2008 Institut National de Recherche en Informatique    *)
   9 (*  et en Automatique. All rights reserved. This file is distributed      *)
  10 (*  under the terms of the Q Public License version 1.0, with the change  *)
  11 (*  described in file LICENSE.                                            *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This module provides an implementation of Tarjan's algorithm for
  16    finding the strongly connected components of a graph.
  17
  18    The algorithm runs when the functor is applied. Its complexity is
  19    $O(V+E)$, where $V$ is the number of vertices in the graph $G$, and
  20    $E$ is the number of edges. *)
  21
  22 module Run (G : sig
  23
  24   type node
  25
  26   (* We assume each node has a unique index. Indices must range from
  27      $0$ to $n-1$, where $n$ is the number of nodes in the graph. *)
  28
  29   val n: int
  30   val index: node -> int
  31
  32   (* Iterating over a node's immediate successors. *)
  33
  34   val successors: (node -> unit) -> node -> unit
  35
  36   (* Iterating over all nodes. *)
  37
  38   val iter: (node -> unit) -> unit
  39
  40 end) = struct
  41
  42   (* Define the internal data structure associated with each node. *)
  43
  44   type data = {
  45
  46       (* Each node carries a flag which tells whether it appears
  47          within the SCC stack (which is defined below). *)
  48
  49       mutable stacked: bool;
  50
  51       (* Each node carries a number. Numbers represent the order in
  52          which nodes were discovered. *)
  53
  54       mutable number: int;
  55
  56       (* Each node [x] records the lowest number associated to a node
  57          already detected within [x]'s SCC. *)
  58
  59       mutable low: int;
  60
  61       (* Each node carries a pointer to a representative element of
  62          its SCC. This field is used by the algorithm to store its
  63          results. *)
  64
  65       mutable representative: G.node;
  66
  67       (* Each representative node carries a list of the nodes in
  68          its SCC. This field is used by the algorithm to store its
  69          results. *)
  70
  71       mutable scc: G.node list
  72
  73     }
  74
  75   (* Define a mapping from external nodes to internal ones. Here, we
  76      simply use each node's index as an entry into a global array. *)
  77
  78   let table =
  79
  80     (* Create the array. We initially fill it with [None], of type
  81        [data option], because we have no meaningful initial value of
  82        type [data] at hand. *)
  83
  84     let table = Array.create G.n None in
  85
  86     (* Initialize the array. *)
  87
  88     G.iter (fun x ->
  89       table.(G.index x) <- Some {
  90         stacked = false;
  91         number = 0;
  92         low = 0;
  93         representative = x;
  94         scc = []
  95       }
  96     );
  97
  98     (* Define a function which gives easy access to the array. It maps
  99        each node to its associated piece of internal data. *)
 100
 101     function x ->
 102       match table.(G.index x) with
 103       | Some dx ->
 104           dx
 105       | None ->
 106           assert false (* Indices do not cover the range $0\ldots n$, as expected. *)
 107
 108   (* Create an empty stack, used to record all nodes which belong to
 109      the current SCC. *)
 110
 111   let scc_stack = Stack.create()
 112
 113   (* Initialize a function which allocates numbers for (internal)
 114      nodes. A new number is assigned to each node the first time it is
 115      visited. Numbers returned by this function start at 1 and
 116      increase. Initially, all nodes have number 0, so they are
 117      considered unvisited. *)
 118
 119   let mark =
 120     let counter = ref 0 in
 121     fun dx ->
 122       incr counter;
 123       dx.number <- !counter;
 124       dx.low <- !counter
 125
 126   (* This reference will hold a list of all representative nodes. *)
 127
 128   let representatives =
 129     ref []
 130
 131   (* Look at all nodes of the graph, one after the other. Any
 132      unvisited nodes become roots of the search forest. *)
 133
 134   let () = G.iter (fun root ->
 135     let droot = table root in
 136
 137     if droot.number = 0 then begin
 138
 139       (* This node hasn't been visited yet. Start a depth-first walk
 140          from it. *)
 141
 142       mark droot;
 143       droot.stacked <- true;
 144       Stack.push droot scc_stack;
 145
 146       let rec walk x =
 147         let dx = table x in
 148
 149         G.successors (fun y ->
 150           let dy = table y in
 151
 152           if dy.number = 0 then begin
 153
 154             (* $y$ hasn't been visited yet, so $(x,y)$ is a regular
 155                edge, part of the search forest. *)
 156
 157             mark dy;
 158             dy.stacked <- true;
 159             Stack.push dy scc_stack;
 160
 161             (* Continue walking, depth-first. *)
 162
 163             walk y;
 164             if dy.low < dx.low then
 165               dx.low <- dy.low
 166
 167           end
 168           else if (dy.low < dx.low) & dy.stacked then begin
 169
 170             (* The first condition above indicates that $y$ has been
 171                visited before $x$, so $(x, y)$ is a backwards or
 172                transverse edge. The second condition indicates that
 173                $y$ is inside the same SCC as $x$; indeed, if it
 174                belongs to another SCC, then the latter has already
 175                been identified and moved out of [scc_stack]. *)
 176
 177             if dy.number < dx.low then
 178               dx.low <- dy.number
 179
 180           end
 181
 182         ) x;
 183
 184         (* We are done visiting $x$'s neighbors. *)
 185
 186         if dx.low = dx.number then begin
 187
 188           (* $x$ is the entry point of a SCC. The whole SCC is now
 189              available; move it out of the stack. We pop elements out
 190              of the SCC stack until $x$ itself is found. *)
 191
 192           let rec loop () =
 193             let element = Stack.pop scc_stack in
 194             element.stacked <- false;
 195             dx.scc <- element.representative :: dx.scc;
 196             element.representative <- x;
 197             if element != dx then
 198               loop() in
 199
 200           loop();
 201           representatives := x :: !representatives
 202
 203         end in
 204
 205       walk root
 206
 207     end
 208   )
 209
 210   (* There only remains to make our results accessible to the
 211      outside. *)
 212
 213   let representative x =
 214     (table x).representative
 215
 216   let scc x =
 217     (table x).scc
 218
 219   let iter action =
 220     List.iter (fun x ->
 221       let data = table x in
 222       assert (data.representative == x); (* a sanity check *)
 223       assert (data.scc <> []); (* a sanity check *)
 224       action x data.scc
 225     ) !representatives
 226
 227 end
 228