From 314768bf287efcc25fa0c0045b45e11fb14e75f6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Jan 2004 17:08:45 +0000
Subject: [PATCH] * src/ltlast/refformula.hh (ref_formula::ref_count_): New
 method. * src/ltlast/refformula.cc (ref_formula::ref_count_): New method. *
 src/ltlast/atomic_prop.hh (atomic_prop::dump_instance): New method. *
 src/ltlast/atomic_prop.cc (atomic_prop::dump_instance): New method.

---
 ChangeLog                 |  5 +++++
 src/ltlast/atomic_prop.cc | 15 ++++++++++++++-
 src/ltlast/atomic_prop.hh |  5 ++++-
 src/ltlast/refformula.cc  | 16 +++++++++++-----
 src/ltlast/refformula.hh  |  6 ++++--
 5 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 6618bcc99..b46b03f6c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,10 @@
 2004-01-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlast/refformula.hh (ref_formula::ref_count_): New method.
+	* src/ltlast/refformula.cc (ref_formula::ref_count_): New method.
+	* src/ltlast/atomic_prop.hh (atomic_prop::dump_instance): New method.
+	* src/ltlast/atomic_prop.cc (atomic_prop::dump_instance): New method.
+
 	* src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments.
 
 2004-01-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index c0c98f612..61fb0fa06 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -88,5 +88,18 @@ namespace spot
       return instances.size();
     }
 
+    std::ostream&
+    atomic_prop::dump_instances(std::ostream& os)
+    {
+
+      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
+	{
+	  os << i->second << " = " << i->second->ref_count_()
+	     << " * atomic_prop(" << i->first.first << ", "
+	     << i->first.second->name() << ")" << std::endl;
+	}
+      return os;
+    }
+
   }
 }
diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh
index eed808f63..e4d8864cc 100644
--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -23,6 +23,7 @@
 # define SPOT_LTLAST_ATOMIC_PROP_HH
 
 #include <string>
+#include <iostream>
 #include <map>
 #include "refformula.hh"
 #include "ltlenv/environment.hh"
@@ -50,6 +51,8 @@ namespace spot
 
       /// Number of instantiated atomic propositions.  For debugging.
       static unsigned instance_count();
+      /// List all instances of atomic propositions.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
 
     protected:
       atomic_prop(const std::string& name, environment& env);
diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc
index 589969f2d..06ad2dad7 100644
--- a/src/ltlast/refformula.cc
+++ b/src/ltlast/refformula.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -27,7 +27,7 @@ namespace spot
   namespace ltl
   {
     ref_formula::ref_formula()
-      : ref_count_(0)
+      : ref_counter_(0)
     {
     }
 
@@ -38,14 +38,20 @@ namespace spot
     void
     ref_formula::ref_()
     {
-      ++ref_count_;
+      ++ref_counter_;
     }
 
     bool
     ref_formula::unref_()
     {
-      assert(ref_count_ > 0);
-      return !--ref_count_;
+      assert(ref_counter_ > 0);
+      return !--ref_counter_;
+    }
+
+    unsigned
+    ref_formula::ref_count_()
+    {
+      return ref_counter_;
     }
 
   }
diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh
index 789d88325..bd9f7f2a1 100644
--- a/src/ltlast/refformula.hh
+++ b/src/ltlast/refformula.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -37,8 +37,10 @@ namespace spot
       ref_formula();
       void ref_();
       bool unref_();
+      /// Number of references to this formula.
+      unsigned ref_count_();
     private:
-      unsigned ref_count_;
+      unsigned ref_counter_;
     };
 
   }