diff --git a/ChangeLog b/ChangeLog
index d25da73a5..14031700e 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
 2004-04-21  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document
+	arguments.
+	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
+	New method.
+	(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
+	Use it.
+
 	* wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
 	the new variable dot_bgcolor.
 
diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc
index a9826f590..95f68c054 100644
--- a/src/tgbaalgos/neverclaim.cc
+++ b/src/tgbaalgos/neverclaim.cc
@@ -35,8 +35,10 @@ namespace spot
   class never_claim_bfs : public tgba_reachable_iterator_breadth_first
   {
   public:
-    never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, const ltl::formula* f)
-      : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false)
+    never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os,
+		    const ltl::formula* f)
+      : tgba_reachable_iterator_breadth_first(a),
+	os_(os), f_(f), accept_all_(-1), fi_needed_(false)
     {
     }
 
@@ -68,12 +70,19 @@ namespace spot
       delete init_;
     }
 
+    bool
+    state_is_accepting(const state *s)
+    {
+      return
+	dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s);
+    }
+
     std::string
     get_state_label(const state* s, int n)
     {
       std::string label;
       if (s->compare(init_) == 0)
-        if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s))
+        if (state_is_accepting(s))
           label = "accept_init";
         else
           label = "T0_init";
@@ -83,7 +92,7 @@ namespace spot
           ost << n;
           std::string ns(ost.str());
 
-          if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s))
+          if (state_is_accepting(s))
             {
               tgba_succ_iterator* it = automata_->succ_iter(s);
               it->first();
@@ -92,7 +101,8 @@ namespace spot
               else
                 {
                   state* current = it->current_state();
-                  if (it->current_condition() != bddtrue || s->compare(current) != 0)
+                  if (it->current_condition() != bddtrue
+		      || s->compare(current) != 0)
                     label = "accept_S" + ns;
                   else
                     label = "accept_all";
@@ -125,9 +135,10 @@ namespace spot
       else
         {
           state* current =it->current_state();
-          if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s) &&
-              (it->current_condition() == bddtrue) && s->compare(init_) != 0 &&
-              s->compare(current) == 0)
+          if (state_is_accepting(s)
+	      && it->current_condition() == bddtrue
+	      && s->compare(init_) != 0
+	      && s->compare(current) == 0)
             accept_all_ = n;
           else
             {
@@ -150,7 +161,8 @@ namespace spot
       if (in != accept_all_)
         {
           os_ << "  :: (" ;
-          const ltl::formula* f = bdd_to_formula(si->current_condition(), automata_->get_dict());
+          const ltl::formula* f = bdd_to_formula(si->current_condition(),
+						 automata_->get_dict());
           to_spin_string(f, os_);
           destroy(f);
           state* current = si->current_state();
@@ -168,7 +180,8 @@ namespace spot
   };
 
   std::ostream&
-  never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f)
+  never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g,
+			const ltl::formula* f)
   {
     never_claim_bfs n(g, os, f);
     n.run();
diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh
index 00349e55a..ba672603e 100644
--- a/src/tgbaalgos/neverclaim.hh
+++ b/src/tgbaalgos/neverclaim.hh
@@ -29,7 +29,14 @@
 namespace spot
 {
   /// \brief Print reachable states in Spin never claim format.
-  std::ostream& never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f=0);
+  ///
+  /// \param os The output stream to print on.
+  /// \param g The degeneralized automaton to output.
+  /// \param f The (optional) formula associated to the automaton.  If given
+  ///          it will be output as a comment.
+  std::ostream& never_claim_reachable(std::ostream& os,
+				      const tgba_tba_proxy* g,
+				      const ltl::formula* f = 0);
 }
 
 #endif // SPOT_TGBAALGOS_NEVERCLAIM_HH