Make it easier to debug reference counts in LTL nodes.

* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
Add a dump_instance() static method to all class.
* src/ltltest/readltl.cc: Add option -r to dump all instances
with their reference count, after parsing and after deletion.

ChangeLog

@@ -1,3 +1,14 @@
+2009-11-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Make it easier to debug reference counts in LTL nodes.
+
+	* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
+	src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/multop.cc,
+	src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
+	Add a dump_instance() static method to all class.
+	* src/ltltest/readltl.cc: Add option -r to dump all instances
+	with their reference count, after parsing and after deletion.
+
 2009-11-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Better types for instance maps.

src/ltlast/automatop.cc

@@ -117,5 +117,19 @@ namespace spot
     {
       return instances.size();
     }
+
+    std::ostream&
+    automatop::dump_instances(std::ostream& os)
+    {
+      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
+	{
+	  os << i->second << " = "
+	     << i->second->ref_count_() << " * "
+	     << i->second->dump()
+	     << std::endl;
+	}
+      return os;
+    }
+
   }
 }

src/ltlast/automatop.hh

@@ -24,6 +24,7 @@
 # define SPOT_LTLAST_AUTOMATOP_HH
 
 # include <vector>
+# include <iosfwd>
 # include <map>
 # include "nfa.hh"
 # include "refformula.hh"
@@ -72,6 +73,10 @@ namespace spot
       /// Number of instantiated multop operators.  For debugging.
       static unsigned instance_count();
 
+      /// Dump all instances.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
+
+
     protected:
       typedef std::pair<std::pair<nfa::ptr, bool>, vec*> triplet;
       /// Comparison functor used internally by ltl::automatop.

src/ltlast/binop.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2005, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,6 +23,7 @@
 #include <utility>
 #include "binop.hh"
 #include "visitor.hh"
+#include <iostream>
 
 namespace spot
 {
@@ -149,5 +150,21 @@ namespace spot
     {
       return instances.size();
     }
+
+    std::ostream&
+    binop::dump_instances(std::ostream& os)
+    {
+      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
+	{
+	  os << i->second << " = "
+	     << i->second->ref_count_() << " * "
+	     << i->second->dump()
+	     << std::endl;
+	}
+      return os;
+
+    }
+
+
   }
 }

src/ltlast/binop.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -28,6 +28,7 @@
 # define SPOT_LTLAST_BINOP_HH
 
 #include <map>
+#include <iosfwd>
 #include "refformula.hh"
 
 namespace spot
@@ -70,6 +71,9 @@ namespace spot
       /// Number of instantiated binary operators.  For debugging.
       static unsigned instance_count();
 
+      /// Dump all instances.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
+
     protected:
       typedef std::pair<formula*, formula*> pairf;
       typedef std::pair<type, pairf> pair;

src/ltlast/multop.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2005, 2009 Laboratoire d'Informatique de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -22,6 +22,7 @@
 #include <cassert>
 #include <utility>
 #include <algorithm>
+#include <iostream>
 #include "multop.hh"
 #include "constant.hh"
 #include "visitor.hh"
@@ -208,5 +209,19 @@ namespace spot
     {
       return instances.size();
     }
+
+    std::ostream&
+    multop::dump_instances(std::ostream& os)
+    {
+      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
+	{
+	  os << i->second << " = "
+	     << i->second->ref_count_() << " * "
+	     << i->second->dump()
+	     << std::endl;
+	}
+      return os;
+    }
+
   }
 }

src/ltlast/multop.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -26,6 +26,7 @@
 
 #include <vector>
 #include <map>
+#include <iosfwd>
 #include "refformula.hh"
 
 namespace spot
@@ -95,6 +96,9 @@ namespace spot
       /// Number of instantiated multi-operand operators.  For debugging.
       static unsigned instance_count();
 
+      /// Dump all instances.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
+
     protected:
       typedef std::pair<type, vec*> pair;
       /// Comparison functor used internally by ltl::multop.

src/ltlast/unop.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2005, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -22,6 +22,7 @@
 #include "unop.hh"
 #include "visitor.hh"
 #include <cassert>
+#include <iostream>
 
 namespace spot
 {
@@ -117,5 +118,19 @@ namespace spot
     {
       return instances.size();
     }
+
+    std::ostream&
+    unop::dump_instances(std::ostream& os)
+    {
+      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
+	{
+	  os << i->second << " = "
+	     << i->second->ref_count_() << " * "
+	     << i->second->dump()
+	     << std::endl;
+	}
+      return os;
+    }
+
   }
 }

src/ltlast/unop.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -25,6 +25,7 @@
 # define SPOT_LTLAST_UNOP_HH
 
 #include <map>
+#include <iosfwd>
 #include "refformula.hh"
 
 namespace spot
@@ -59,6 +60,9 @@ namespace spot
       /// Number of instantiated unary operators.  For debugging.
       static unsigned instance_count();
 
+      /// Dump all instances.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
+
     protected:
       typedef std::pair<type, formula*> pair;
       typedef std::map<pair, unop*> map;

src/ltltest/readltl.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6
+// Copyright (C) 2003, 2008, 2009 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
 //
@@ -36,6 +36,16 @@ syntax(char* prog)
   exit(2);
 }
 
+void
+dump_instances(const std::string& label)
+{
+  std::cerr << "=== " << label << " ===" << std::endl;
+  spot::ltl::atomic_prop::dump_instances(std::cerr);
+  spot::ltl::unop::dump_instances(std::cerr);
+  spot::ltl::binop::dump_instances(std::cerr);
+  spot::ltl::multop::dump_instances(std::cerr);
+}
+
 int
 main(int argc, char** argv)
 {
@@ -45,6 +55,7 @@ main(int argc, char** argv)
     syntax(argv[0]);
 
   bool debug = false;
+  bool debug_ref = false;
   int formula_index = 1;
 
   if (!strcmp(argv[1], "-d"))
@@ -54,6 +65,13 @@ main(int argc, char** argv)
 	syntax(argv[0]);
       formula_index = 2;
     }
+  else if (!strcmp(argv[1], "-r"))
+    {
+      debug_ref = true;
+      if (argc < 3)
+	syntax(argv[0]);
+      formula_index = 2;
+    }
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::parse_error_list pel;
@@ -63,8 +81,12 @@ main(int argc, char** argv)
   exit_code =
     spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
 
+
   if (f)
     {
+      if (debug_ref)
+	dump_instances("before");
+
 #ifdef DOTTY
       spot::ltl::dotty(std::cout, f);
 #else
@@ -72,6 +94,9 @@ main(int argc, char** argv)
       std::cout << std::endl;
 #endif
       spot::ltl::destroy(f);
+
+      if (debug_ref)
+	dump_instances("after");
     }
   else
     {