From d2cf7199bc5506fc014c25ab36bf98d971debc62 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 10 Feb 2006 14:38:35 +0000
Subject: [PATCH] * iface/gspn/ltlgspn.cc (display_stats): New function.
 (main): Use it. * iface/gspn/ssp.cc: Add more counters for statistics.

---
 ChangeLog             |  4 +++
 iface/gspn/ltlgspn.cc | 19 ++++++++++--
 iface/gspn/ssp.cc     | 69 +++++++++++++++++++++++++++++++++++++++----
 3 files changed, 83 insertions(+), 9 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 760f30c2d..4766cfa4b 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,9 @@
 2006-02-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* iface/gspn/ltlgspn.cc (display_stats): New function.
+	(main): Use it.
+	* iface/gspn/ssp.cc: Add more counters for statistics.
+
 	* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state): Correctly
 	update the emptiness statistics.
 
diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc
index 2d96b2325..447571b0b 100644
--- a/iface/gspn/ltlgspn.cc
+++ b/iface/gspn/ltlgspn.cc
@@ -1,6 +1,6 @@
-// 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.
+// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6
+// (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -79,6 +79,16 @@ syntax(char* prog)
   exit(2);
 }
 
+
+void
+display_stats(const spot::unsigned_statistics* s)
+{
+  assert(s);
+  spot::unsigned_statistics::stats_map::const_iterator i;
+  for (i = s->stats.begin(); i != s->stats.end(); ++i)
+    std::cout << i->first << " = " << (s->*i->second)() << std::endl;
+}
+
 int
 main(int argc, char **argv)
   try
@@ -283,6 +293,7 @@ main(int argc, char **argv)
 			spot::print_tgba_run(std::cout, prod, run);
 		      }
 		    ce->print_stats(std::cout);
+		    display_stats(ec);
 		    delete run;
 		    delete ce;
 		  }
@@ -290,6 +301,7 @@ main(int argc, char **argv)
 		  {
 		    std::cout << "non empty" << std::endl;
 		    ecs->print_stats(std::cout);
+		    display_stats(ec);
 		  }
 		delete res;
 	      }
@@ -297,6 +309,7 @@ main(int argc, char **argv)
 	      {
 		std::cout << "empty" << std::endl;
 		ecs->print_stats(std::cout);
+		display_stats(ec);
 	      }
 	    std::cout << std::endl;
 	    delete ec;
diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc
index eb576b512..0bc15d487 100644
--- a/iface/gspn/ssp.cc
+++ b/iface/gspn/ssp.cc
@@ -914,11 +914,33 @@ namespace spot
     couvreur99_check_shy_ssp(const tgba* a)
       : couvreur99_check_shy(a,
 			     option_map(),
-			     numbered_state_heap_ssp_factory_semi::instance())
+			     numbered_state_heap_ssp_factory_semi::instance()),
+	inclusion_count_heap(0),
+	inclusion_count_stack(0)
      {
+       stats["inclusion count heap"] =
+	 static_cast<spot::unsigned_statistics::unsigned_fun>
+	 (&couvreur99_check_shy_ssp::get_inclusion_count_heap);
+       stats["inclusion count stack"] =
+	 static_cast<spot::unsigned_statistics::unsigned_fun>
+	 (&couvreur99_check_shy_ssp::get_inclusion_count_stack);
      }
 
+  private:
+    unsigned inclusion_count_heap;
+    unsigned inclusion_count_stack;
+
   protected:
+    unsigned
+    get_inclusion_count_heap() const
+    {
+      return inclusion_count_heap;
+    };
+    unsigned
+    get_inclusion_count_stack() const
+    {
+      return inclusion_count_stack;
+    };
 
     // If a new state includes an older state, we may have to add new
     // children to the list of children of that older state.  We cannot
@@ -950,12 +972,17 @@ namespace spot
 		  if (i->second == -1)
 		    {
 		      if (spot_inclusion(new_state->left(), old_state->left()))
-			break;
+			{
+			  ++inclusion_count_heap;
+			  break;
+			}
 		    }
 		  else
 		    {
 		      if (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;
@@ -1000,6 +1027,39 @@ namespace spot
   };
 
 
+  // The only purpose of this class is the inclusion_count counter.
+  class couvreur99_check_shy_semi_ssp : public couvreur99_check_shy
+  {
+  public:
+    couvreur99_check_shy_semi_ssp(const tgba* a)
+      : couvreur99_check_shy(a,
+			     option_map(),
+			     numbered_state_heap_ssp_factory_semi::instance()),
+	inclusion_count(0)
+     {
+       stats["inclusion count"] =
+	 static_cast<spot::unsigned_statistics::unsigned_fun>
+	 (&couvreur99_check_shy_semi_ssp::get_inclusion_count);
+     }
+
+  private:
+    unsigned inclusion_count;
+
+  protected:
+    unsigned
+    get_inclusion_count() const
+    {
+      return inclusion_count;
+    };
+
+    virtual numbered_state_heap::state_index_p
+    find_state(const state* s)
+    {
+      ++inclusion_count;
+      return couvreur99_check_shy::find_state(s);
+    }
+  };
+
 
   couvreur99_check*
   couvreur99_check_ssp_semi(const tgba* ssp_automata)
@@ -1016,10 +1076,7 @@ namespace spot
   {
     assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
     return
-      new couvreur99_check_shy
-      (ssp_automata,
-       option_map(),
-       numbered_state_heap_ssp_factory_semi::instance());
+      new couvreur99_check_shy_semi_ssp(ssp_automata);
   }
 
   couvreur99_check*