'([]a && XXXX!a)' was not properly minimized because its

translation contain useless SCCs that where not ignored for
minimization.

* src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless
SCCs before minimization.
* src/tgbatest/ltl2tgba.test: Add a check.

ChangeLog

+2011-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	'([]a && XXXX!a)' was not properly minimized because its
+	translation contain useless SCCs that where not ignored for
+	minimization.
+
+	* src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless
+	SCCs before minimization.
+	* src/tgbatest/ltl2tgba.test: Add a check.
+
 2011-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	The neverclaim output by spin -f '([]a && XXXX!a)' was not

src/tgbaalgos/minimize.cc

@@ -522,14 +522,27 @@ namespace spot
       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);
       // SCC are numbered in topological order
       for (unsigned n = 0; n < scc_count; ++n)
 	{
 	  bool acc = true;
+	  bool is_useless = true;
 
 	  if (sm.trivial(n))
 	    {
+	      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
 	      // successors are accepting.
 
@@ -540,31 +553,48 @@ namespace spot
 	      // (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);
+	      // 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 (!accepting[i->first])
-		    {
-		      acc = false;
-		      break;
-		    }
+		  is_useless &= useless[i->first];
+		  acc &= accepting[i->first];
 		}
 	    }
 	  else
 	    {
 	      // Regular SCCs are accepting if any of their loop
-	      // corresponds to an accepting
+	      // corresponds to an accepted word in the original
+	      // automaton.
 	      acc = wdba_scc_is_accepting(det_a, n, a, sm, pm);
+
+	      if (acc)
+		{
+		  is_useless = false;
+		}
+	      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];
+		}
 	    }
 
+	  useless[n] = is_useless;
 	  accepting[n] = acc;
 
-	  hash_set* dest_set = acc ? final : non_final;
-	  const std::list<const state*>& l = sm.states_of(n);
-	  std::list<const state*>::const_iterator il;
-	  for (il = l.begin(); il != l.end(); ++il)
-	    dest_set->insert((*il)->clone());
+	  if (!is_useless)
+	    {
+	      hash_set* dest_set = acc ? final : non_final;
+	      const std::list<const state*>& l = sm.states_of(n);
+	      std::list<const state*>::const_iterator il;
+	      for (il = l.begin(); il != l.end(); ++il)
+		dest_set->insert((*il)->clone());
+	    }
 	}
     }
 

src/tgbatest/ltl2tgba.test

 #!/bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -92,6 +92,15 @@ grep 'states: 7$' stdout
 # Make sure 'GFa & GFb & GFc & GFd & GFe & GFf'
 # has 7 states and 34 transitions after degeneralization.
 f='GFa & GFb & GFc & GFd & GFe & GFg'
-../ltl2tgba -ks -DS -x -f $opt "$f" > stdout
+../ltl2tgba -ks -DS -x -f "$f" > stdout
 grep 'transitions: 34$' stdout
 grep 'states: 7$' stdout
+
+# Make sure 'Ga & XXXX!a' is minimized to one state.
+f='Ga & XXXX!a'
+../ltl2tgba -ks -f "$f" > stdout
+grep 'transitions: 4$' stdout
+grep 'states: 5$' stdout
+../ltl2tgba -ks -Rm -f "$f" > stdout
+grep 'transitions: 0$' stdout
+grep 'states: 1$' stdout