diff --git a/NEWS b/NEWS
index a2db78662..019cac11e 100644
--- a/NEWS
+++ b/NEWS
@@ -64,6 +64,12 @@ New in spot 1.99.4a (not yet released)
     print_tgba_run -> operator<<
     tgba_run_to_tgba -> twa_run::as_twa
     format_parse_aut_errors -> parsed_aut::format_errors
+    twa_succ_iterator::current_state -> twa_succ_iterator::dst
+    twa_succ_iterator::current_condition -> twa_succ_iterator::cond
+    twa_succ_iterator::current_acceptance_conditions -> twa_succ_iterator::acc
+    ta_succ_iterator::current_state -> ta_succ_iterator::dst
+    ta_succ_iterator::current_condition -> ta_succ_iterator::cond
+    ta_succ_iterator::current_acceptance_conditions -> ta_succ_iterator::acc
 
   Python:
 
diff --git a/iface/ltsmin/ltsmin.cc b/iface/ltsmin/ltsmin.cc
index 063848dbf..ea3fb918a 100644
--- a/iface/ltsmin/ltsmin.cc
+++ b/iface/ltsmin/ltsmin.cc
@@ -289,7 +289,7 @@ namespace spot
       }
 
       virtual
-      state* current_state() const
+      state* dst() const
       {
 	return (*it_)->clone();
       }
diff --git a/src/kripke/fairkripke.cc b/src/kripke/fairkripke.cc
index 87209eb01..3e5148e5a 100644
--- a/src/kripke/fairkripke.cc
+++ b/src/kripke/fairkripke.cc
@@ -33,7 +33,7 @@ namespace spot
   }
 
   bdd
-  fair_kripke_succ_iterator::current_condition() const
+  fair_kripke_succ_iterator::cond() const
   {
     // Do not assert(!done()) here.  It is OK to call
     // this function on a state without successor.
@@ -41,7 +41,7 @@ namespace spot
   }
 
   acc_cond::mark_t
