This is something Soheib and I worked on back in July, but a

intricate memory corruption bug prevented me to check the patch
in.  It took me two days to realize why find_state() must do a
double loop over the candidates to check for equality before
checking for inclusion(s).

* iface/gspn/ltlgspn.cc: New options, -e45 and -n.
* iface/gspn/ssp.cc, iface/gspn/ssp.hh: Handle these.
* src/tgbaalgos/gtec/gtec.cc (TRACE): Add some debugging traces.
(couvreur99_check_shy::dump_queue): New function.
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::dump_queue):
New function.

ChangeLog

@@ -1,3 +1,18 @@
+2008-01-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	This is something Soheib and I worked on back in July, but a
+	intricate memory corruption bug prevented me to check the patch
+	in.  It took me two days to realize why find_state() must do a
+	double loop over the candidates to check for equality before
+	checking for inclusion(s).
+
+	* iface/gspn/ltlgspn.cc: New options, -e45 and -n.
+	* iface/gspn/ssp.cc, iface/gspn/ssp.hh: Handle these.
+	* src/tgbaalgos/gtec/gtec.cc (TRACE): Add some debugging traces.
+	(couvreur99_check_shy::dump_queue): New function.
+	* src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::dump_queue):
+	New function.
+
 2007-11-29  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Keep libtool's files under CVS so that we don't use the broken

iface/gspn/ltlgspn.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de Paris 6
+// Copyright (C) 2003, 2004, 2006, 2007, 2008 Laboratoire
-// (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
-// Université Pierre et Marie Curie.
+// Coopératifs (SRC), Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -73,6 +73,7 @@ syntax(char* prog)
 	    << "  -e4 use semi-d. incl. Couvreur's emptiness-check's "
 	    << "shy variant"
 	    << std::endl
+	    << "  -e45 mix of -e4 and -e5 " << std::endl
 	    << "  -e5 use d. incl. Couvreur's emptiness-check's shy variant"
 	    << std::endl
 	    << "  -e6 like -e5, but without inclusion checks in the "
@@ -80,6 +81,9 @@ syntax(char* prog)
 #endif
 	    << "  -m  degeneralize and perform a magic-search" << std::endl
 	    << std::endl
+#ifdef SSP
+            << "  -n  do not perform any decomposition" << std::endl
+#endif
             << "  -l  use Couvreur's LaCIM algorithm for translation (default)"
 	    << std::endl
             << "  -f  use Couvreur's FM algorithm for translation" << std::endl
@@ -111,6 +115,8 @@ main(int argc, char **argv)
       bool doublehash = true;
       bool stack_inclusion = true;
       bool pushfront = false;
+      bool double_inclusion = false;
+      bool no_decomp = false;
 #endif
       std::string dead = "true";
 
@@ -161,6 +167,11 @@ main(int argc, char **argv)
 	    {
 	      check = Couvreur4;
 	    }
+	  else if (!strcmp(argv[formula_index], "-e45"))
+	    {
+	      check = Couvreur5;
+	      double_inclusion = true;
+	    }
 	  else if (!strcmp(argv[formula_index], "-e5"))
 	    {
 	      check = Couvreur5;
@@ -175,6 +186,12 @@ main(int argc, char **argv)
 	    {
 	      check = Magic;
 	    }
+#ifdef SSP
+	  else if (!strcmp(argv[formula_index], "-n"))
+	    {
+	      no_decomp = true;
+	    }
+#endif
 	  else if (!strcmp(argv[formula_index], "-l"))
 	    {
 	      trans = Lacim;
@@ -276,7 +293,9 @@ main(int argc, char **argv)
 		ec = spot::couvreur99_check_ssp_shy_semi(prod);
 		break;
 	      case Couvreur5:
-		ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion);
+		ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion,
+						    double_inclusion,
+						    no_decomp);
 		break;
 #endif
 	      default:
@@ -389,6 +408,7 @@ main(int argc, char **argv)
 #else
       delete model;
       delete control;
+      delete ca;
 #endif
       delete a_f;
       delete dict;

iface/gspn/ssp.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
+// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire
-// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
-// Université Pierre et Marie Curie.
+// Coopératifs (SRC), Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -240,10 +240,11 @@ namespace spot
     virtual state*
     current_state() const
     {
-      return
+      state_gspn_ssp* s =
 	new state_gspn_ssp(successors_[current_succ_].succ_,
 			   (state_array_[successors_[current_succ_]
 					 .arc->curr_state])->clone());
+      return s;
     }
 
     virtual bdd
