(* Strongly connected components.
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "scc_h";
open "rel_h";

fun scc (G : ''_node digraph, root : ''_node) =
    let val dfsr = ref ({} : ''_node -m> int) (* dfsnum *)
	val lowr = ref ({} : ''_node -m> int) (* low *)
	val nr = ref 0
	val sp = ref nil
	val cl = ref nil
	val cls = ref ({} : ''_node set)
	val scc_list = ref ({} : int -m> ''_node set)
	fun scc_explore v =
	    (inc nr;
	     dfsr := !dfsr ++ {v => !nr};
	     lowr := !lowr ++ {v => !nr};
	     cl := v :: !cl;
	     cls := !cls U {v};
	     iterate
	       if w inset low
		   then if w inset !cls
			    then let val low_w = ?low w
				     val low_v = ?low v
				 in
				     if low_w < low_v
					 then lowr := !lowr ++ {v => low_w}
				     else ()
				 end
			else ()
	       else (scc_explore w;
		     let val low = !lowr
			 val low_v = ?low v
			 val low_w = ?low w
		     in
			 if low_w < low_v
			     then lowr := low ++ {v => low_w}
			 else ()
		     end)
	     | w in set if v inset G then ?G v else {}
	       val low = !lowr
	     end;
	     let val low = !lowr
		 val low_v = ?low v
	     in
		 if low_v = ?(!dfsr) v
		     then let val finished = ref false
			      val sc_v = {let val w::rest = !cl
					  in
					      if w=v
						  then finished := true
					      else ();
						  cl := rest;
						  w
					  end
					 |while not (!finished)}
			  in
			      cls := !cls \ sc_v;
			      scc_list := !scc_list ++ {low_v => sc_v}
			  end
		 else ()
	     end)
	    (* It is sometimes claimed that when (dfsnum_v, low_v) = ?info v,
	     then low_v is the minimum of all dfsnums of nodes reachable from
	     v.  This is wrong.
	     For example, consider the graph:
	     a <=> b <=> c
	     where <=> means -> and <-.
	     Start from a.  Then a gets dfsnum=1, low=1.
	     Continue on b: b gets dfsnum=2, low=2.
	     From b, go to c: c gets dfsnum=3, low=3.
	     The stack cl is now [c, b, a].
	     Now, from c, the only successor is b, which is on the stack.
	     So put c's low value to 2 (min with that of b).
	     We are done with c's descendants.  Since c has different
	     dfsnum (=3) and low (=2), there is nothing else to do with c.
	     We get back to b.  We have already explored c, now go to a,
	     which is on the stack.
	     So put b's low value to 1 (min with that of a).
	     The point here is that although b's low value has been
	     lowered to 1, c's low value is still at 2!
	     We are done with b's descendants.  Since b has different
	     dfsnum (=2) and low (=1), there is nothing else to do with b.
	     We get back to a, which has no other descendants.
	     However, a has the same dfsnum and low (=1), so
	     we pop the stack until and including a, yielding
	     the only scc, {a,b,c}.
	     However, a and b have low=1, while c has low=2.

	     Therefore we decide not to return the low values.
	     *)
    in
	scc_explore root; (!dfsr, !scc_list)
    end;

(*
 Test:
val G = { 1 => {2, 4},
	  2 => {3, 4, 5},
	  3 => {2},
	  4 => {},
	  5 => {1, 6},
	  6 => {7},
	  7 => {8},
	  8 => {6},
	  9 => {2, 3, 11},
	  10 => {6, 9},
	  11 => {7, 10}}; 
 *)

fun scc_condense (G, root, scc) =
    let val lowmap = overwrite [{P => low
				| P in set preds}
			       | low => preds in map scc]
    in
	({low => union {{?lowmap Q
			| Q in set if P inset G then ?G P \ cc else {}}
		       | P in set cc}
	 | low => cc in map scc},
	   ?lowmap root)
    end;