-  fair_kripke_succ_iterator::current_acceptance_conditions() const
+  fair_kripke_succ_iterator::acc() const
   {
     // Do not assert(!done()) here.  It is OK to call
     // this function on a state without successor.
diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh
index 6a648a74b..ed69c06d1 100644
--- a/src/kripke/fairkripke.hh
+++ b/src/kripke/fairkripke.hh
@@ -39,23 +39,23 @@ namespace spot
   ///   - fair_kripke_succ_iterator::first()
   ///   - fair_kripke_succ_iterator::next()
   ///   - fair_kripke_succ_iterator::done()
-  ///   - fair_kripke_succ_iterator::current_state()
+  ///   - fair_kripke_succ_iterator::dst()
   ///
-  /// This class implements fair_kripke_succ_iterator::current_condition(),
-  /// and fair_kripke_succ_iterator::current_acceptance_conditions().
+  /// This class implements fair_kripke_succ_iterator::cond(),
+  /// and fair_kripke_succ_iterator::acc().
   class SPOT_API fair_kripke_succ_iterator : public twa_succ_iterator
   {
   public:
     /// \brief Constructor
     ///
     /// The \a cond and \a acc_cond arguments will be those returned
-    /// by fair_kripke_succ_iterator::current_condition(),
-    /// and fair_kripke_succ_iterator::current_acceptance_conditions().
+    /// by fair_kripke_succ_iterator::cond(),
+    /// and fair_kripke_succ_iterator::acc().
     fair_kripke_succ_iterator(const bdd& cond, acc_cond::mark_t acc_cond);
     virtual ~fair_kripke_succ_iterator();
 
-    virtual bdd current_condition() const;
-    virtual acc_cond::mark_t current_acceptance_conditions() const;
+    virtual bdd cond() const;
+    virtual acc_cond::mark_t acc() const;
   protected:
     bdd cond_;
     acc_cond::mark_t acc_cond_;
diff --git a/src/kripke/kripke.cc b/src/kripke/kripke.cc
index 810c76d8d..36d69c23a 100644
--- a/src/kripke/kripke.cc
+++ b/src/kripke/kripke.cc
@@ -27,7 +27,7 @@ namespace spot
   }
 
   bdd
-  kripke_succ_iterator::current_condition() const
+  kripke_succ_iterator::cond() const
   {
     // Do not assert(!done()) here.  It is OK to call
     // this function on a state without successor.
@@ -35,7 +35,7 @@ namespace spot
   }
 
   acc_cond::mark_t
-  kripke_succ_iterator::current_acceptance_conditions() const
+  kripke_succ_iterator::acc() const
   {
     // Do not assert(!done()) here.  It is OK to call
     // this function on a state without successor.
diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh
index 47b05e8b3..e363a59fd 100644
--- a/src/kripke/kripke.hh
+++ b/src/kripke/kripke.hh
@@ -36,17 +36,17 @@ namespace spot
   ///   - kripke_succ_iterator::first()
   ///   - kripke_succ_iterator::next()
   ///   - kripke_succ_iterator::done()
-  ///   - kripke_succ_iterator::current_state()
+  ///   - kripke_succ_iterator::dst()
   ///
-  /// This class implements kripke_succ_iterator::current_condition(),
-  /// and kripke_succ_iterator::current_acceptance_conditions().
+  /// This class implements kripke_succ_iterator::cond(),
+  /// and kripke_succ_iterator::acc().
   class SPOT_API kripke_succ_iterator : public twa_succ_iterator
   {
   public:
     /// \brief Constructor
     ///
     /// The \a cond argument will be the one returned
-    /// by kripke_succ_iterator::current_condition().
+    /// by kripke_succ_iterator::cond().
     kripke_succ_iterator(const bdd& cond)
       : cond_(cond)
     {
@@ -59,8 +59,8 @@ namespace spot
 
     virtual ~kripke_succ_iterator();
 
-    virtual bdd current_condition() const;
-    virtual acc_cond::mark_t current_acceptance_conditions() const;
+    virtual bdd cond() const;
+    virtual acc_cond::mark_t acc() const;
   protected:
     bdd cond_;
   };
diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc
index 4075f3cb8..7b726b464 100644
--- a/src/kripke/kripkeexplicit.cc
+++ b/src/kripke/kripkeexplicit.cc
@@ -116,7 +116,7 @@ namespace spot
     return it_ == s_->get_succ().end();
   }
 
-  state_kripke* kripke_explicit_succ_iterator::current_state() const
+  state_kripke* kripke_explicit_succ_iterator::dst() const
   {
     assert(!done());
     return *it_;
diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh
index 3a801d84a..220dee06c 100644
--- a/src/kripke/kripkeexplicit.hh
+++ b/src/kripke/kripkeexplicit.hh
@@ -99,7 +99,7 @@ namespace spot
     virtual bool next();
     virtual bool done() const;
 
-    virtual state_kripke* current_state() const;
+    virtual state_kripke* dst() const;
 
     private:
     const state_kripke* s_;
diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc
index 5243591ab..a069be7d8 100644
--- a/src/kripke/kripkeprint.cc
+++ b/src/kripke/kripkeprint.cc
@@ -52,7 +52,7 @@ namespace spot
 	os_ << "\",";
 	for (si->first(); !si->done(); si->next())
 	  {
-	    state* dest = si->current_state();
+	    state* dest = si->dst();
 	    os_ << " \"";
 	    escape_str(os_, aut_->format_state(dest));
 	    os_ << '"';
diff --git a/src/ta/ta.hh b/src/ta/ta.hh
index 7d4148096..f2b8bdc04 100644
--- a/src/ta/ta.hh
+++ b/src/ta/ta.hh
@@ -206,16 +206,16 @@ namespace spot
     virtual bool done() const = 0;
 
     virtual state*
-    current_state() const = 0;
+    dst() const = 0;
 
     /// \brief Get the changeset on the transition leading to current successor.
     ///
     /// This is a boolean function of atomic propositions.
     virtual bdd
-    current_condition() const = 0;
+    cond() const = 0;
 
     acc_cond::mark_t
-    current_acceptance_conditions() const = 0;
+    acc() const = 0;
 
   };
 
diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc
index e5c6d5e9c..d70194145 100644
--- a/src/ta/taexplicit.cc
+++ b/src/ta/taexplicit.cc
@@ -72,28 +72,28 @@ namespace spot
   }
 
   state*
-  ta_explicit_succ_iterator::current_state() const
+  ta_explicit_succ_iterator::dst() const
   {
     trace
-      << "***ta_explicit_succ_iterator::current_state()  if(done()) =***"
+      << "***ta_explicit_succ_iterator::dst()  if(done()) =***"
           << done() << std::endl;
     assert(!done());
     trace
-      << "***ta_explicit_succ_iterator::current_state() (*i_)->condition =***"
+      << "***ta_explicit_succ_iterator::dst() (*i_)->condition =***"
           << (*i_)->condition << std::endl;
     state_ta_explicit* s = (*i_)->dest;
     return s;
   }
 
   bdd
-  ta_explicit_succ_iterator::current_condition() const
+  ta_explicit_succ_iterator::cond() const
   {
     assert(!done());
     return (*i_)->condition;
   }
 
   acc_cond::mark_t
-  ta_explicit_succ_iterator::current_acceptance_conditions() const
+  ta_explicit_succ_iterator::acc() const
   {
     assert(!done());
     return (*i_)->acceptance_conditions;
diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh
index 7e71579f0..98cb0d6b6 100644
--- a/src/ta/taexplicit.hh
+++ b/src/ta/taexplicit.hh
@@ -239,12 +239,12 @@ namespace spot
     virtual bool done() const;
 
     virtual state*
-    current_state() const;
+    dst() const;
     virtual bdd
-    current_condition() const;
+    cond() const;
 
     virtual acc_cond::mark_t
-    current_acceptance_conditions() const;
+    acc() const;
 
   private:
     state_ta_explicit::transitions* transitions_;
diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc
index f99aa74ee..60e90b0a9 100644
--- a/src/ta/taproduct.cc
+++ b/src/ta/taproduct.cc
@@ -130,7 +130,7 @@ namespace spot
         return;
       }
 
-    kripke_current_dest_state = kripke_succ_it_->current_state();
+    kripke_current_dest_state = kripke_succ_it_->dst();
     bdd kripke_current_dest_condition = kripke_->state_condition(
         kripke_current_dest_state);
     is_stuttering_transition_ = (kripke_source_condition
@@ -196,10 +196,10 @@ namespace spot
 
         if (!ta_succ_it_->done())
           {
-            current_state_ = new state_ta_product(ta_succ_it_->current_state(),
+            current_state_ = new state_ta_product(ta_succ_it_->dst(),
                 kripke_current_dest_state->clone());
             current_acceptance_conditions_
-                = ta_succ_it_->current_acceptance_conditions();
+                = ta_succ_it_->acc();
             return true;
           }
 
@@ -215,7 +215,7 @@ namespace spot
   }
 
   state_ta_product*
-  ta_succ_iterator_product::current_state() const
+  ta_succ_iterator_product::dst() const
   {
     return current_state_->clone();
   }
@@ -227,13 +227,13 @@ namespace spot
   }
 
   bdd
-  ta_succ_iterator_product::current_condition() const
+  ta_succ_iterator_product::cond() const
   {
     return current_condition_;
   }
 
   acc_cond::mark_t
-  ta_succ_iterator_product::current_acceptance_conditions() const
+  ta_succ_iterator_product::acc() const
   {
     return current_acceptance_conditions_;
   }
@@ -281,7 +281,7 @@ namespace spot
             artificial_initial_state, kripke_init_state_condition);
         for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next())
           {
-            ta_init_states_set.insert(ta_init_it_->current_state());
+            ta_init_states_set.insert(ta_init_it_->dst());
           }
         delete ta_init_it_;
 
@@ -444,7 +444,7 @@ namespace spot
         return;
       }
 
