From f06fc8ac776ee9f16a2974587921178934c1c3e6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 5 Jan 2011 12:34:37 +0100
Subject: [PATCH] * src/tgbaalgos/minimize.cc (minimize): Use the Loeding
 algorithm to label transient states.

---
 ChangeLog                 |  5 +++++
 src/tgbaalgos/minimize.cc | 39 ++++++++++++++++++++++++++++++++++++---
 2 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 3c26242b5..a0bb0670c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2011-01-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm
+	to label transient states.
+
 2011-01-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Rewrite the check of WDBA state acceptance in minimize().
diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index 737c9df50..27662b702 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -22,6 +22,7 @@
 #include <deque>
 #include <set>
 #include <list>
+#include <vector>
 #include "minimize.hh"
 #include "ltlast/allnodes.hh"
 #include "misc/hash.hh"
@@ -291,12 +292,44 @@ namespace spot
 	  scc_map sm(det_a);
 	  sm.build_map();
 	  unsigned scc_count = sm.scc_count();
+	  std::vector<bool> accepting(scc_count);
+	  // SCC are numbered in topological order
 	  for (unsigned n = 0; n < scc_count; ++n)
 	    {
-	      // Trivial SCCs are not accepting.
+	      bool acc = true;
+
 	      if (sm.trivial(n))
-		continue;
-	      if (wdba_scc_is_accepting(det_a, n, a, sm, pm))
+		{
+		  // Trivial SCCs are accepting if all their
+		  // successors are accepting.
+
+		  // This corresponds to the algorithm in Fig. 1 of
+		  // "Efficient minimization of deterministic weak
+		  // omega-automata" written by Christof Löding and
+		  // published in Information Processing Letters 79
+		  // (2001) pp 105--109.  Except we do not keep track
+		  // of the actual color associated to each SCC.
+
+		  const scc_map::succ_type& succ = sm.succ(n);
+		  for (scc_map::succ_type::const_iterator i = succ.begin();
+		       i != succ.end(); ++i)
+		    {
+		      if (!accepting[i->first])
+			{
+			  acc = false;
+			  break;
+			}
+		    }
+		}
+	      else
+		{
+		  // Regular SCCs are accepting if any of their loop
+		  // corresponds to an accepting
+		  acc = wdba_scc_is_accepting(det_a, n, a, sm, pm);
+		}
+
+	      accepting[n] = acc;
+	      if (acc)
 		{
 		  std::list<const state*> l = sm.states_of(n);
 		  std::list<const state*>::const_iterator il;