@@ -992,13 +993,16 @@ namespace spot
   class couvreur99_check_shy_ssp : public couvreur99_check_shy
   {
   public:
-    couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion)
+    couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion,
+			     bool double_inclusion, bool no_decomp)
       : couvreur99_check_shy(a,
 			     option_map(),
 			     numbered_state_heap_ssp_factory_semi::instance()),
 	inclusion_count_heap(0),
 	inclusion_count_stack(0),
-	stack_inclusion(stack_inclusion)
+	stack_inclusion(stack_inclusion),
+	double_inclusion(double_inclusion),
+	no_decomp(no_decomp)
     {
       onepass_ = true;
 
@@ -1017,6 +1021,8 @@ namespace spot
     unsigned inclusion_count_heap;
     unsigned inclusion_count_stack;
     bool stack_inclusion;
+    bool double_inclusion;
+    bool no_decomp;
 
   protected:
     unsigned
@@ -1063,6 +1069,7 @@ namespace spot
 	      const state_list& l = k->second;
 	      state_list::const_iterator j;
 
+	      // Make a first pass looking for identical states.
 	      for (j = l.begin(); j != l.end(); ++j)
 		{
 		  const state_gspn_ssp* old_state =
@@ -1073,7 +1080,18 @@ namespace spot
 		  assert(new_state);
 
 		  if (old_state->left() == new_state->left())
-		    break;
+		    goto found_match;
+		}
+
+	      // Now, check for inclusions.
+	      for (j = l.begin(); j != l.end(); ++j)
+		{
+		  const state_gspn_ssp* old_state =
+		    dynamic_cast<const state_gspn_ssp*>(*j);
+		  const state_gspn_ssp* new_state =
+		    dynamic_cast<const state_gspn_ssp*>(s);
+		  assert(old_state);
+		  assert(new_state);
 
 		  if (old_state->left() && new_state->left())
 		    {
@@ -1090,42 +1108,83 @@ namespace spot
 			}
 		      else
 			{
+			  if (stack_inclusion
+			      && double_inclusion
+			      && spot_inclusion(new_state->left(),
+						old_state->left()))
+			    break;
 			  if (stack_inclusion
 			      && spot_inclusion(old_state->left(),
 						new_state->left()))
 			    {
 			      ++inclusion_count_stack;
 
-			      State* succ_tgba_ = 0;
-			      size_t size_tgba_ = 0;
 			      succ_queue& queue = todo.back().q;
-
-			      Diff_succ(old_state->left(), new_state->left(),
-					&succ_tgba_, &size_tgba_);
-
 			      succ_queue::iterator old;
 			      if (pos == queue.end())
 				old = queue.begin();
 			      else
-				old = pos;
-
-			      for (size_t i = 0; i < size_tgba_; i++)
 				{
-				  state_gspn_ssp* s =
+				  old = pos;
-				    new state_gspn_ssp
+				  // Should not happen, because onepass_ == 1
-				    (succ_tgba_[i],
+				  assert(0);
-				     old_state->right()->clone());
-				  queue.push_back(successor(old->acc,
-							    s));
-				  inc_depth();
 				}
-			      if (size_tgba_ != 0)
+
-				diff_succ_free(succ_tgba_);
+			      if (no_decomp)
+				{
+				  queue.push_back  // why not push_front?
+				    (successor(old->acc,
+					       old_state->clone()));
+
+				  assert(pos == queue.end());
+
+				  inc_depth();
+
+				  // If we had not done the first loop
+				  // over the container to check for
+				  // equal states, we would have to do
+				  // one here to make sure that state
+				  // s is not equal to another known
+				  // state.  (We risk some intricate
+				  // memory corruption if we don't
+				  // delete "clone states" at this
+				  // point.)
+
+				  // Since we have that first loop and
+				  // we therefore know that state s is
+				  // genuinely new, position j so that
+				  // we won't delete it.
+				  j = l.end();
+				}
+			      else
+				{
+				  State* succ_tgba_ = 0;
+				  size_t size_tgba_ = 0;
+
+				  Diff_succ(old_state->left(),
+					    new_state->left(),
+					    &succ_tgba_, &size_tgba_);
+
+				  for (size_t i = 0; i < size_tgba_; i++)
+				    {
+				      state_gspn_ssp* s =
+					new state_gspn_ssp
+					(succ_tgba_[i],
+					 old_state->right()->clone());
+				      // why not push_front?
+				      queue.push_back(successor(old->acc, s));
+				      inc_depth();
+				    }
+				  if (size_tgba_ != 0)
+				    diff_succ_free(succ_tgba_);
+				}
+
 			      break;
 			    }
 			}
 		    }
 		}