-    kripke_current_dest_state = kripke_succ_it_->current_state();
+    kripke_current_dest_state = kripke_succ_it_->dst();
     bdd kripke_current_dest_condition = kripke_->state_condition(
         kripke_current_dest_state);
 
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index 3c3ca7a61..96ab85219 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -88,12 +88,12 @@ namespace spot
 
     // inspection
     state_ta_product*
-    current_state() const;
+    dst() const;
     bdd
-    current_condition() const;
+    cond() const;
 
     acc_cond::mark_t
-    current_acceptance_conditions() const;
+    acc() const;
 
     /// \brief Return true if the changeset of the current transition is empty
     bool
diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc
index 09a699561..16bfca601 100644
--- a/src/ta/tgtaproduct.cc
+++ b/src/ta/tgtaproduct.cc
@@ -162,7 +162,7 @@ namespace spot
         return;
       }
 
-    kripke_current_dest_state = kripke_succ_it_->current_state();
+    kripke_current_dest_state = kripke_succ_it_->dst();
     bdd kripke_current_dest_condition = kripke_->state_condition(
         kripke_current_dest_state);
 
@@ -205,9 +205,9 @@ namespace spot
           {
             current_state_ = new (pool_->allocate()) state_product(
                 kripke_current_dest_state->clone(),
-                tgta_succ_it_->current_state(), pool_);
+                tgta_succ_it_->dst(), pool_);
             current_acceptance_conditions_
-	      = tgta_succ_it_->current_acceptance_conditions();
+	      = tgta_succ_it_->acc();
             return true;
           }
 
@@ -231,21 +231,21 @@ namespace spot
   }
 
   state_product*
-  tgta_succ_iterator_product::current_state() const
+  tgta_succ_iterator_product::dst() const
   {
     trace
-      << "*** current_state() .... if(done()) = ***" << done() << std::endl;
+      << "*** dst() .... if(done()) = ***" << done() << std::endl;
     return current_state_->clone();
   }
 
   bdd
-  tgta_succ_iterator_product::current_condition() const
+  tgta_succ_iterator_product::cond() const
   {
     return current_condition_;
   }
 
   acc_cond::mark_t
-  tgta_succ_iterator_product::current_acceptance_conditions() const
+  tgta_succ_iterator_product::acc() const
   {
     return current_acceptance_conditions_;
   }
diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh
index ca6ed5a63..182233171 100644
--- a/src/ta/tgtaproduct.hh
+++ b/src/ta/tgtaproduct.hh
@@ -67,12 +67,12 @@ namespace spot
 
     // inspection
     state_product*
-    current_state() const;
+    dst() const;
     bdd
-    current_condition() const;
+    cond() const;
 
     acc_cond::mark_t
-    current_acceptance_conditions() const;
+    acc() const;
 
   private:
     //@{
diff --git a/src/taalgos/dot.cc b/src/taalgos/dot.cc
index a17f829fa..ed5bc8124 100644
--- a/src/taalgos/dot.cc
+++ b/src/taalgos/dot.cc
@@ -203,8 +203,8 @@ namespace spot
 	bdd_dict_ptr d = t_automata_->get_dict();
 	std::string label =
 	  ((in == 1 && artificial_initial_state_)
-	   ? bdd_format_formula(d, si->current_condition())
-	   : bdd_format_accset(d, si->current_condition()));
+	   ? bdd_format_formula(d, si->cond())
+	   : bdd_format_accset(d, si->cond()));
 
 	if (label.empty())
 	  label = "{}";
@@ -213,7 +213,7 @@ namespace spot
 	  {
 	    label += "\n";
 	    label += t_automata_->acc().
-	      format(si->current_acceptance_conditions());
+	      format(si->acc());
 	  }
 
         os_ << "  " << in << " -> " << out << " [label=\"";
diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc
index 2ce3b2dec..08ba135ac 100644
--- a/src/taalgos/emptinessta.cc
+++ b/src/taalgos/emptinessta.cc
@@ -101,7 +101,7 @@ namespace spot
       {
 
         state_ta_product* init = new state_ta_product(
-            (ta_init_it_->current_state()), kripke_init_state->clone());
+            (ta_init_it_->dst()), kripke_init_state->clone());
 
         if (!h.emplace(init, num + 1).second)
 	  {
@@ -188,9 +188,9 @@ namespace spot
             inc_transitions();
             trace << "PASS 1: transition\n";
             // Fetch the values destination state we are interested in...
-            state* dest = succ->current_state();
+            state* dest = succ->dst();
 
-            auto acc_cond = succ->current_acceptance_conditions();
+            auto acc_cond = succ->acc();
 
             bool curr_is_livelock_hole_state_in_ta_component =
                 (a_->is_hole_state_in_ta_component(curr))
@@ -472,7 +472,7 @@ namespace spot
             inc_transitions();
             trace << "PASS 2 : transition\n";
             // Fetch the values destination state we are interested in...
-            state* dest = succ->current_state();
+            state* dest = succ->dst();
 
             bool is_stuttering_transition = succ->is_stuttering_transition();
             // ... and point the iterator to the next successor, for
diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc
index 6c23212cb..c0bdf0d5c 100644
--- a/src/taalgos/minimize.cc
+++ b/src/taalgos/minimize.cc
@@ -138,7 +138,7 @@ namespace spot
 
 	   for (succit->first(); !succit->done(); succit->next())
 	     {
-	       const state* dst = succit->current_state();
+	       const state* dst = succit->dst();
 	       hash_map::const_iterator i = state_num.find(dst);
 
 	       if (i == state_num.end()) // Ignore useless destinations.
@@ -175,8 +175,8 @@ namespace spot
 		 result->add_to_initial_states_set(new_dst);
 
 	       result->create_transition
-		 (ta_src, succit->current_condition(),
-		  succit->current_acceptance_conditions(),
+		 (ta_src, succit->cond(),
+		  succit->acc(),
 		  ta_dst);
 	     }
 	   delete succit;
@@ -390,24 +390,24 @@ namespace spot
 		  trace << "+src: " << src << std::endl;
 		  for (si->first(); !si->done(); si->next())
 		    {
-		      const state* dst = si->current_state();
+		      const state* dst = si->dst();
 		      hash_map::const_iterator i = state_set_map.find(dst);
 
 		      assert(i != state_set_map.end());
 		      auto curacc =
-			mark_to_bdd(si->current_acceptance_conditions());
+			mark_to_bdd(si->acc());
 		      f |= (bdd_ithvar(i->second)
-			    & si->current_condition() & curacc);
+			    & si->cond() & curacc);
 		      trace
 			<< "+f: " << bdd_format_accset(ta_->get_dict(), f)
 			<< "\n      -bdd_ithvar(i->second): "
 			<< bdd_format_accset(ta_->get_dict(),
 					     bdd_ithvar(i->second))
-			<< "\n      -si->current_condition(): "
+			<< "\n      -si->cond(): "
 			<< bdd_format_accset(ta_->get_dict(),
-					     si->current_condition())
+					     si->cond())
 			<< "\n      -current_acceptance_conditions: "
-			<< si->current_acceptance_conditions()
+			<< si->acc()
 		      << std::endl;
 		    }
 		  delete si;
