minimize_wdba() failed to fully minimize some automata.

* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
algorithm to use colors.  The previous implementation was an
incorrect approximation.
* src/tgbatest/wdba2.test: New file showing two equivalent
formulas that were minimized in automata with different sizes.
* src/tgbatest/Makefile.am: Add it.

ChangeLog

@@ -1,3 +1,14 @@
+2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	minimize_wdba() failed to fully minimize some automata.
+
+	* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
+	algorithm to use colors.  The previous implementation was an
+	incorrect approximation.
+	* src/tgbatest/wdba2.test: New file showing two equivalent
+	formulas that were minimized in automata with different sizes.
+	* src/tgbatest/Makefile.am: Add it.
+
 2012-01-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* NEWS: Update with recent fixes.

NEWS

@@ -3,6 +3,8 @@ New in spot 0.8.1a:
   * Bug fixes:
     - spot::ltl::length() forgot to count the '&' and '|' operators
       in an LTL formula.
+    - minimize_wdba() could fail to mark some transiant SCCs as accepting,
+      producing an automaton that was not fully minimized.
     - minimize_dfa() could produce incorrect automata, but it's not
       clear whether this could have had an inpact on WDBA minimization
       (the worse case is that some TGBA would not have been minimized

src/tgbaalgos/minimize.cc

@@ -531,83 +531,84 @@ namespace spot
       power_map pm;
       det_a = tgba_powerset(a, pm);
 
-      // For each SCC of the deterministic automaton, determine if
-      // it is accepting or not.
+      // For each SCC of the deterministic automaton, determine if it
+      // is accepting or not.
+
+      // 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.
+
+      // We also keep track of whether an SCC is useless
+      // (i.e., it is not the start of any accepting word).
+
       scc_map sm(det_a);
       sm.build_map();
       unsigned scc_count = sm.scc_count();
-      // SCC that have been marked as accepting.
-      std::vector<bool> accepting(scc_count);
       // SCC that have been marked as useless.
       std::vector<bool> useless(scc_count);
+      // The "color".  Even number correspond to
+      // accepting SCCs.
+      std::vector<unsigned> d(scc_count);
+
+      // An even number larger than scc_count.
+      unsigned k = (scc_count | 1) + 1;
+
       // SCC are numbered in topological order
-      for (unsigned n = 0; n < scc_count; ++n)
+      // (but in the reverse order as Löding's)
+      for (unsigned m = 0; m < scc_count; ++m)
 	{
-	  bool acc = true;
 	  bool is_useless = true;
+	  bool transient = sm.trivial(m);
+	  const scc_map::succ_type& succ = sm.succ(m);
 
-	  if (sm.trivial(n))
+	  if (transient && succ.empty())
 	    {
-	      const scc_map::succ_type& succ = sm.succ(n);
-	      if (succ.empty())
-		{
-		  // A trivial SCC without successor is useless.
-		  useless[n] = true;
-		  accepting[n] = false;
-		  // Do not add even add it to final or non_final.
-		  continue;
-		}
-	      // Trivial SCCs are accepting if all their
-	      // useful successors are accepting.
+	      // A trivial SCC without successor is useless.
+	      useless[m] = true;
+	      d[m] = k - 1;
+	      continue;
+	    }
 
-	      // 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.
+	  // Compute the minimum color l of the successors.
+	  // Also SCCs are useless if all their successor are
+	  // useless.
+	  unsigned l = k;
+	  for (scc_map::succ_type::const_iterator j = succ.begin();
+	       j != succ.end(); ++j)
+	    {
+	      is_useless &= useless[j->first];
+	      unsigned dj = d[j->first];
+	      if (dj < l)
+		l = dj;
+	    }
 
-	      // Also they are useless if all their successor are
-	      // useless.
-	      for (scc_map::succ_type::const_iterator i = succ.begin();
-		   i != succ.end(); ++i)
-		{
-		  if (!useless[i->first])
-		    {
-		      is_useless = false;
-		      acc &= accepting[i->first];
-		    }
-		}
+	  if (transient)
+	    {
+	      d[m] = l;
 	    }
 	  else
 	    {
 	      // Regular SCCs are accepting if any of their loop
 	      // corresponds to an accepted word in the original
 	      // automaton.
-	      acc = wdba_scc_is_accepting(det_a, n, a, sm, pm);
-
-	      if (acc)
+	      if (wdba_scc_is_accepting(det_a, m, a, sm, pm))
 		{
 		  is_useless = false;
+		  d[m] = (l | 1) - 1; // largest even number inferior or equal
 		}
 	      else
 		{
-		  // Unaccepting SCCs are useless if their successors
-		  // are all useless.
-		  const scc_map::succ_type& succ = sm.succ(n);
-		  for (scc_map::succ_type::const_iterator i = succ.begin();
-		       i != succ.end(); ++i)
-		    is_useless &= useless[i->first];
+		  d[m] = (l - 1) | 1; // largest odd number inferior or equal
 		}
 	    }
 
-	  useless[n] = is_useless;
-	  accepting[n] = acc;
+	  useless[m] = is_useless;
 
 	  if (!is_useless)
 	    {
-	      hash_set* dest_set = acc ? final : non_final;
-	      const std::list<const state*>& l = sm.states_of(n);
+	      hash_set* dest_set = (d[m]&1) ? non_final : final;
+	      const std::list<const state*>& l = sm.states_of(m);
 	      std::list<const state*>::const_iterator il;
 	      for (il = l.begin(); il != l.end(); ++il)
 		dest_set->insert((*il)->clone());

src/tgbatest/Makefile.am

@@ -1,5 +1,5 @@
-## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-## de l'Epita (LRDE).
+## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
@@ -100,6 +100,7 @@ TESTS = \
   sccsimpl.test \
   obligation.test \
   wdba.test \
+  wdba2.test \
   babiak.test \
   randtgba.test \
   emptchk.test \

src/tgbatest/wdba2.test

@@ -0,0 +1,38 @@
+#!/bin/sh
+# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot 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 of the License, or
+# (at your option) any later version.
+#
+# Spot 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+. ./defs
+
+set -e
+
+cat >expected <<EOF
+sub trans.: 16
+transitions: 8
+states: 4
+EOF
+
+# These two equivalent formulae used to produce
+# minimized automata of different sizes...
+run 0 ../ltl2tgba -Rm -kt 'a | X(Gd|Fa)' > out
+run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2
+
+cmp out expected
+cmp out2 expected