+	    found_match:
 	      if (j != l.end())
 		{
 		  if (s != *j)
@@ -1166,6 +1225,7 @@ namespace spot
 	  res.first = k->first;
 	  res.second = &k->second;
 	}
+
       return res;
     }
   };
@@ -1235,10 +1295,12 @@ namespace spot
   }
 
   couvreur99_check*
-  couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion)
+  couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion,
+			   bool double_inclusion, bool no_decomp)
   {
     assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
-    return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion);
+    return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion,
+					double_inclusion, no_decomp);
   }
 
 #if 0

iface/gspn/ssp.hh

@@ -56,7 +56,9 @@ namespace spot
   couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata);
   couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata);
   couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata,
-					     bool stack_inclusion = true);
+					     bool stack_inclusion = true,
+					     bool double_inclusion = false,
+					     bool no_decomp = false);
 
   /// @}
 

src/tgbaalgos/gtec/gtec.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
 //
@@ -19,6 +19,15 @@
 // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 // 02111-1307, USA.
 
+// #define TRACE
+
+#include <iostream>
+#ifdef TRACE
+#define trace std::cerr
+#else
+#define trace while (0) std::cerr
+#endif
+
 #include "gtec.hh"
 #include "ce.hh"
 #include "misc/memusage.hh"
@@ -374,6 +383,27 @@ namespace spot
     assert(depth() == 0);
   }
 
+  void
+  couvreur99_check_shy::dump_queue(std::ostream& os)
+  {
+    os << "--- TODO ---" << std::endl;
+    unsigned pos = 0;
+    for (todo_list::const_iterator ti = todo.begin(); ti != todo.end(); ++ti)
+      {
+	++pos;
+	os << "#" << pos << " s:" << ti->s << " n:" << ti->n
+	   << " q:{";
+	for (succ_queue::const_iterator qi = ti->q.begin(); qi != ti->q.end();)
+	  {
+	    os << qi->s;
+	    ++qi;
+	    if (qi != ti->q.end())
+	      os << ", ";
+	  }
+	os << "}" << std::endl;;
+      }
+  }
+
   emptiness_check_result*
   couvreur99_check_shy::check()
   {
@@ -382,6 +412,10 @@ namespace spot
 
     for (;;)
       {
+#ifdef TRACE
+	dump_queue();
+#endif
+
 	assert(ecs_->root.size() == 1 + arc.size());
 
 	// Get the successors of the current state.
@@ -390,6 +424,7 @@ namespace spot
 	// If there is no more successor, backtrack.
 	if (queue.empty())
 	  {
+	    trace << "backtrack" << std::endl;
 
 	    // We have explored all successors of state CURR.
 	    const state* curr = todo.back().s;
@@ -451,18 +486,23 @@ namespace spot
 	  old = pos;
 	successor succ = *old;
 	// Beware: the implementation of find_state in ifage/gspn/ssp.cc
-	// uses POS and modify QUEUE.
+	// uses POS and modifies QUEUE.
 	numbered_state_heap::state_index_p sip = find_state(succ.s);
 	if (pos != queue.end())
 	  ++pos;
 	int* i = sip.second;
 
+	trace << "picked state " << succ.s << std::endl;
+
 	if (!i)
 	  {
 	    // It's a new state.
 	    // If we are seeking known states, just skip it.
 	    if (pos != queue.end())
 	      continue;
+
+	    trace << "new state" << std::endl;
+
 	    // Otherwise, number it and stack it so we recurse.
 	    queue.erase(old);
 	    dec_depth();
@@ -480,7 +520,12 @@ namespace spot
 
 	// Skip dead states.
 	if (*i == -1)
-	  continue;
+	  {
+	    trace << "dead state" << std::endl;
+	    continue;
+	  }
+
+	trace << "merging..." << std::endl;
 
 	// Now this is the most interesting case.  We have
 	// reached a state S1 which is already part of a
@@ -542,7 +587,7 @@ namespace spot
 		todo_list::reverse_iterator last = prev++;
 		// If group2 is used we insert the last->q in front
 		// of prev->q so that the states in prev->q are checked
-		// for existence again after we have done with the states
+		// for existence again after we have processed the states
 		// of last->q.  Otherwise we just append to the end.
 		prev->q.splice(group2_ ? prev->q.begin() : prev->q.end(),
 			       last->q);

src/tgbaalgos/gtec/gtec.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
 //
@@ -238,6 +238,9 @@ namespace spot
 
     void clear_todo();
 
+    /// Dump the queue for debugging.
+    void dump_queue(std::ostream& os = std::cerr);
+
     /// Whether successors should be grouped for states in the same SCC.
     bool group_;
     // If the "group2" option is set (it implies "group"), we