diff --git a/src/taalgos/reachiter.cc b/src/taalgos/reachiter.cc
index da8c625f1..86ecd1056 100644
--- a/src/taalgos/reachiter.cc
+++ b/src/taalgos/reachiter.cc
@@ -84,7 +84,7 @@ namespace spot
         process_state(t, tn);
         for (si->first(); !si->done(); si->next())
           {
-            const state* current = si->current_state();
+            const state* current = si->dst();
             seen_map::const_iterator s = seen.find(current);
             bool ws = want_state(current);
             if (s == seen.end())
diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc
index 5ba49b247..eb629a1eb 100644
--- a/src/taalgos/tgba2ta.cc
+++ b/src/taalgos/tgba2ta.cc
@@ -285,9 +285,9 @@ namespace spot
 		}
 
 	      // Fetch the values destination state we are interested in...
-	      state* dest = succ->current_state();
+	      state* dest = succ->dst();
 
-	      auto acc_cond = succ->current_acceptance_conditions();
+	      auto acc_cond = succ->acc();
 	      // ... and point the iterator to the next successor, for
 	      // the next iteration.
 	      succ->next();
@@ -422,7 +422,7 @@ namespace spot
 	  twa_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
 	  it->first();
 	  if (!it->done())
-	    is_acc = it->current_acceptance_conditions() != 0U;
+	    is_acc = it->acc() != 0U;
 	  delete it;
 	}
 
