rename tgba_succ_iterator as twa_succ_iterator

Automatic mass renaming.

* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeprint.cc, src/ta/ta.hh, src/ta/taproduct.hh,
src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/emptinessta.cc, src/taalgos/reachiter.hh,
src/taalgos/tgba2ta.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbamask.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/stats.cc, src/tgbaalgos/stutter.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Rename
tgba_succ_iterator as twa_succ_iterator.

src/dstarparse/dra2ba.cc

@@ -240,7 +240,7 @@ namespace spot
       void
       process_link(const state* sin, int,
 		   const state* sout, int,
-		   const tgba_succ_iterator* si)
+		   const twa_succ_iterator* si)
       {
 	int in = in_->aut->state_number(sin);
 	int out = in_->aut->state_number(sout);

src/dstarparse/nra2nba.cc

@@ -64,7 +64,7 @@ namespace spot
       void
       process_link(const state* sin, int,
 		   const state* sout, int,
-		   const tgba_succ_iterator* si)
+		   const twa_succ_iterator* si)
       {
 	int in = d_->aut->state_number(sin);
 	int out = d_->aut->state_number(sout);

src/kripke/fairkripke.hh

@@ -43,7 +43,7 @@ namespace spot
   ///
   /// This class implements fair_kripke_succ_iterator::current_condition(),
   /// and fair_kripke_succ_iterator::current_acceptance_conditions().
-  class SPOT_API fair_kripke_succ_iterator : public tgba_succ_iterator
+  class SPOT_API fair_kripke_succ_iterator : public twa_succ_iterator
   {
   public:
     /// \brief Constructor

src/kripke/kripke.hh

@@ -40,7 +40,7 @@ namespace spot
   ///
   /// This class implements kripke_succ_iterator::current_condition(),
   /// and kripke_succ_iterator::current_acceptance_conditions().
-  class SPOT_API kripke_succ_iterator : public tgba_succ_iterator
+  class SPOT_API kripke_succ_iterator : public twa_succ_iterator
   {
   public:
     /// \brief Constructor

src/kripke/kripkeprint.cc

@@ -39,7 +39,7 @@ namespace spot
       {
       }
 
-      void process_state(const state* s, int, tgba_succ_iterator* si)
+      void process_state(const state* s, int, twa_succ_iterator* si)
       {
 	const bdd_dict_ptr d = aut_->get_dict();
 	os_ << '"';
@@ -80,7 +80,7 @@ namespace spot
 	lastsuccs.str("");
       }
 
-      void process_state(const state* s, int in_s, tgba_succ_iterator*)
+      void process_state(const state* s, int in_s, twa_succ_iterator*)
       {
 	if (notfirst)
 	  finish_state();
@@ -98,7 +98,7 @@ namespace spot
 
       void
       process_link(const state*, int, const state*, int d,
-		   const tgba_succ_iterator*)
+		   const twa_succ_iterator*)
       {
 	lastsuccs << " S" << d;
       }

src/ta/ta.hh

@@ -193,7 +193,7 @@ namespace spot
   /// transition labels.  Because transitions are never explicitely
   /// encoded, labels (conditions and acceptance conditions) can only
   /// be queried while iterating over the successors.
-  class ta_succ_iterator : public tgba_succ_iterator
+  class ta_succ_iterator : public twa_succ_iterator
   {
   public:
     virtual

src/ta/taproduct.hh

@@ -116,7 +116,7 @@ namespace spot
     const ta* ta_;
     const kripke* kripke_;
     ta_succ_iterator* ta_succ_it_;
-    tgba_succ_iterator* kripke_succ_it_;
+    twa_succ_iterator* kripke_succ_it_;
     state_ta_product* current_state_;
     bdd current_condition_;
     acc_cond::mark_t current_acceptance_conditions_;

src/ta/tgta.hh

@@ -74,7 +74,7 @@ namespace spot
     /// responsability of the caller to \c delete it when no
     /// longer needed.
     ///
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0;
   };
 

src/ta/tgtaexplicit.cc

@@ -42,7 +42,7 @@ namespace spot
     return ta_->get_artificial_initial_state();
   }
 
-  tgba_succ_iterator*
+  twa_succ_iterator*
   tgta_explicit::succ_iter(const spot::state* state) const
   {
     return ta_->succ_iter(state);
@@ -68,7 +68,7 @@ namespace spot
     return ta_->format_state(s);
   }
 
-  spot::tgba_succ_iterator*
+  spot::twa_succ_iterator*
   tgta_explicit::succ_iter_by_changeset(const spot::state* s, bdd chngset) const
   {
     return ta_->succ_iter(s, chngset);

src/ta/tgtaexplicit.hh

@@ -44,7 +44,7 @@ namespace spot
     // tgba interface
     virtual spot::state* get_init_state() const;
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const spot::state* local_state) const;
 
     virtual bdd_dict_ptr
@@ -55,7 +55,7 @@ namespace spot
 
     virtual std::string format_state(const spot::state* s) const;
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter_by_changeset(const spot::state* s, bdd change_set) const;
   protected:
     virtual bdd compute_support_conditions(const spot::state* state) const;

src/ta/tgtaproduct.cc

@@ -57,7 +57,7 @@ namespace spot
         right_->get_init_state(), p);
   }
 
-  tgba_succ_iterator*
+  twa_succ_iterator*
   tgta_product::succ_iter(const state* state) const
   {
     const state_product* s = down_cast<const state_product*> (state);

src/ta/tgtaproduct.hh

@@ -38,7 +38,7 @@ namespace spot
     virtual state*
     get_init_state() const;
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const state* local_state) const;
   };
 
