From b60722bc58a7acfb882b101acb87aa56bf3453a3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Oct 2003 13:50:15 +0000
Subject: [PATCH] * src/tgbaalgos/emptinesscheck.hh
 (connected_component::not_null, connected_component::transition_acc,
 connected_component::nb_transition, connected_component::nb_state): Remove
 these unused attributes. (connected_component::connected_component): Merge
 the two definitions into one. (connected_component::~connected_component):
 Remove. (connected_component::isAccepted): Delete, unused. *
 src/tgbaalgos/emptinesscheck.cc (connected_component::connected_component,
 connected_component::~connected_component): Adjust.
 (connected_component::isAccepted): Delete. (spot):

* src/tgbatest/emptchk.test: Typo.
---
 ChangeLog                       | 16 ++++++++++++++++
 src/tgbaalgos/emptinesscheck.cc | 34 ++++-----------------------------
 src/tgbaalgos/emptinesscheck.hh |  9 +--------
 src/tgbatest/emptchk.test       |  4 ++--
 4 files changed, 23 insertions(+), 40 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index e85dea570..2e98df7ce 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,21 @@
 2003-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/emptinesscheck.hh (connected_component::not_null,
+	connected_component::transition_acc,
+	connected_component::nb_transition,
+	connected_component::nb_state): Remove these unused attributes.
+	(connected_component::connected_component): Merge the two
+	definitions into one.
+	(connected_component::~connected_component): Remove.
+	(connected_component::isAccepted): Delete, unused.
+	* src/tgbaalgos/emptinesscheck.cc
+	(connected_component::connected_component,
+	connected_component::~connected_component): Adjust.
+	(connected_component::isAccepted): Delete.
+	(spot):
+
+	* src/tgbatest/emptchk.test: Typo.
+
 	* src/tgbaalgos/emptinesscheck.hh
 	(emptiness_check::remove_component, emptiness_check::root_component,
 	emptiness_check::seen_state_num, emptiness_check::suffix): Move in
diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc
index 6d6e111b3..f4bd1d274 100644
--- a/src/tgbaalgos/emptinesscheck.cc
+++ b/src/tgbaalgos/emptinesscheck.cc
@@ -8,13 +8,11 @@
 #include "bdd.h"
 #include <map>
 #include <list>
-#include <sstream>
 #include <stack>
 #include <queue>
 #include <stdio.h>
 #include <vector>
 #include <set>
-#include <iterator>
 #include <utility>
 #include <ostream>
 
@@ -23,34 +21,10 @@ namespace spot
   typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
   typedef std::pair<pair_state_iter, bdd> triplet;
 
-  connected_component::connected_component()
-  {
-    index = 0;
-    condition = bddfalse;
-    transition_acc = -1;
-    nb_transition = 0;
-    nb_state = 1;
-    not_null = false;
-  }
-
-  connected_component::connected_component(int i, bdd a)
+  connected_component::connected_component(int i)
   {
     index = i;
-    condition = a;
-    transition_acc = -1;
-    nb_transition = 0;
-    nb_state = 1;
-    not_null = false;
-  }
-
-  connected_component::~connected_component()
-  {
-  }
-
-  bool
-  connected_component::isAccepted(tgba* aut)
-  {
-    return aut->all_accepting_conditions() == condition;
+    condition = bddfalse;
   }
 
   /// \brief Remove all the nodes accessible from the given node start_delete.
@@ -98,7 +72,7 @@ namespace spot
     int nbstate = 1;
     state* init = aut_check->get_init_state();
     seen_state_num[init] = 1;
-    root_component.push(spot::connected_component(1,bddfalse));
+    root_component.push(spot::connected_component(1));
     arc_accepting.push(bddfalse);
     tgba_succ_iterator* iter_ = aut_check->succ_iter(init);
     iter_->first();
@@ -143,7 +117,7 @@ namespace spot
 		nbstate = nbstate + 1;
 		assert(nbstate != 0);
 		seen_state_num[current_state] = nbstate;
-		root_component.push(connected_component(nbstate, bddfalse));
+		root_component.push(connected_component(nbstate));
 		arc_accepting.push(current_accepting);
 		tgba_succ_iterator* iter2 = aut_check->succ_iter(current_state);
 		iter2->first();
diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh
index eafe09dcf..3ce9caf35 100644
--- a/src/tgbaalgos/emptinesscheck.hh
+++ b/src/tgbaalgos/emptinesscheck.hh
@@ -20,10 +20,7 @@ namespace spot
   {
     // During the Depth path we keep the connected component that we met.
   public:
-    connected_component();
-    connected_component(int i, bdd a);
-    virtual ~connected_component();
-    bool isAccepted(tgba* aut);
+    connected_component(int index = -1);
 
   public:
     int index;
@@ -36,10 +33,6 @@ namespace spot
     /// for the counter example we need to know all the states of the
     /// component
     set_of_state state_set;
-    int transition_acc;
-    int nb_transition;
-    int nb_state;
-    bool not_null;
   };
 
   class emptiness_check
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 9b48ca44e..2ccf54a1f 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -38,5 +38,5 @@ expect_no '!((FF a) <=> (F a))'
 expect_no 'Xa && (!a U b) && !b && X!b'
 expect_no '(a U !b) && Gb'
 
-# Expect four counter-examples..
-test `./ltl2tgba -n 'FFx <=> Fx' | grep Prefix: | wc -l` = 4
+# Expect five counter-examples..
+test `./ltl2tgba -n 'FFx <=> Fx' | grep Prefix: | wc -l` = 5