@@ -453,10 +453,10 @@ namespace spot
 	  for (twa_succ_it->first(); !twa_succ_it->done();
 	       twa_succ_it->next())
 	    {
-	      const state* tgba_state = twa_succ_it->current_state();
-	      bdd tgba_condition = twa_succ_it->current_condition();
+	      const state* tgba_state = twa_succ_it->dst();
+	      bdd tgba_condition = twa_succ_it->cond();
 	      acc_cond::mark_t tgba_acceptance_conditions =
-                twa_succ_it->current_acceptance_conditions();
+                twa_succ_it->acc();
 	      bdd satone_tgba_condition;
 	      while ((satone_tgba_condition =
 		      bdd_satoneset(tgba_condition,
@@ -474,7 +474,7 @@ namespace spot
 		    twa_succ_iterator* it = tgba_->succ_iter(tgba_state);
 		    it->first();
 		    if (!it->done())
-		      is_acc = it->current_acceptance_conditions() != 0U;
+		      is_acc = it->acc() != 0U;
 		    delete it;
 		  }
 
@@ -623,7 +623,7 @@ namespace spot
 	delete initial_states_iter;
 	return tgta;
       }
-    bdd first_state_condition = initial_states_iter->current_condition();
+    bdd first_state_condition = initial_states_iter->cond();
     delete initial_states_iter;
 
     bdd bdd_stutering_transition = bdd_setxor(first_state_condition,
diff --git a/src/twa/taatgba.cc b/src/twa/taatgba.cc
index c951fa62a..c60f2f454 100644
--- a/src/twa/taatgba.cc
+++ b/src/twa/taatgba.cc
@@ -287,21 +287,21 @@ namespace spot
   }
 
   spot::set_state*
-  taa_succ_iterator::current_state() const
+  taa_succ_iterator::dst() const
   {
     assert(!done());
     return new spot::set_state(new taa_tgba::state_set(*(*i_)->dst), true);
   }
 
   bdd
-  taa_succ_iterator::current_condition() const
+  taa_succ_iterator::cond() const
   {
     assert(!done());
     return (*i_)->condition;
   }
 
   acc_cond::mark_t
-  taa_succ_iterator::current_acceptance_conditions() const
+  taa_succ_iterator::acc() const
   {
     assert(!done());
     return acc_.comp((*i_)->acceptance_conditions);
diff --git a/src/twa/taatgba.hh b/src/twa/taatgba.hh
index efd3c7314..6d69a65ba 100644
--- a/src/twa/taatgba.hh
+++ b/src/twa/taatgba.hh
@@ -109,9 +109,9 @@ namespace spot
     virtual bool next();
     virtual bool done() const;
 
-    virtual set_state* current_state() const;
-    virtual bdd current_condition() const;
-    virtual acc_cond::mark_t current_acceptance_conditions() const;
+    virtual set_state* dst() const;
+    virtual bdd cond() const;
+    virtual acc_cond::mark_t acc() const;
 
   private:
     /// Those typedefs are used to generate all possible successors in
diff --git a/src/twa/twa.hh b/src/twa/twa.hh
index f1ceae301..cf1adc5ca 100644
--- a/src/twa/twa.hh
+++ b/src/twa/twa.hh
@@ -385,14 +385,14 @@ namespace spot
     ///
     /// The returned state should be destroyed (see state::destroy)
     /// by the caller after it is no longer used.
-    virtual state* current_state() const = 0;
+    virtual state* dst() const = 0;
     /// \brief Get the condition on the transition leading to this successor.
     ///
     /// This is a boolean function of atomic propositions.
-    virtual bdd current_condition() const = 0;
+    virtual bdd cond() const = 0;
     /// \brief Get the acceptance conditions on the transition leading
     /// to this successor.
-    virtual acc_cond::mark_t current_acceptance_conditions() const = 0;
+    virtual acc_cond::mark_t acc() const = 0;
 
     //@}
   };
@@ -545,7 +545,7 @@ namespace spot
     /// \brief Build an iterable over the successors of \a s.
     ///
     /// This is meant to be used as
-    /// <code>for (auto i: aut->succ(s)) { /* i->current_state() */ }</code>.
+    /// <code>for (auto i: aut->succ(s)) { /* i->dst() */ }</code>.
     succ_iterable
     succ(const state* s) const
     {
diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh
index fb4b3530b..a4d36bf0b 100644
--- a/src/twa/twagraph.hh
+++ b/src/twa/twagraph.hh
@@ -143,20 +143,20 @@ namespace spot
       return !p_;
     }
 
-    virtual twa_graph_state* current_state() const
+    virtual twa_graph_state* dst() const
     {
       assert(!done());
       return const_cast<twa_graph_state*>
 	(&g_->state_data(g_->edge_storage(p_).dst));
     }
 
-    virtual bdd current_condition() const
+    virtual bdd cond() const
     {
       assert(!done());
       return g_->edge_data(p_).cond;
     }
 
-    virtual acc_cond::mark_t current_acceptance_conditions() const
+    virtual acc_cond::mark_t acc() const
     {
       assert(!done());
       return g_->edge_data(p_).acc;
diff --git a/src/twa/twaproduct.cc b/src/twa/twaproduct.cc
index 0ddeb1cdc..983aa6e7b 100644
--- a/src/twa/twaproduct.cc
+++ b/src/twa/twaproduct.cc
@@ -130,10 +130,10 @@ namespace spot
 	return !right_ || right_->done();
       }
 
-      state_product* current_state() const
+      state_product* dst() const
       {
-	return new(pool_->allocate()) state_product(left_->current_state(),
-						    right_->current_state(),
+	return new(pool_->allocate()) state_product(left_->dst(),
+						    right_->dst(),
 						    pool_);
       }
 
@@ -175,8 +175,8 @@ namespace spot
 	assert(!done());
 	do
 	  {
-	    bdd l = left_->current_condition();
-	    bdd r = right_->current_condition();
+	    bdd l = left_->cond();
+	    bdd r = right_->cond();
 	    bdd current_cond = l & r;
 
 	    if (current_cond != bddfalse)
@@ -196,18 +196,18 @@ namespace spot
 	return false;
       }
 
-      bdd current_condition() const
+      bdd cond() const
       {
 	return current_cond_;
       }
 
-      acc_cond::mark_t current_acceptance_conditions() const
+      acc_cond::mark_t acc() const
       {
 	return
 	  prod_->acc().join(prod_->left_acc(),
-			    left_->current_acceptance_conditions(),
+			    left_->acc(),
 			    prod_->right_acc(),
-			    right_->current_acceptance_conditions());
+			    right_->acc());
        }
 
     protected:
@@ -236,11 +236,11 @@ namespace spot
       {
 	// All the transitions of left_ iterator have the
 	// same label, because it is a Kripke structure.
-	bdd l = left_->current_condition();
+	bdd l = left_->cond();
 	assert(!right_->done());
 	do
 	  {
-	    bdd r = right_->current_condition();
+	    bdd r = right_->cond();
 	    bdd current_cond = l & r;
 
 	    if (current_cond != bddfalse)
@@ -263,14 +263,14 @@ namespace spot
 	return false;
       }
 
-      bdd current_condition() const
+      bdd cond() const
       {
 	return current_cond_;
       }
 
-      acc_cond::mark_t current_acceptance_conditions() const
+      acc_cond::mark_t acc() const
       {
-	return right_->current_acceptance_conditions();
+	return right_->acc();
       }
 
     protected:
diff --git a/src/twa/twasafracomplement.cc b/src/twa/twasafracomplement.cc
index a566a8776..43af5c2d4 100644
--- a/src/twa/twasafracomplement.cc
+++ b/src/twa/twasafracomplement.cc
@@ -661,9 +661,9 @@ namespace spot
         safra_tree::tr_cache_t transitions;
 	for (auto iterator: sba_aut->succ(n))
         {
-          bdd condition = iterator->current_condition();
+          bdd condition = iterator->cond();
           typedef std::pair<bdd, const state*> bdd_state;
-          transitions.insert(bdd_state(condition, iterator->current_state()));
+          transitions.insert(bdd_state(condition, iterator->dst()));
           set_atomic_list(atomic_list, condition);
         }
         cache[n] = transitions;
@@ -958,9 +958,9 @@ namespace spot
       virtual bool first();
       virtual bool next();
       virtual bool done() const;
-      virtual state_complement* current_state() const;
-      virtual bdd current_condition() const;
-      virtual acc_cond::mark_t current_acceptance_conditions() const;
+      virtual state_complement* dst() const;
+      virtual bdd cond() const;
+      virtual acc_cond::mark_t acc() const;
     private:
       succ_list_t list_;
       acc_cond::mark_t the_acceptance_cond_;
@@ -988,21 +988,21 @@ namespace spot
     }
 
     state_complement*
-    twa_safra_complement_succ_iterator::current_state() const
+    twa_safra_complement_succ_iterator::dst() const
     {
       assert(!done());
       return new state_complement(*(it_->second));
     }
 
     bdd
-    twa_safra_complement_succ_iterator::current_condition() const
+    twa_safra_complement_succ_iterator::cond() const
     {
       assert(!done());
       return it_->first;
     }
 
     acc_cond::mark_t
-    twa_safra_complement_succ_iterator::current_acceptance_conditions() const
+    twa_safra_complement_succ_iterator::acc() const
     {
       assert(!done());
       return the_acceptance_cond_;
diff --git a/src/twaalgos/bfssteps.cc b/src/twaalgos/bfssteps.cc
index 2248c3494..81e5133b2 100644
--- a/src/twaalgos/bfssteps.cc
+++ b/src/twaalgos/bfssteps.cc
@@ -77,13 +77,13 @@ namespace spot
 	todo.pop_front();
 	for (auto i: a_->succ(src))
 	  {
-	    const state* dest = filter(i->current_state());
+	    const state* dest = filter(i->dst());
 
 	    if (!dest)
 	      continue;
 
-	    bdd cond = i->current_condition();
-	    acc_cond::mark_t acc = i->current_acceptance_conditions();
+	    bdd cond = i->cond();
+	    acc_cond::mark_t acc = i->acc();
 	    twa_run::step s = { src, cond, acc };
 
 	    if (match(s, dest))
diff --git a/src/twaalgos/bfssteps.hh b/src/twaalgos/bfssteps.hh
index c704ee110..66a31e19d 100644
--- a/src/twaalgos/bfssteps.hh
+++ b/src/twaalgos/bfssteps.hh
@@ -55,7 +55,7 @@ namespace spot
     /// bfs_steps does not do handle the memory for the states it
     /// generates, this is the job of filter().  Here \a s is a new
     /// state* that search() has just allocated (using
-    /// twa_succ_iterator::current_state()), and the return of this
+    /// twa_succ_iterator::dst()), and the return of this
     /// function should be a state* that does not need to be freed by
     /// search().
     ///
diff --git a/src/twaalgos/compsusp.cc b/src/twaalgos/compsusp.cc
index 520dc666c..b3985eca2 100644
--- a/src/twaalgos/compsusp.cc
+++ b/src/twaalgos/compsusp.cc
@@ -195,8 +195,8 @@ namespace spot
 
 	  for (auto li: left->succ(ls))
 	    {
-	      state_pair d(li->current_state(), ris);
-	      bdd lc = li->current_condition();
+	      state_pair d(li->dst(), ris);
+	      bdd lc = li->cond();
 
 	      twa_succ_iterator* ri = nullptr;
 	      // Should we reset the right automaton?
@@ -222,15 +222,15 @@ namespace spot
 		  acc_cond::mark_t racc = radd;
 		  if (ri)
 		    {
-		      cond = lc & ri->current_condition();
+		      cond = lc & ri->cond();
 		      // Skip incompatible edges.
 		      if (cond == bddfalse)
 			{
 			  ri->next();
 			  continue;
 			}
-		      d.second = ri->current_state();
-		      racc = ri->current_acceptance_conditions();
+		      d.second = ri->dst();
+		      racc = ri->acc();
 		    }
 
 		  int dest;
@@ -247,7 +247,7 @@ namespace spot
 		    }
 
 		  acc_cond::mark_t a =
-		    res->acc().join(la, li->current_acceptance_conditions(),
+		    res->acc().join(la, li->acc(),
 				    ra, racc);
 		  res->new_edge(src, dest, bdd_exist(cond, v), a);
 
diff --git a/src/twaalgos/copy.cc b/src/twaalgos/copy.cc
index a1f4f1eea..229eec681 100644
--- a/src/twaalgos/copy.cc
+++ b/src/twaalgos/copy.cc
@@ -73,8 +73,8 @@ namespace spot
 		   const twa_succ_iterator* si)
       {
 	out_->new_edge
-	  (in - 1, out - 1, si->current_condition(),
-	   si->current_acceptance_conditions());
+	  (in - 1, out - 1, si->cond(),
+	   si->acc());
       }
 
     protected:
diff --git a/src/twaalgos/emptiness.cc b/src/twaalgos/emptiness.cc
index 8cb28200a..f092c1663 100644
--- a/src/twaalgos/emptiness.cc
+++ b/src/twaalgos/emptiness.cc
@@ -548,11 +548,11 @@ namespace spot
 	if (j->first())
 	  do
 	    {
-	      if (j->current_condition() != label
-		  || j->current_acceptance_conditions() != acc)
+	      if (j->cond() != label
+		  || j->acc() != acc)
 		continue;
 
-	      const state* s2 = j->current_state();
+	      const state* s2 = j->dst();
 	      if (s2->compare(next))
 		{
 		  s2->destroy();
@@ -579,15 +579,15 @@ namespace spot
 		if (j->first())
 		  do
 		    {
-		      const state* s2 = j->current_state();
+		      const state* s2 = j->dst();
 		      os << "  *";
 		      print_annotation(os, aut, j);
 		      os << " label="
 			 << bdd_format_formula(aut->get_dict(),
-					       j->current_condition())
+					       j->cond())
 			 << " and acc="
 			 << (aut->acc().format
-			     (j->current_acceptance_conditions()))
+			     (j->acc()))
 			 << " going to " << aut->format_state(s2) << '\n';
 		      s2->destroy();
 		    }
@@ -717,11 +717,11 @@ namespace spot
 	const state* the_next = nullptr;
 	for (auto j: aut->succ(s))
           {
-            if (j->current_condition() != label
-                || j->current_acceptance_conditions() != acc)
+            if (j->cond() != label
+                || j->acc() != acc)
               continue;
 
-            const state* s2 = j->current_state();
+            const state* s2 = j->dst();
             if (s2->compare(next) == 0)
               {
 		the_next = s2;
diff --git a/src/twaalgos/gtec/gtec.cc b/src/twaalgos/gtec/gtec.cc
index 930d7997c..743356430 100644
--- a/src/twaalgos/gtec/gtec.cc
+++ b/src/twaalgos/gtec/gtec.cc
@@ -108,7 +108,7 @@ namespace spot
 	    {
 	      inc_transitions();
 
-	      state* s = i->current_state();
+	      state* s = i->dst();
 	      auto j = ecs_->h.find(s);
 	      assert(j != ecs_->h.end());
 	      s->destroy();
@@ -215,8 +215,8 @@ namespace spot
 	inc_transitions();
 	// Fetch the values (destination state, acceptance conditions
 	// of the arc) we are interested in...
-	const state* dest = succ->current_state();
-	acc_cond::mark_t acc = succ->current_acceptance_conditions();
+	const state* dest = succ->dst();
+	acc_cond::mark_t acc = succ->acc();
 	// ... and point the iterator to the next successor, for
 	// the next iteration.
 	succ->next();
@@ -319,8 +319,8 @@ namespace spot
   {
     for (auto iter: shy->ecs_->aut->succ(s))
       {
-	q.emplace_back(iter->current_acceptance_conditions(),
-		       iter->current_state());
+	q.emplace_back(iter->acc(),
+		       iter->dst());
 	shy->inc_depth();
 	shy->inc_transitions();
       }
diff --git a/src/twaalgos/gv04.cc b/src/twaalgos/gv04.cc
index 8b568a5f9..14f299897 100644
--- a/src/twaalgos/gv04.cc
+++ b/src/twaalgos/gv04.cc
@@ -120,9 +120,9 @@ namespace spot
 	      }
 	    else
 	      {
-		const state* s_prime = iter->current_state();
+		const state* s_prime = iter->dst();
 		bool acc =
-		  a_->acc().accepting(iter->current_acceptance_conditions());
+		  a_->acc().accepting(iter->acc());
 		inc_transitions();
 
 		trace << " Next successor: s_prime = "
@@ -312,8 +312,8 @@ namespace spot
 	      twa_run::step st =
 		{
 		  data.stack[father].s->clone(),
-		  data.stack[father].lasttr->current_condition(),
-		  data.stack[father].lasttr->current_acceptance_conditions()
+		  data.stack[father].lasttr->cond(),
+		  data.stack[father].lasttr->acc()
 		};
 	      res->prefix.push_front(st);
 	      father = data.stack[father].pre;
diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc
index 8f1f7904e..467c195b5 100644
--- a/src/twaalgos/lbtt.cc
+++ b/src/twaalgos/lbtt.cc
@@ -67,7 +67,7 @@ namespace spot
 	twa_succ_iterator* it = aut_->succ_iter(s);
 	if (!it->first())
 	  return {};
-	auto res = it->current_acceptance_conditions();
+	auto res = it->acc();
 	aut_->release_iter(it);
 	return res;
       }
@@ -98,11 +98,11 @@ namespace spot
 	body_ << out - 1 << ' ';
 	if (!sba_format_)
 	  {
-	    for (auto s: aut_->acc().sets(si->current_acceptance_conditions()))
+	    for (auto s: aut_->acc().sets(si->acc()))
 	      body_ << s << ' ';
 	    body_ << "-1 ";
 	  }
-	print_lbt_ltl(body_, bdd_to_formula(si->current_condition(),
+	print_lbt_ltl(body_, bdd_to_formula(si->cond(),
 					    aut_->get_dict())) << '\n';
       }
 
diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index 6f8872238..d86721677 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -1234,8 +1234,8 @@ namespace spot
 		return res;
 	      for (auto i: aut->succ(st))
 		{
-		  bdd label = i->current_condition();
-		  state* s = i->current_state();
+		  bdd label = i->cond();
+		  state* s = i->dst();
 		  formula dest =
 		    namer->get_name(aut->state_number(s));
 
@@ -1279,8 +1279,8 @@ namespace spot
 
 	      for (auto i: aut->succ(st))
 		{
-		  bdd label = i->current_condition();
-		  state* s = i->current_state();
+		  bdd label = i->cond();
+		  state* s = i->dst();
 		  formula dest = namer->get_name(aut->state_number(s));
 
 		  missing -= label;
diff --git a/src/twaalgos/magic.cc b/src/twaalgos/magic.cc
index 034e2f2e1..931f46a08 100644
--- a/src/twaalgos/magic.cc
+++ b/src/twaalgos/magic.cc
@@ -186,11 +186,11 @@ namespace spot
             trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
@@ -273,11 +273,11 @@ namespace spot
             trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc
index 26adcdc54..dc466697f 100644
--- a/src/twaalgos/minimize.cc
+++ b/src/twaalgos/minimize.cc
@@ -98,7 +98,7 @@ namespace spot
 
 	  for (auto sit: a->succ(src))
 	    {
-	      const state* dst = sit->current_state();
+	      const state* dst = sit->dst();
 	      // Is it a new state ?
 	      if (seen->find(dst) == seen->end())
 		{
@@ -156,13 +156,13 @@ namespace spot
 	  // Connect it to all destinations.
 	  for (auto succit: a->succ(src))
 	    {
-	      const state* dst = succit->current_state();
+	      const state* dst = succit->dst();
 	      hash_map::const_iterator i = state_num.find(dst);
 	      dst->destroy();
 	      if (i == state_num.end()) // Ignore useless destinations.
 		continue;
 	      res->new_acc_edge(src_num, i->second,
-				succit->current_condition(), accepting);
+				succit->cond(), accepting);
 	    }
 	}
       res->merge_edges();
@@ -354,7 +354,7 @@ namespace spot
 		  bdd f = bddfalse;
 		  for (auto si: det_a->succ(src))
 		    {
-		      const state* dst = si->current_state();
+		      const state* dst = si->dst();
 		      hash_map::const_iterator i = state_set_map.find(dst);
 		      dst->destroy();
 		      if (i == state_set_map.end())
@@ -365,7 +365,7 @@ namespace spot
 			// want to ignore some useless states).  Simply
 			// ignore these states here.
 			continue;
-		      f |= (bdd_ithvar(i->second) & si->current_condition());
+		      f |= (bdd_ithvar(i->second) & si->cond());
 		    }
 
 		  // Have we already seen this formula ?
diff --git a/src/twaalgos/ndfs_result.hxx b/src/twaalgos/ndfs_result.hxx
index edaaa72e8..05d1dc954 100644
--- a/src/twaalgos/ndfs_result.hxx
+++ b/src/twaalgos/ndfs_result.hxx
@@ -272,11 +272,11 @@ namespace spot
                       << std::endl;
           if (!f.it->done())
             {
-              const state *s_prime = f.it->current_state();
+              const state *s_prime = f.it->dst();
               ndfsr_trace << "  Visit the successor: "
                           << a_->format_state(s_prime) << std::endl;
-              bdd label = f.it->current_condition();
-	      auto acc = f.it->current_acceptance_conditions();
+              bdd label = f.it->cond();
+	      auto acc = f.it->acc();
               f.it->next();
               if (h_.has_been_visited(s_prime))
                 {
diff --git a/src/twaalgos/reachiter.cc b/src/twaalgos/reachiter.cc
index 00081bc8e..d32d3185d 100644
--- a/src/twaalgos/reachiter.cc
+++ b/src/twaalgos/reachiter.cc
@@ -64,7 +64,7 @@ namespace spot
 	if (si->first())
 	  do
 	    {
-	      const state* current = si->current_state();
+	      const state* current = si->dst();
 	      seen_map::const_iterator s = seen.find(current);
 	      bool ws = want_state(current);
 	      if (s == seen.end())
@@ -202,7 +202,7 @@ namespace spot
 	    continue;
 	  }
 
-	dst = si->current_state();
+	dst = si->dst();
 	auto res = seen.emplace(dst, n);
 	if (!res.second)
 	  {
diff --git a/src/twaalgos/se05.cc b/src/twaalgos/se05.cc
index b90182d3e..265a81dde 100644
--- a/src/twaalgos/se05.cc
+++ b/src/twaalgos/se05.cc
@@ -183,11 +183,11 @@ namespace spot
             trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
@@ -274,11 +274,11 @@ namespace spot
             trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
diff --git a/src/twaalgos/stats.cc b/src/twaalgos/stats.cc
index de09ff0e0..a9ea9bba6 100644
--- a/src/twaalgos/stats.cc
+++ b/src/twaalgos/stats.cc
@@ -72,7 +72,7 @@ namespace spot
       {
 	++s_.edges;
 
-	bdd cond = it->current_condition();
+	bdd cond = it->cond();
 	bdd newvars = bdd_exist(bdd_support(cond), seen_);
 	if (newvars != bddtrue)
 	  {
diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc
index 5631fd282..fa8a2d8fa 100644
--- a/src/twaalgos/stutter.cc
+++ b/src/twaalgos/stutter.cc
@@ -119,7 +119,7 @@ namespace spot
         need_loop_ = true;
         if (it_->first())
           {
-            cond_ = it_->current_condition();
+            cond_ = it_->cond();
             next_edge();
           }
         return true;
@@ -142,7 +142,7 @@ namespace spot
           }
         else
           {
-            cond_ = it_->current_condition();
+            cond_ = it_->cond();
             next_edge();
             return true;
           }
@@ -157,15 +157,15 @@ namespace spot
       // inspection
 
       state_tgbasl*
-      current_state() const
+      dst() const
       {
         if (loop_)
           return new state_tgbasl(state_->real_state(), state_->cond());
-        return new state_tgbasl(it_->current_state(), one_);
+        return new state_tgbasl(it_->dst(), one_);
       }
 
       bdd
-      current_condition() const
+      cond() const
       {
         if (loop_)
           return state_->cond();
@@ -173,11 +173,11 @@ namespace spot
       }
 
       acc_cond::mark_t
-      current_acceptance_conditions() const
+      acc() const
       {
         if (loop_)
           return 0U;
-        return it_->current_acceptance_conditions();
+        return it_->acc();
       }
 
     private:
@@ -187,7 +187,7 @@ namespace spot
         one_ = bdd_satoneset(cond_, aps_, bddtrue);
         cond_ -= one_;
         if (need_loop_ && (state_->cond() == one_)
-            && (state_ == it_->current_state()))
+            && (state_ == it_->dst()))
           need_loop_ = false;
       }
 
diff --git a/src/twaalgos/tau03.cc b/src/twaalgos/tau03.cc
index 8802466a3..31f6399ce 100644
--- a/src/twaalgos/tau03.cc
+++ b/src/twaalgos/tau03.cc
@@ -156,11 +156,11 @@ namespace spot
             trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
@@ -190,12 +190,12 @@ namespace spot
 		for (auto i: a_->succ(f.s))
                   {
                    inc_transitions();
-                   const state *s_prime = i->current_state();
+                   const state *s_prime = i->dst();
                    trace << "DFS_BLUE rescanning the arc from "
                          << a_->format_state(f.s) << "  to "
                          << a_->format_state(s_prime) << std::endl;
-                    bdd label = i->current_condition();
-                    auto acc = i->current_acceptance_conditions();
+                    bdd label = i->cond();
+                    auto acc = i->acc();
                     typename heap::color_ref c_prime = h.get_color_ref(s_prime);
                     assert(!c_prime.is_white());
 		    auto acu = acc | c.get_acc();
@@ -236,11 +236,11 @@ namespace spot
             trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
diff --git a/src/twaalgos/tau03opt.cc b/src/twaalgos/tau03opt.cc
index 2d601859d..17a5bb63f 100644
--- a/src/twaalgos/tau03opt.cc
+++ b/src/twaalgos/tau03opt.cc
@@ -196,11 +196,11 @@ namespace spot
             trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
@@ -315,11 +315,11 @@ namespace spot
             trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
             if (!f.it->done())
               {
-                const state *s_prime = f.it->current_state();
+                const state *s_prime = f.it->dst();
                 trace << "  Visit the successor: "
                       << a_->format_state(s_prime) << std::endl;
-                bdd label = f.it->current_condition();
-                auto acc = f.it->current_acceptance_conditions();
+                bdd label = f.it->cond();
+                auto acc = f.it->acc();
                 // Go down the edge (f.s, <label, acc>, s_prime)
                 f.it->next();
                 inc_transitions();
diff --git a/wrap/python/tests/interdep.py b/wrap/python/tests/interdep.py
index 03a8e3465..4a767ebef 100755
--- a/wrap/python/tests/interdep.py
+++ b/wrap/python/tests/interdep.py
@@ -42,7 +42,7 @@ s0 = a.get_init_state()
 it = a.succ_iter(s0)
 it.first()
 while not it.done():
-    c = it.current_condition()
+    c = it.cond()
     sys.stdout.write("%s\n" % c)
     b &= c # `&=' is defined only in buddy.  So if this statement works
            # it means buddy can grok spot's objects.