@@ -49,7 +49,7 @@ namespace spot
   }
 
   /// \brief Iterate over the successors of a product computed on the fly.
-  class SPOT_API tgta_succ_iterator_product : public tgba_succ_iterator
+  class SPOT_API tgta_succ_iterator_product : public twa_succ_iterator
   {
   public:
     tgta_succ_iterator_product(const state_product* s,
@@ -91,8 +91,8 @@ namespace spot
     const_tgta_ptr tgta_;
     const_kripke_ptr kripke_;
     fixed_size_pool* pool_;
-    tgba_succ_iterator* tgta_succ_it_;
+    twa_succ_iterator* tgta_succ_it_;
-    tgba_succ_iterator* kripke_succ_it_;
+    twa_succ_iterator* kripke_succ_it_;
     state_product* current_state_;
     bdd current_condition_;
     acc_cond::mark_t current_acceptance_conditions_;

src/taalgos/emptinessta.cc

@@ -392,7 +392,7 @@ namespace spot
     int num = 0;
 
     // * todo: the depth-first search stack.  This holds pairs of the
-    //   form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
+    //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
     //   over the successors of STATE.  In our use, ITERATOR should
     //   always be freed when TODO is popped, but STATE should not because
     //   it is also used as a key in H.

src/taalgos/reachiter.hh

@@ -79,7 +79,7 @@ namespace spot
     ///
     /// \param in The source state number.
     /// \param out The destination state number.
-    /// \param si The spot::tgba_succ_iterator positionned on the current
+    /// \param si The spot::twa_succ_iterator positionned on the current
     ///             transition.
     virtual void
     process_link(int in, int out, const ta_succ_iterator* si);

src/taalgos/tgba2ta.cc

@@ -45,7 +45,7 @@ namespace spot
 
   namespace
   {
-    typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
+    typedef std::pair<spot::state*, twa_succ_iterator*> pair_state_iter;
 
     static void
     transform_to_single_pass_automaton
@@ -171,7 +171,7 @@ namespace spot
       int num = 0;
 
       // * todo: the depth-first search stack.  This holds pairs of the
-      //   form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
+      //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
       //   over the successors of STATE.  In our use, ITERATOR should
       //   always be freed when TODO is popped, but STATE should not because
       //   it is also used as a key in H.
@@ -202,7 +202,7 @@ namespace spot
 	    arc.push(0U);
 	    sscc.top().is_accepting
               = testing_aut->is_accepting_state(init);
-	    tgba_succ_iterator* iter = testing_aut->succ_iter(init);
+	    twa_succ_iterator* iter = testing_aut->succ_iter(init);
 	    iter->first();
 	    todo.emplace(init, iter);
 	  }
@@ -220,7 +220,7 @@ namespace spot
 		}
 
 	      // We are looking at the next successor in SUCC.
-	      tgba_succ_iterator* succ = todo.top().second;
+	      twa_succ_iterator* succ = todo.top().second;
 
 	      // If there is no more successor, backtrack.
 	      if (succ->done())
@@ -322,7 +322,7 @@ namespace spot
 		  sscc.top().is_accepting =
 		    testing_aut->is_accepting_state(dest);
 
-		  tgba_succ_iterator* iter = testing_aut->succ_iter(dest);
+		  twa_succ_iterator* iter = testing_aut->succ_iter(dest);
 		  iter->first();
 		  todo.emplace(dest, iter);
 		  continue;
@@ -425,7 +425,7 @@ namespace spot
       bool is_acc = false;
       if (degeneralized)
 	{
-	  tgba_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
+	  twa_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
 	  it->first();
 	  if (!it->done())
 	    is_acc = it->current_acceptance_conditions() != 0U;
@@ -454,7 +454,7 @@ namespace spot
 	  state_ta_explicit* source = todo.top();
 	  todo.pop();
 
-	  tgba_succ_iterator* tgba_succ_it =
+	  twa_succ_iterator* tgba_succ_it =
 	    tgba_->succ_iter(source->get_tgba_state());
 	  for (tgba_succ_it->first(); !tgba_succ_it->done();
 	       tgba_succ_it->next())
@@ -477,7 +477,7 @@ namespace spot
 		  bool is_acc = false;
 		  if (degeneralized)
 		  {
-		    tgba_succ_iterator* it = tgba_->succ_iter(tgba_state);
+		    twa_succ_iterator* it = tgba_->succ_iter(tgba_state);
 		    it->first();
 		    if (!it->done())
 		      is_acc = it->current_acceptance_conditions() != 0U;
@@ -621,7 +621,7 @@ namespace spot
     // adapt a ta automata to build tgta automata :
     ta::states_set_t states_set = ta->get_states_set();
     ta::states_set_t::iterator it;
-    tgba_succ_iterator* initial_states_iter =
+    twa_succ_iterator* initial_states_iter =
       ta->succ_iter(ta->get_artificial_initial_state());
     initial_states_iter->first();
     if (initial_states_iter->done())

src/tgba/taatgba.cc

@@ -60,7 +60,7 @@ namespace spot
     return new spot::set_state(init_);
   }
 
-  tgba_succ_iterator*
+  twa_succ_iterator*
   taa_tgba::succ_iter(const spot::state* state) const
   {
     const spot::set_state* s = down_cast<const spot::set_state*>(state);

src/tgba/taatgba.hh

@@ -55,7 +55,7 @@ namespace spot
     /// TGBA interface.
     virtual ~taa_tgba();
     virtual spot::state* get_init_state() const final;
-    virtual tgba_succ_iterator* succ_iter(const spot::state* state) const final;
+    virtual twa_succ_iterator* succ_iter(const spot::state* state) const final;
     virtual std::string format_state(const spot::state* state) const = 0;
 
   protected:
@@ -101,7 +101,7 @@ namespace spot
     bool delete_me_;
   };
 
-  class SPOT_API taa_succ_iterator final: public tgba_succ_iterator
+  class SPOT_API taa_succ_iterator final: public twa_succ_iterator
   {
   public:
     taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);

src/tgba/tgba.cc

@@ -68,7 +68,7 @@ namespace spot
   }
 
   std::string
-  twa::transition_annotation(const tgba_succ_iterator*) const
+  twa::transition_annotation(const twa_succ_iterator*) const
   {
     return "";
   }

src/tgba/tgba.hh

@@ -78,7 +78,7 @@ namespace spot
 
     /// \brief Release a state.
     ///
-    /// Methods from the tgba or tgba_succ_iterator always return a
+    /// Methods from the tgba or twa_succ_iterator always return a
     /// new state that you should deallocate with this function.
     /// Before Spot 0.7, you had to "delete" your state directly.
     /// Starting with Spot 0.7, you should update your code to use
@@ -326,11 +326,11 @@ namespace spot
   /// transition labels.  Because transitions are never explicitely
   /// encoded, labels (conditions and acceptance conditions) can only
   /// be queried while iterating over the successors.
-  class SPOT_API tgba_succ_iterator
+  class SPOT_API twa_succ_iterator
   {
   public:
     virtual
-    ~tgba_succ_iterator()
+    ~twa_succ_iterator()
     {
     }
 
@@ -400,10 +400,10 @@ namespace spot
     struct SPOT_API succ_iterator
     {
     protected:
-      tgba_succ_iterator* it_;
+      twa_succ_iterator* it_;
     public:
 
-      succ_iterator(tgba_succ_iterator* it):
+      succ_iterator(twa_succ_iterator* it):
 	it_(it)
       {
       }
@@ -418,7 +418,7 @@ namespace spot
 	return it_ != o.it_;
       }
 
-      const tgba_succ_iterator* operator*() const
+      const twa_succ_iterator* operator*() const
       {
 	return it_;
       }
@@ -482,7 +482,7 @@ namespace spot
   protected:
     twa(const bdd_dict_ptr& d);
     // Any iterator returned via release_iter.
-    mutable tgba_succ_iterator* iter_cache_;
+    mutable twa_succ_iterator* iter_cache_;
     bdd_dict_ptr dict_;
   public:
 
@@ -491,9 +491,9 @@ namespace spot
     {
     protected:
       const twa* aut_;
-      tgba_succ_iterator* it_;
+      twa_succ_iterator* it_;
     public:
-      succ_iterable(const twa* aut, tgba_succ_iterator* it)
+      succ_iterable(const twa* aut, twa_succ_iterator* it)
 	: aut_(aut), it_(it)
       {
       }
@@ -536,7 +536,7 @@ namespace spot
     /// The iterator has been allocated with \c new.  It is the
     /// responsability of the caller to \c delete it when no
     /// longer needed.
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const state* local_state) const = 0;
 
 #ifndef SWIG
@@ -555,7 +555,7 @@ namespace spot
     ///
     /// This iterator can then be reused by succ_iter() to avoid
     /// memory allocation.
-    void release_iter(tgba_succ_iterator* i) const
+    void release_iter(twa_succ_iterator* i) const
     {
       if (iter_cache_)
 	delete i;
@@ -611,9 +611,9 @@ namespace spot
     /// This method is used for instance in dotty_reachable(),
     /// and replay_tgba_run().
     ///
-    /// \param t a non-done tgba_succ_iterator for this automaton
+    /// \param t a non-done twa_succ_iterator for this automaton
     virtual std::string
-    transition_annotation(const tgba_succ_iterator* t) const;
+    transition_annotation(const twa_succ_iterator* t) const;
 
     /// \brief Project a state on an automaton.
     ///

src/tgba/tgbagraph.hh

@@ -106,7 +106,7 @@ namespace spot
 
   template<class Graph>
   class SPOT_API twa_graph_succ_iterator final:
-    public tgba_succ_iterator
+    public twa_succ_iterator
   {
   private:
     typedef typename Graph::transition transition;
@@ -268,7 +268,7 @@ namespace spot
       return const_cast<tgba_graph_state*>(state_from_number(init_number_));
     }
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const state* st) const
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
@@ -312,7 +312,7 @@ namespace spot
       return format_state(state_number(st));
     }
 
-    tgba_graph_trans_data& trans_data(const tgba_succ_iterator* it)
+    tgba_graph_trans_data& trans_data(const twa_succ_iterator* it)
     {
       auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
       return g_.trans_data(i->pos());
@@ -323,7 +323,7 @@ namespace spot
       return g_.trans_data(t);
     }
 
-    const tgba_graph_trans_data& trans_data(const tgba_succ_iterator* it) const
+    const tgba_graph_trans_data& trans_data(const twa_succ_iterator* it) const
     {
       auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
       return g_.trans_data(i->pos());
@@ -334,7 +334,7 @@ namespace spot
       return g_.trans_data(t);
     }
 
-    trans_storage_t& trans_storage(const tgba_succ_iterator* it)
+    trans_storage_t& trans_storage(const twa_succ_iterator* it)
     {
       auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
       return g_.trans_storage(i->pos());
@@ -346,7 +346,7 @@ namespace spot
     }
 
     const trans_storage_t
-      trans_storage(const tgba_succ_iterator* it) const
+      trans_storage(const twa_succ_iterator* it) const
     {
       auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
       return g_.trans_storage(i->pos());

src/tgba/tgbamask.cc

@@ -32,7 +32,7 @@ namespace spot
     };
     typedef std::vector<transition> transitions;
 
-    struct succ_iter_filtered: public tgba_succ_iterator
+    struct succ_iter_filtered: public twa_succ_iterator
     {
       ~succ_iter_filtered()
       {
@@ -111,7 +111,7 @@ namespace spot
 	return init_->clone();
       }
 
-      virtual tgba_succ_iterator*
+      virtual twa_succ_iterator*
       succ_iter(const state* local_state) const
       {
 	succ_iter_filtered* res;

src/tgba/tgbaproduct.cc

@@ -74,24 +74,24 @@ namespace spot
   }
 
   ////////////////////////////////////////////////////////////
-  // tgba_succ_iterator_product
+  // twa_succ_iterator_product
 
   namespace
   {
 
-    class tgba_succ_iterator_product_common: public tgba_succ_iterator
+    class twa_succ_iterator_product_common: public twa_succ_iterator
     {
     public:
-      tgba_succ_iterator_product_common(tgba_succ_iterator* left,
+      twa_succ_iterator_product_common(twa_succ_iterator* left,
-					tgba_succ_iterator* right,
+					twa_succ_iterator* right,
 					const twa_product* prod,
 					fixed_size_pool* pool)
 	: left_(left), right_(right), prod_(prod), pool_(pool)
       {
       }
 
-      void recycle(const const_tgba_ptr& l, tgba_succ_iterator* left,
+      void recycle(const const_tgba_ptr& l, twa_succ_iterator* left,
-		   const_tgba_ptr r, tgba_succ_iterator* right)
+		   const_tgba_ptr r, twa_succ_iterator* right)
       {
 	l->release_iter(left_);
 	left_ = left;
@@ -99,7 +99,7 @@ namespace spot
 	right_ = right;
       }
 
-      virtual ~tgba_succ_iterator_product_common()
+      virtual ~twa_succ_iterator_product_common()
       {
 	delete left_;
 	delete right_;
@@ -138,8 +138,8 @@ namespace spot
       }
 
     protected:
-      tgba_succ_iterator* left_;
+      twa_succ_iterator* left_;
-      tgba_succ_iterator* right_;
+      twa_succ_iterator* right_;
       const twa_product* prod_;
       fixed_size_pool* pool_;
       friend class spot::twa_product;
@@ -147,18 +147,18 @@ namespace spot
 
 
     /// \brief Iterate over the successors of a product computed on the fly.
-    class tgba_succ_iterator_product: public tgba_succ_iterator_product_common
+    class twa_succ_iterator_product: public twa_succ_iterator_product_common
     {
     public:
-      tgba_succ_iterator_product(tgba_succ_iterator* left,
+      twa_succ_iterator_product(twa_succ_iterator* left,
-				 tgba_succ_iterator* right,
+				 twa_succ_iterator* right,
 				 const twa_product* prod,
 				 fixed_size_pool* pool)
-	: tgba_succ_iterator_product_common(left, right, prod, pool)
+	: twa_succ_iterator_product_common(left, right, prod, pool)
       {
       }
 
-      virtual ~tgba_succ_iterator_product()
+      virtual ~twa_succ_iterator_product()
       {
       }
 
@@ -216,19 +216,19 @@ namespace spot
 
     /// Iterate over the successors of a product computed on the fly.
     /// This one assumes that LEFT is an iterator over a Kripke structure
-    class tgba_succ_iterator_product_kripke:
+    class twa_succ_iterator_product_kripke:
-      public tgba_succ_iterator_product_common
+      public twa_succ_iterator_product_common
     {
     public:
-      tgba_succ_iterator_product_kripke(tgba_succ_iterator* left,
+      twa_succ_iterator_product_kripke(twa_succ_iterator* left,
-					tgba_succ_iterator* right,
+					twa_succ_iterator* right,
 					const twa_product* prod,
 					fixed_size_pool* pool)
-	: tgba_succ_iterator_product_common(left, right, prod, pool)
+	: twa_succ_iterator_product_common(left, right, prod, pool)
       {
       }
 
-      virtual ~tgba_succ_iterator_product_kripke()
+      virtual ~twa_succ_iterator_product_kripke()
       {
       }
 
@@ -338,18 +338,18 @@ namespace spot
 					    right_->get_init_state(), p);
   }
 
-  tgba_succ_iterator*
+  twa_succ_iterator*
   twa_product::succ_iter(const state* state) const
   {
     const state_product* s = down_cast<const state_product*>(state);
     assert(s);
-    tgba_succ_iterator* li = left_->succ_iter(s->left());
+    twa_succ_iterator* li = left_->succ_iter(s->left());
-    tgba_succ_iterator* ri = right_->succ_iter(s->right());
+    twa_succ_iterator* ri = right_->succ_iter(s->right());
 
     if (iter_cache_)
       {
-	tgba_succ_iterator_product_common* it =
+	twa_succ_iterator_product_common* it =
-	  down_cast<tgba_succ_iterator_product_common*>(iter_cache_);
+	  down_cast<twa_succ_iterator_product_common*>(iter_cache_);
 	it->recycle(left_, li, right_, ri);
 	iter_cache_ = nullptr;
 	return it;
@@ -357,9 +357,9 @@ namespace spot
 
     fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_);
     if (left_kripke_)
-      return new tgba_succ_iterator_product_kripke(li, ri, this, p);
+      return new twa_succ_iterator_product_kripke(li, ri, this, p);
     else
-      return new tgba_succ_iterator_product(li, ri, this, p);
+      return new twa_succ_iterator_product(li, ri, this, p);
   }
 
   bdd
@@ -406,10 +406,10 @@ namespace spot
   }
 
   std::string
-  twa_product::transition_annotation(const tgba_succ_iterator* t) const
+  twa_product::transition_annotation(const twa_succ_iterator* t) const
   {
-    const tgba_succ_iterator_product_common* i =
+    const twa_succ_iterator_product_common* i =
-      down_cast<const tgba_succ_iterator_product_common*>(t);
+      down_cast<const twa_succ_iterator_product_common*>(t);
     assert(i);
     std::string left = left_->transition_annotation(i->left_);
     std::string right = right_->transition_annotation(i->right_);

src/tgba/tgbaproduct.hh

@@ -90,13 +90,13 @@ namespace spot
 
     virtual state* get_init_state() const;
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const state* state) const;
 
     virtual std::string format_state(const state* state) const;
 
     virtual std::string
-    transition_annotation(const tgba_succ_iterator* t) const;
+    transition_annotation(const twa_succ_iterator* t) const;
 
     virtual state* project_state(const state* s, const const_tgba_ptr& t) const;
 

src/tgba/tgbaproxy.cc

@@ -38,7 +38,7 @@ namespace spot
     return original_->get_init_state();
   }
 
-  tgba_succ_iterator*
+  twa_succ_iterator*
   tgba_proxy::succ_iter(const state* state) const
   {
     if (iter_cache_)
@@ -56,7 +56,7 @@ namespace spot
   }
 
   std::string
-  tgba_proxy::transition_annotation(const tgba_succ_iterator* t) const
+  tgba_proxy::transition_annotation(const twa_succ_iterator* t) const
   {
     return original_->transition_annotation(t);
   }

src/tgba/tgbaproxy.hh

@@ -42,13 +42,13 @@ namespace spot
 
     virtual state* get_init_state() const;
 
-    virtual tgba_succ_iterator*
+    virtual twa_succ_iterator*
     succ_iter(const state* state) const;
 
     virtual std::string format_state(const state* state) const;
 
     virtual std::string
-    transition_annotation(const tgba_succ_iterator* t) const;
+    transition_annotation(const twa_succ_iterator* t) const;
 
     virtual state* project_state(const state* s, const const_tgba_ptr& t) const;
 

src/tgba/tgbasafracomplement.cc

@@ -955,7 +955,7 @@ namespace spot
 
     /// Successor iterators used by spot::tgba_safra_complement.
     /// \ingroup tgba_representation
-    class tgba_safra_complement_succ_iterator: public tgba_succ_iterator
+    class tgba_safra_complement_succ_iterator: public twa_succ_iterator
     {
     public:
       typedef std::multimap<bdd, state_complement*, bdd_less_than> succ_list_t;
@@ -1141,7 +1141,7 @@ namespace spot
   ///   series        = {Lecture Notes in Computer Science},
   ///   publisher     = {Springer-Verlag}
   /// }
-  tgba_succ_iterator*
+  twa_succ_iterator*
   tgba_safra_complement::succ_iter(const state* state) const
   {
     const safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);

src/tgba/tgbasafracomplement.hh

@@ -54,7 +54,7 @@ namespace spot
 
     // tgba interface.
     virtual state* get_init_state() const;
-    virtual tgba_succ_iterator* succ_iter(const state* state) const;
+    virtual twa_succ_iterator* succ_iter(const state* state) const;
 
     virtual std::string format_state(const state* state) const;
 

src/tgbaalgos/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
-    /// tgba_succ_iterator::current_state()), and the return of this
+    /// twa_succ_iterator::current_state()), and the return of this
     /// function should be a state* that does not need to be freed by
     /// search().
     ///

src/tgbaalgos/compsusp.cc

@@ -254,7 +254,7 @@ namespace spot
 	      state_pair d(li->current_state(), ris);
 	      bdd lc = li->current_condition();
 
-	      tgba_succ_iterator* ri = 0;
+	      twa_succ_iterator* ri = 0;
 	      // Should we reset the right automaton?
 	      if ((lc & v) == lc)
 		{

src/tgbaalgos/dupexp.cc

@@ -51,7 +51,7 @@ namespace spot
       }
 
       virtual void
-      process_state(const state*, int n, tgba_succ_iterator*)
+      process_state(const state*, int n, twa_succ_iterator*)
       {
 	unsigned ns = out_->new_state();
 	assert(ns == static_cast<unsigned>(n) - 1);
@@ -62,7 +62,7 @@ namespace spot
       virtual void
       process_link(const state*, int in,
 		   const state*, int out,
-		   const tgba_succ_iterator* si)
+		   const twa_succ_iterator* si)
       {
 	out_->new_transition
 	  (in - 1, out - 1, si->current_condition(),

src/tgbaalgos/gtec/gtec.cc

@@ -37,7 +37,7 @@ namespace spot
 {
   namespace
   {
-    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
+    typedef std::pair<const spot::state*, twa_succ_iterator*> pair_state_iter;
   }
 
   couvreur99_check::couvreur99_check(const const_tgba_ptr& a, option_map o)
@@ -91,14 +91,14 @@ namespace spot
     // Remove from H all states which are reachable from state FROM.
 
     // Stack of iterators towards states to remove.
-    std::stack<tgba_succ_iterator*> to_remove;
+    std::stack<twa_succ_iterator*> to_remove;
 
     // Remove FROM itself, and prepare to remove its successors.
     // (FROM should be in H, otherwise it means all reachable
     // states from FROM have already been removed and there is no
     // point in calling remove_component.)
     ecs_->h[from] = -1;
-    tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
+    twa_succ_iterator* i = ecs_->aut->succ_iter(from);
 
     for (;;)
       {
@@ -150,7 +150,7 @@ namespace spot
     //   visited node,
     int num = 1;
     // * todo, the depth-first search stack.  This holds pairs of the
-    //   form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
+    //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
     //   over the successors of STATE.  In our use, ITERATOR should
     //   always be freed when TODO is popped, but STATE should not because
     //   it is also used as a key in H.
@@ -162,7 +162,7 @@ namespace spot
       ecs_->h[init] = 1;
       ecs_->root.push(1);
       arc.push(0U);
-      tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
+      twa_succ_iterator* iter = ecs_->aut->succ_iter(init);
       iter->first();
       todo.emplace(init, iter);
       inc_depth();
@@ -173,7 +173,7 @@ namespace spot
 	assert(ecs_->root.size() == arc.size());
 
 	// We are looking at the next successor in SUCC.
-	tgba_succ_iterator* succ = todo.top().second;
+	twa_succ_iterator* succ = todo.top().second;
 
 	// If there is no more successor, backtrack.
 	if (succ->done())
@@ -230,7 +230,7 @@ namespace spot
 	    // successors for later processing.
 	    ecs_->root.push(++num);
 	    arc.push(acc);
-	    tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
+	    twa_succ_iterator* iter = ecs_->aut->succ_iter(dest);
 	    iter->first();
 	    todo.emplace(dest, iter);
 	    inc_depth();

src/tgbaalgos/gtec/gtec.hh

@@ -102,14 +102,14 @@ namespace spot
   /// the depth first search is directed.
   ///
   /// spot::couvreur99_check performs a straightforward depth first search.
-  /// The DFS stacks store tgba_succ_iterators, so that only the
+  /// The DFS stacks store twa_succ_iterators, so that only the
   /// iterators which really are explored are computed.
   ///
   /// spot::couvreur99_check_shy tries to explore successors which are
   /// visited states first.  this helps to merge SCCs and generally
   /// helps to produce shorter counter-examples.  However this
   /// algorithm cannot stores unprocessed successors as
-  /// tgba_succ_iterators: it must compute all successors of a state
+  /// twa_succ_iterators: it must compute all successors of a state
   /// at once in order to decide which to explore first, and must keep
   /// a list of all unexplored successors in its DFS stack.
   ///

src/tgbaalgos/gv04.cc

@@ -46,7 +46,7 @@ namespace spot
     struct stack_entry
     {
       const state* s;		  // State stored in stack entry.
-      tgba_succ_iterator* lasttr; // Last transition explored from this state.
+      twa_succ_iterator* lasttr; // Last transition explored from this state.
       int lowlink;		  // Lowlink value if this entry.
       int pre;			  // DFS predecessor.
       int acc;			  // Accepting state link.
@@ -101,7 +101,7 @@ namespace spot
 		  << ", s = " << a_->format_state(stack[dftop].s)
 		  << ')' << std::endl;
 
-	    tgba_succ_iterator* iter = stack[dftop].lasttr;
+	    twa_succ_iterator* iter = stack[dftop].lasttr;
 	    bool cont;
 	    if (!iter)
 	      {

src/tgbaalgos/lbtt.cc

@@ -65,7 +65,7 @@ namespace spot
 	// we just check the acceptance of the first transition.  This
 	// is not terribly efficient since we have to create the
 	// iterator.
-	tgba_succ_iterator* it = aut_->succ_iter(s);
+	twa_succ_iterator* it = aut_->succ_iter(s);
 	bool accepting = it->first()
 	  && aut_->acc().accepting(it->current_acceptance_conditions());
 	aut_->release_iter(it);
@@ -74,7 +74,7 @@ namespace spot
 
 
       void
-      process_state(const state* s, int n, tgba_succ_iterator*)
+      process_state(const state* s, int n, twa_succ_iterator*)
       {
 	--n;
 	if (n == 0)
@@ -96,7 +96,7 @@ namespace spot
 
       void
       process_link(const state*, int,
-		   const state*, int out, const tgba_succ_iterator* si)
+		   const state*, int out, const twa_succ_iterator* si)
       {
 	body_ << out - 1 << ' ';
 	if (!sba_format_)

src/tgbaalgos/magic.cc

@@ -153,7 +153,7 @@ namespace spot
 		const bdd& label, acc_cond::mark_t acc)
       {
         inc_depth();
-        tgba_succ_iterator* i = a_->succ_iter(s);
+        twa_succ_iterator* i = a_->succ_iter(s);
         i->first();
         st.emplace_front(s, i, label, acc);
       }

src/tgbaalgos/ndfs_result.hxx

@@ -45,12 +45,12 @@ namespace spot
 {
   struct stack_item
   {
-    stack_item(const state* n, tgba_succ_iterator* i, bdd l, acc_cond::mark_t a)
+    stack_item(const state* n, twa_succ_iterator* i, bdd l, acc_cond::mark_t a)
       : s(n), it(i), label(l), acc(a) {};
     /// The visited state.
     const state* s;
     /// Design the next successor of \a s which has to be visited.
-    tgba_succ_iterator* it;
+    twa_succ_iterator* it;
     /// The label of the transition traversed to reach \a s
     /// (false for the first one).
     bdd label;
@@ -261,7 +261,7 @@ namespace spot
       const state* start = target->clone();
 
       seen.insert(start);
-      tgba_succ_iterator* i = a_->succ_iter(start);
+      twa_succ_iterator* i = a_->succ_iter(start);
       i->first();
       st1.emplace_front(start, i, bddfalse, 0U);
 
@@ -290,7 +290,7 @@ namespace spot
 		      this->inc_ars_cycle_states();
                       ndfsr_trace << "  it is not seen, go down" << std::endl;
                       seen.insert(s_prime);
-                      tgba_succ_iterator* i = a_->succ_iter(s_prime);
+                      twa_succ_iterator* i = a_->succ_iter(s_prime);
                       i->first();
                       st1.emplace_front(s_prime, i, label, acc);
                     }

src/tgbaalgos/reachiter.cc

@@ -59,7 +59,7 @@ namespace spot
       {
 	assert(seen.find(t) != seen.end());
 	int tn = seen[t];
-	tgba_succ_iterator* si = aut_->succ_iter(t);
+	twa_succ_iterator* si = aut_->succ_iter(t);
 	process_state(t, tn, si);
 	if (si->first())
 	  do
@@ -107,14 +107,14 @@ namespace spot
 
   void
   tgba_reachable_iterator::process_state(const state*, int,
-					 tgba_succ_iterator*)
+					 twa_succ_iterator*)
   {
   }
 
   void
   tgba_reachable_iterator::process_link(const state*, int,
 					const state*, int,
-					const tgba_succ_iterator*)
+					const twa_succ_iterator*)
   {
   }
 
@@ -167,7 +167,7 @@ namespace spot
   void
   tgba_reachable_iterator_depth_first::push(const state* s, int sn)
   {
-    tgba_succ_iterator* si = aut_->succ_iter(s);
+    twa_succ_iterator* si = aut_->succ_iter(s);
     process_state(s, sn, si);
     stack_item item = { s, sn, si };
     todo.push_back(item);
@@ -195,7 +195,7 @@ namespace spot
     const state* dst;
     while (!todo.empty())
       {
-	tgba_succ_iterator* si = todo.back().it;
+	twa_succ_iterator* si = todo.back().it;
 	if (si->done())
 	  {
 	    pop();
@@ -257,14 +257,14 @@ namespace spot
 
   void
   tgba_reachable_iterator_depth_first::process_state(const state*, int,
-						     tgba_succ_iterator*)
+						     twa_succ_iterator*)
   {
   }
 
   void
   tgba_reachable_iterator_depth_first::process_link(const state*, int,
 						    const state*, int,
-						    const tgba_succ_iterator*)
+						    const twa_succ_iterator*)
   {
   }
 

src/tgbaalgos/reachiter.hh

@@ -69,15 +69,15 @@ namespace spot
     ///
     /// \param s The current state.
     /// \param n A unique number assigned to \a s.
-    /// \param si The spot::tgba_succ_iterator for \a s.
+    /// \param si The spot::twa_succ_iterator for \a s.
-    virtual void process_state(const state* s, int n, tgba_succ_iterator* si);
+    virtual void process_state(const state* s, int n, twa_succ_iterator* si);
     /// Called by run() to process a transition.
     ///
     /// \param in_s The source state
     /// \param in The source state number.
     /// \param out_s The destination state
     /// \param out The destination state number.
-    /// \param si The spot::tgba_succ_iterator positionned on the current
+    /// \param si The spot::twa_succ_iterator positionned on the current
     ///             transition.
     ///
     /// The in_s and out_s states are owned by the
@@ -85,7 +85,7 @@ namespace spot
     /// instance is destroyed.
     virtual void process_link(const state* in_s, int in,
 			      const state* out_s, int out,
-			      const tgba_succ_iterator* si);
+			      const twa_succ_iterator* si);
 
   protected:
     const_tgba_ptr aut_;	///< The spot::tgba to explore.
@@ -139,15 +139,15 @@ namespace spot
     ///
     /// \param s The current state.
     /// \param n A unique number assigned to \a s.
-    /// \param si The spot::tgba_succ_iterator for \a s.
+    /// \param si The spot::twa_succ_iterator for \a s.
-    virtual void process_state(const state* s, int n, tgba_succ_iterator* si);
+    virtual void process_state(const state* s, int n, twa_succ_iterator* si);
     /// Called by run() to process a transition.
     ///
     /// \param in_s The source state
     /// \param in The source state number.
     /// \param out_s The destination state
     /// \param out The destination state number.
-    /// \param si The spot::tgba_succ_iterator positionned on the current
+    /// \param si The spot::twa_succ_iterator positionned on the current
     ///             transition.
     ///
     /// The in_s and out_s states are owned by the
@@ -155,7 +155,7 @@ namespace spot
     /// instance is destroyed.
     virtual void process_link(const state* in_s, int in,
 			      const state* out_s, int out,
-			      const tgba_succ_iterator* si);
+			      const twa_succ_iterator* si);
 
   protected:
     const_tgba_ptr aut_;		///< The spot::tgba to explore.
@@ -167,7 +167,7 @@ namespace spot
     {
       const state* src;
       int src_n;
-      tgba_succ_iterator* it;
+      twa_succ_iterator* it;
     };
     std::deque<stack_item> todo; ///< the DFS stack
 

src/tgbaalgos/replayrun.cc

@@ -34,7 +34,7 @@ namespace spot
     void
     print_annotation(std::ostream& os,
 		     const const_tgba_ptr& a,
-		     const tgba_succ_iterator* i)
+		     const twa_succ_iterator* i)
     {
       std::string s = a->transition_annotation(i);
       if (s == "")
@@ -138,7 +138,7 @@ namespace spot
 	  }
 
 	// browse the actual outgoing transitions
-	tgba_succ_iterator* j = a->succ_iter(s);
+	twa_succ_iterator* j = a->succ_iter(s);
 	// When not debugging, S is not used as key in SEEN, so we can
 	// destroy it right now.
 	if (!debug)

src/tgbaalgos/scc.cc

@@ -135,7 +135,7 @@ namespace spot
       root_.emplace_front(num_);
       arc_acc_.push(0U);
       arc_cond_.push(bddfalse);
-      tgba_succ_iterator* iter = aut_->succ_iter(init);
+      twa_succ_iterator* iter = aut_->succ_iter(init);
       iter->first();
       todo_.emplace(init, iter);
     }
@@ -146,7 +146,7 @@ namespace spot
 	assert(root_.size() == arc_cond_.size());
 
 	// We are looking at the next successor in SUCC.
-	tgba_succ_iterator* succ = todo_.top().second;
+	twa_succ_iterator* succ = todo_.top().second;
 
 	// If there is no more successor, backtrack.
 	if (succ->done())
@@ -212,7 +212,7 @@ namespace spot
 	    root_.emplace_front(num_);
 	    arc_acc_.push(acc);
 	    arc_cond_.push(cond);
-	    tgba_succ_iterator* iter = aut_->succ_iter(dest);
+	    twa_succ_iterator* iter = aut_->succ_iter(dest);
 	    iter->first();
 	    todo_.emplace(dest, iter);
 	    continue;

src/tgbaalgos/scc.hh

@@ -185,7 +185,7 @@ namespace spot
                                 // number states that are part of
                                 // incomplete SCCs being completed.
     int num_;			// Number of visited nodes, negated.
-    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
+    typedef std::pair<const spot::state*, twa_succ_iterator*> pair_state_iter;
     std::stack<pair_state_iter> todo_; // DFS stack.  Holds (STATE,
 				       // ITERATOR) pairs where
 				       // ITERATOR is an iterator over

src/tgbaalgos/se05.cc

@@ -153,7 +153,7 @@ namespace spot
 		const bdd& label, acc_cond::mark_t acc)
       {
         inc_depth();
-        tgba_succ_iterator* i = a_->succ_iter(s);
+        twa_succ_iterator* i = a_->succ_iter(s);
         i->first();
         st.emplace_front(s, i, label, acc);
       }

src/tgbaalgos/stats.cc

@@ -42,14 +42,14 @@ namespace spot
       }
 
       void
-      process_state(const state*, int, tgba_succ_iterator*)
+      process_state(const state*, int, twa_succ_iterator*)
       {
 	++s_.states;
       }
 
       void
       process_link(const state*, int, const state*, int,
-		   const tgba_succ_iterator*)
+		   const twa_succ_iterator*)
       {
 	++s_.transitions;
       }
@@ -68,7 +68,7 @@ namespace spot
 
       void
       process_link(const state*, int, const state*, int,
-		   const tgba_succ_iterator* it)
+		   const twa_succ_iterator* it)
       {
 	++s_.transitions;
 

src/tgbaalgos/stutter.cc

@@ -94,10 +94,10 @@ namespace spot
       bdd cond_;
     };
 
-    class tgbasl_succ_iterator : public tgba_succ_iterator
+    class tgbasl_succ_iterator : public twa_succ_iterator
     {
     public:
-      tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state,
+      tgbasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state,
 			   bdd_dict_ptr d, bdd atomic_propositions)
         : it_(it), state_(state), aps_(atomic_propositions), d_(d)
       {
@@ -191,7 +191,7 @@ namespace spot
           need_loop_ = false;
       }
 
-      tgba_succ_iterator* it_;
+      twa_succ_iterator* it_;
       const state_tgbasl* state_;
       bdd cond_;
       bdd one_;
@@ -225,7 +225,7 @@ namespace spot
 	return new state_tgbasl(a_->get_init_state(), bddfalse);
       }
 
-      virtual tgba_succ_iterator* succ_iter(const state* state) const override
+      virtual twa_succ_iterator* succ_iter(const state* state) const override
       {
 	const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
 	assert(s);

src/tgbaalgos/tau03.cc

@@ -126,7 +126,7 @@ namespace spot
 		const bdd& label, acc_cond::mark_t acc)
       {
         inc_depth();
-        tgba_succ_iterator* i = a_->succ_iter(s);
+        twa_succ_iterator* i = a_->succ_iter(s);
         i->first();
         st.emplace_front(s, i, label, acc);
       }

src/tgbaalgos/tau03opt.cc

@@ -141,7 +141,7 @@ namespace spot
 		const bdd& label, acc_cond::mark_t acc)
       {
         inc_depth();
-        tgba_succ_iterator* i = a_->succ_iter(s);
+        twa_succ_iterator* i = a_->succ_iter(s);
         i->first();
         st.emplace_front(s, i, label, acc);
       }