diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 106e222525cc9e23037a6a8b8f6038c37d2011ed..6faec223eb5a0165da66147cf55dd46c59c37c06 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -488,7 +488,7 @@ namespace
       // never modify the original automaton (e.g. with
       // merge_transitions()) and the statistics about it make sense.
       auto aut = ((automaton_format == Stats) || opt_name)
-	? spot::make_tgba_digraph(haut->aut, spot::tgba::prop_set::all())
+	? spot::make_tgba_digraph(haut->aut, spot::twa::prop_set::all())
 	: haut->aut;
 
       // Preprocessing.
@@ -577,7 +577,7 @@ namespace
         {
           auto tmp =
 	    spot::canonicalize(make_tgba_digraph(aut,
-						 spot::tgba::prop_set::all()));
+						 spot::twa::prop_set::all()));
           if (!opt->uniq->emplace(tmp->transition_vector().begin() + 1,
 				  tmp->transition_vector().end()).second)
 	    return 0;
diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc
index a7dbbd66d6beedf348c96757cb2ef7704c80de25..c00c7d0d90324a083907751848fd964e779833ce 100644
--- a/src/bin/randaut.cc
+++ b/src/bin/randaut.cc
@@ -307,7 +307,7 @@ main(int argc, char** argv)
 	  if (opt_uniq)
 	    {
 	      auto tmp = spot::canonicalize
-		(make_tgba_digraph(aut, spot::tgba::prop_set::all()));
+		(make_tgba_digraph(aut, spot::twa::prop_set::all()));
 	      std::vector<tr_t> trans(tmp->transition_vector().begin() + 1,
 				      tmp->transition_vector().end());
 	      if (!opt_uniq->emplace(trans).second)
diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh
index a13ccd7192761cb67aa106c864d490d1b9e12e1f..6f33c2eecc0373aa86101e9dd491d2fee13849d6 100644
--- a/src/kripke/fairkripke.hh
+++ b/src/kripke/fairkripke.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2013, 2014, 2015 Laboratoire de Recherche et
 // Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
@@ -85,11 +85,11 @@ namespace spot
   /// class and need not be defined.
   ///
   /// See also spot::fair_kripke_succ_iterator.
-  class SPOT_API fair_kripke: public tgba
+  class SPOT_API fair_kripke: public twa
   {
   public:
     fair_kripke(const bdd_dict_ptr& d)
-      : tgba(d)
+      : twa(d)
       {
       }
 
diff --git a/src/ta/tgta.cc b/src/ta/tgta.cc
index d0bf8dc7f5de06618c8e715d2fab9b6d74e9926d..7b86c3db5c4910fb2b33a4877be5965e80553a55 100644
--- a/src/ta/tgta.cc
+++ b/src/ta/tgta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,7 +23,7 @@
 namespace spot
 {
   tgta::tgta(const bdd_dict_ptr& d)
-    : tgba(d)
+    : twa(d)
   {};
   tgta::~tgta()
   {};
diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh
index ecabd8c9b4307396960a55c34810462ff7626e8d..8c309924d874c7da301ac27855bd324ea6f2f4b4 100644
--- a/src/ta/tgta.hh
+++ b/src/ta/tgta.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -56,7 +56,7 @@ namespace spot
   /// obtained by querying the iterator over the successors of
   /// a state.
 
-  class SPOT_API tgta : public tgba
+  class SPOT_API tgta : public twa
   {
 
   protected:
diff --git a/src/tgba/fwd.hh b/src/tgba/fwd.hh
index 5388acadcca9341e92ed1ca49482ef225e56c4f0..b8d32b8443668fcca7a4115c1eaecdeb09192f84 100644
--- a/src/tgba/fwd.hh
+++ b/src/tgba/fwd.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,9 +23,9 @@
 
 namespace spot
 {
-  class tgba;
-  typedef std::shared_ptr<tgba> tgba_ptr;
-  typedef std::shared_ptr<const tgba> const_tgba_ptr;
+  class twa;
+  typedef std::shared_ptr<twa> tgba_ptr;
+  typedef std::shared_ptr<const twa> const_tgba_ptr;
 
   class tgba_digraph;
   typedef std::shared_ptr<const tgba_digraph> const_tgba_digraph_ptr;
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index 2df276d03a7cbc7bba9e46ab8912b71076eb2a4e..827bca02181ecd1a9bcd1604d600ad10db4f2dd1 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -33,7 +33,7 @@ namespace spot
   `--------*/
 
   taa_tgba::taa_tgba(const bdd_dict_ptr& dict)
-    : tgba(dict),
+    : twa(dict),
       init_(0), state_set_vec_()
   {
   }
diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh
index e3e8ab051ac6854ff86f7f314cf297c269e7fbd9..e58fd7a8885844c9bb445e1497c59c6253a8a711 100644
--- a/src/tgba/taatgba.hh
+++ b/src/tgba/taatgba.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -33,7 +33,7 @@ namespace spot
 {
   /// \brief A self-loop Transition-based Alternating Automaton (TAA)
   /// which is seen as a TGBA (abstract class, see below).
-  class SPOT_API taa_tgba: public tgba
+  class SPOT_API taa_tgba: public twa
   {
   public:
     taa_tgba(const bdd_dict_ptr& dict);
diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc
index 9089ee038031ef831fb106613ba79a6dc89458a8..d34066f8ab54cbdf569d63c92c7030e40671f2a1 100644
--- a/src/tgba/tgba.cc
+++ b/src/tgba/tgba.cc
@@ -28,7 +28,7 @@
 
 namespace spot
 {
-  tgba::tgba(const bdd_dict_ptr& d)
+  twa::twa(const bdd_dict_ptr& d)
     : iter_cache_(nullptr),
       dict_(d),
       last_support_conditions_input_(0)
@@ -36,7 +36,7 @@ namespace spot
     props = 0U;
   }
 
-  tgba::~tgba()
+  twa::~twa()
   {
     if (last_support_conditions_input_)
       last_support_conditions_input_->destroy();
@@ -45,7 +45,7 @@ namespace spot
   }
 
   bdd
-  tgba::support_conditions(const state* state) const
+  twa::support_conditions(const state* state) const
   {
     if (!last_support_conditions_input_
 	|| last_support_conditions_input_->compare(state) != 0)
@@ -59,7 +59,7 @@ namespace spot
   }
 
   state*
-  tgba::project_state(const state* s,
+  twa::project_state(const state* s,
 		      const const_tgba_ptr& t) const
   {
     if (t.get() == this)
@@ -68,13 +68,13 @@ namespace spot
   }
 
   std::string
-  tgba::transition_annotation(const tgba_succ_iterator*) const
+  twa::transition_annotation(const tgba_succ_iterator*) const
   {
     return "";
   }
 
   bool
-  tgba::is_empty() const
+  twa::is_empty() const
   {
     // FIXME: This should be improved based on properties of the
     // automaton.  For instance we do not need couvreur99 is we know
@@ -91,8 +91,8 @@ namespace spot
   }
 
   void
-  tgba::set_named_prop(std::string s,
-		       void* val, std::function<void(void*)> destructor)
+  twa::set_named_prop(std::string s,
+		      void* val, std::function<void(void*)> destructor)
   {
     auto p = named_prop_.emplace(std::piecewise_construct,
 				 std::forward_as_tuple(s),
@@ -105,7 +105,7 @@ namespace spot
   }
 
   void*
-  tgba::get_named_prop_(std::string s) const
+  twa::get_named_prop_(std::string s) const
   {
     auto i = named_prop_.find(s);
     if (i == named_prop_.end())
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index aab3ded2569f3afb1445e33e5df62bdafc560822..edc5cea154aabd7e7c46ef16d201f54611afc718 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -431,46 +431,56 @@ namespace spot
     };
   }
 
-  /// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata)
+  /// \defgroup twa TωA (Transition-based ω-Automata)
   ///
-  /// Spot is centered around the spot::tgba type.  This type and its
+  /// Spot is centered around the spot::twa type.  This type and its
   /// cousins are listed \ref tgba_essentials "here".  This is an
   /// abstract interface.  Its implementations are either \ref
   /// tgba_representation "concrete representations", or \ref
   /// tgba_on_the_fly_algorithms "on-the-fly algorithms".  Other
-  /// algorithms that work on spot::tgba are \ref tgba_algorithms
+  /// algorithms that work on spot::twa are \ref tgba_algorithms
   /// "listed separately".
 
-  /// \addtogroup tgba_essentials Essential TGBA types
-  /// \ingroup tgba
+  /// \addtogroup tgba_essentials Essential TωA types
+  /// \ingroup twa
 
   /// \ingroup tgba_essentials
-  /// \brief A Transition-based Generalized Büchi Automaton.
+  /// \brief A Transition-based ω-Automaton.
   ///
-  /// The acronym TGBA (Transition-based Generalized Büchi Automaton)
-  /// was coined by Dimitra Giannakopoulou and Flavio Lerda
-  /// in "From States to Transitions: Improving Translation of LTL
-  /// Formulae to Büchi Automata".  (FORTE'02)
+  /// The acronym TωA stands for Transition-based ω-automaton.
+  /// We may write it as TwA or twa, but never as TWA as the
+  /// w is just a non-utf8 replacement for ω that should not be
+  /// capitalized.
   ///
-  /// TGBAs are transition-based, meanings their labels are put
-  /// on arcs, not on nodes.  They use Generalized Büchi acceptance
-  /// conditions: there are several acceptance sets (of
-  /// transitions), and a path can be accepted only if it traverses
-  /// at least one transition of each set infinitely often.
+  /// TωAs are transition-based automata, meanings that not-only
+  /// do they have labels on arcs, they also have an acceptance
+  /// condition defined in term of sets of transitions.
+  /// The acceptance condition can be anything supported by
+  /// the HOA format (http://adl.github.io/hoaf/).  The only
+  /// restriction w.r.t. the format is that this class does
+  /// not support alternating automata
+  ///
+  /// Previous version of Spot supported a type of automata called
+  /// TGBA, which are TωA in which the acceptance condition is a set
+  /// of sets of transitions that must be intersected infinitely
+  /// often.
+  ///
+  /// In this version, TGBAs are now represented by TωAs for which
+  /// <code>aut->acc().is_generalized_buchi())</code> returns true.
   ///
   /// Browsing such automaton can be achieved using two functions:
-  /// \c get_init_state, and \c succ_iter.  The former returns
+  /// \c get_init_state, and \c succ.  The former returns
   /// the initial state while the latter lists the
   /// successor states of any state.
   ///
-  /// Note that although this is a transition-based automata,
-  /// we never represent transitions!  Transition informations are
-  /// obtained by querying the iterator over the successors of
-  /// a state.
-  class SPOT_API tgba: public std::enable_shared_from_this<tgba>
+  /// Note that although this is a transition-based automata, we never
+  /// represent transitions in the API!  Transition data are
+  /// obtained by querying the iterator over the successors of a
+  /// state.
+  class SPOT_API twa: public std::enable_shared_from_this<twa>
   {
   protected:
-    tgba(const bdd_dict_ptr& d);
+    twa(const bdd_dict_ptr& d);
     // Any iterator returned via release_iter.
     mutable tgba_succ_iterator* iter_cache_;
     bdd_dict_ptr dict_;
@@ -480,10 +490,10 @@ namespace spot
     class succ_iterable
     {
     protected:
-      const tgba* aut_;
+      const twa* aut_;
       tgba_succ_iterator* it_;
     public:
-      succ_iterable(const tgba* aut, tgba_succ_iterator* it)
+      succ_iterable(const twa* aut, tgba_succ_iterator* it)
 	: aut_(aut), it_(it)
       {
       }
@@ -512,7 +522,7 @@ namespace spot
     };
 #endif
 
-    virtual ~tgba();
+    virtual ~twa();
 
     /// \brief Get the initial state of the automaton.
     ///
@@ -533,7 +543,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->out(s)) { /* i->current_state() */ }</code>.
+    /// <code>for (auto i: aut->succ(s)) { /* i->current_state() */ }</code>.
     succ_iterable
     succ(const state* s) const
     {
@@ -836,10 +846,10 @@ namespace spot
   };
 
   /// \addtogroup tgba_representation TGBA representations
-  /// \ingroup tgba
+  /// \ingroup twa
 
   /// \addtogroup tgba_algorithms TGBA algorithms
-  /// \ingroup tgba
+  /// \ingroup twa
 
   /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms
   /// \ingroup tgba_algorithms
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index eef3cc51aab0c39e26139cb7530303a728a4fecc..695bbd84f5a6d1c319f88e1eed3d0e67605495d1 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -169,7 +169,7 @@ namespace spot
 
   };
 
-  class SPOT_API tgba_digraph final: public tgba
+  class SPOT_API tgba_digraph final: public twa
   {
   public:
     typedef digraph<tgba_graph_state, tgba_graph_trans_data> graph_t;
@@ -181,13 +181,13 @@ namespace spot
 
   public:
     tgba_digraph(const bdd_dict_ptr& dict)
-      : tgba(dict),
+      : twa(dict),
 	init_number_(0)
     {
     }
 
     explicit tgba_digraph(const const_tgba_digraph_ptr& other, prop_set p)
-      : tgba(other->get_dict()),
+      : twa(other->get_dict()),
         g_(other->g_), init_number_(other->init_number_)
       {
 	copy_acceptance_of(other);
@@ -198,7 +198,7 @@ namespace spot
     virtual ~tgba_digraph()
     {
       get_dict()->unregister_all_my_variables(this);
-      // Prevent this state from being destroyed by ~tgba(),
+      // Prevent this state from being destroyed by ~twa(),
       // as the state will be destroyed when g_ is destroyed.
       last_support_conditions_input_ = 0;
     }
@@ -459,19 +459,19 @@ namespace spot
   }
 
   inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut,
-					    tgba::prop_set p)
+					    twa::prop_set p)
   {
     return std::make_shared<tgba_digraph>(aut, p);
   }
 
   inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut,
-					    tgba::prop_set p)
+					    twa::prop_set p)
   {
     return std::make_shared<tgba_digraph>(aut, p);
   }
 
   inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut,
-					    tgba::prop_set p)
+					    twa::prop_set p)
   {
     auto a = std::dynamic_pointer_cast<const tgba_digraph>(aut);
     if (a)
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index f8adacb18dc125c09da7e4d0530d97b77acd81c8..d5f11c4cc322c442301981deb36e9d0641f2017c 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -284,7 +284,7 @@ namespace spot
 
   tgba_product::tgba_product(const const_tgba_ptr& left,
 			     const const_tgba_ptr& right)
-    : tgba(left->get_dict()), left_(left), right_(right),
+    : twa(left->get_dict()), left_(left), right_(right),
       pool_(sizeof(state_product))
   {
     assert(get_dict() == right_->get_dict());
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index b0d42fc3384a94a43abe4c311217cd4c55adb138..278b759ede3dc21326e044d81bfac79e1660f41c 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -77,7 +77,7 @@ namespace spot
 
 
   /// \brief A lazy product.  (States are computed on the fly.)
-  class SPOT_API tgba_product: public tgba
+  class SPOT_API tgba_product: public twa
   {
   public:
     /// \brief Constructor.
diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc
index f5abd77930a48c7987828e6fc310e28bd8a788d2..2b8e2deca6e7fd2e6ad38935c1f9717f4e71aad9 100644
--- a/src/tgba/tgbaproxy.cc
+++ b/src/tgba/tgbaproxy.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -22,7 +22,7 @@
 namespace spot
 {
   tgba_proxy::tgba_proxy(const const_tgba_ptr& original)
-    : tgba(original->get_dict()), original_(original)
+    : twa(original->get_dict()), original_(original)
   {
     get_dict()->register_all_variables_of(original, this);
     acc_.add_sets(original->acc().num_sets());
diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh
index 40956921cdae5d2243cd153102edea5a3e9759e7..8fb2055a39cdd1302cf95464f68ce3fd9eef5880 100644
--- a/src/tgba/tgbaproxy.hh
+++ b/src/tgba/tgbaproxy.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -32,7 +32,7 @@ namespace spot
   /// original automaton right away.  However it is useful
   /// to inherit from this class and override some of its
   /// methods to implement some on-the-fly algorithm.
-  class SPOT_API tgba_proxy: public tgba
+  class SPOT_API tgba_proxy: public twa
   {
   protected:
     tgba_proxy(const const_tgba_ptr& original);
diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc
index 35d2f7e28aa912d904e87e24f238e2f4d1af16ec..e3f85669fd76c10f0afa5f007a41a3e9f13f1b42 100644
--- a/src/tgba/tgbasafracomplement.cc
+++ b/src/tgba/tgbasafracomplement.cc
@@ -1074,7 +1074,7 @@ namespace spot
   //////////////////////////
 
   tgba_safra_complement::tgba_safra_complement(const const_tgba_digraph_ptr& a)
-    : tgba(a->get_dict()), automaton_(a),
+    : twa(a->get_dict()), automaton_(a),
       safra_(safra_determinisation::create_safra_automaton(a))
   {
     assert(safra_ || !"safra construction fails");
diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh
index 44bcefd830f9b625162e270a95fd599d302ebdf3..a05311ef856871dcd9a1ef7f01b8fb6c960804de 100644
--- a/src/tgba/tgbasafracomplement.hh
+++ b/src/tgba/tgbasafracomplement.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -46,7 +46,7 @@ namespace spot
   ///  is done on-the-fly when successors are called.
   ///
   /// \sa safra_determinisation, tgba_safra_complement::succ_iter.
-  class SPOT_API tgba_safra_complement : public tgba
+  class SPOT_API tgba_safra_complement : public twa
   {
   public:
     tgba_safra_complement(const const_tgba_digraph_ptr& a);
diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc
index 5deafe8c0a013b556faf14bd61e44ea23bc4adbc..69e72907d94045743d938f580ca22ec16a8e2269 100644
--- a/src/tgbaalgos/are_isomorphic.cc
+++ b/src/tgbaalgos/are_isomorphic.cc
@@ -112,7 +112,7 @@ namespace spot
 {
   isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref)
   {
-    ref_ = make_tgba_digraph(ref, tgba::prop_set::all());
+    ref_ = make_tgba_digraph(ref, twa::prop_set::all());
     ref_deterministic_ = ref_->is_deterministic();
     if (!ref_deterministic_)
       {
@@ -144,7 +144,7 @@ namespace spot
           }
       }
 
-    auto tmp = make_tgba_digraph(aut, tgba::prop_set::all());
+    auto tmp = make_tgba_digraph(aut, twa::prop_set::all());
     spot::canonicalize(tmp);
     return *tmp == *ref_;
   }
diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc
index e6523f53a8d5b8453a60b1eba0c201ec95175765..34fd1498e2989a303601e8f83f64de345d1a7ed0 100644
--- a/src/tgbaalgos/cleanacc.cc
+++ b/src/tgbaalgos/cleanacc.cc
@@ -56,7 +56,7 @@ namespace spot
   tgba_digraph_ptr cleanup_acceptance(const_tgba_digraph_ptr aut)
   {
     return cleanup_acceptance_here(make_tgba_digraph(aut,
-						     tgba::prop_set::all()));
+						     twa::prop_set::all()));
   }
 
 
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index 904474f55754cc99c77661cf0b14a0842eb20736..7d0f486202ecb166e2a951107a640fb687319292 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -494,7 +494,7 @@ namespace spot
     dotty_output d(os, options);
     auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
     if (!aut)
-      aut = make_tgba_digraph(g, tgba::prop_set::all());
+      aut = make_tgba_digraph(g, twa::prop_set::all());
     d.print(aut);
     return os;
   }
diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc
index ef6e1b89861712f71cb3a41e2daf66a83a31e0c3..e49591dba6c07704d02e1c66a9aa4c1b432a97d3 100644
--- a/src/tgbaalgos/dupexp.cc
+++ b/src/tgbaalgos/dupexp.cc
@@ -36,7 +36,7 @@ namespace spot
     class dupexp_iter: public T
     {
     public:
-      dupexp_iter(const const_tgba_ptr& a, tgba::prop_set p)
+      dupexp_iter(const const_tgba_ptr& a, twa::prop_set p)
 	: T(a), out_(make_tgba_digraph(a->get_dict()))
       {
 	out_->copy_acceptance_of(a);
@@ -76,7 +76,7 @@ namespace spot
   } // anonymous
 
   tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p)
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p)
   {
     dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut, p);
     di.run();
@@ -84,7 +84,7 @@ namespace spot
   }
 
   tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p)
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p)
   {
     dupexp_iter<tgba_reachable_iterator_depth_first> di(aut, p);
     di.run();
diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh
index b8ba1751991986898e2dcb7f1aebda0a4d0d4256..5cf83dcd3d82b8ac609426eb31f38cbab77c3110 100644
--- a/src/tgbaalgos/dupexp.hh
+++ b/src/tgbaalgos/dupexp.hh
@@ -33,10 +33,10 @@ namespace spot
   /// \brief Build an explicit automaton from all states of \a aut,
   /// numbering states in bread first order as they are processed.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_bfs(const const_tgba_ptr& aut, tgba::prop_set p);
+  tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p);
   /// \ingroup tgba_misc
   /// \brief Build an explicit automaton from all states of \a aut,
   /// numbering states in depth first order as they are processed.
   SPOT_API tgba_digraph_ptr
-  tgba_dupexp_dfs(const const_tgba_ptr& aut, tgba::prop_set p);
+  tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p);
 }
diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc
index f9148e1083c54d90f687b54544cc8e95d7573607..3a631d31ab690e41850b29492f342d336d9610f7 100644
--- a/src/tgbaalgos/hoa.cc
+++ b/src/tgbaalgos/hoa.cc
@@ -438,7 +438,7 @@ namespace spot
 
     auto a = std::dynamic_pointer_cast<const tgba_digraph>(aut);
     if (!a)
-      a = make_tgba_digraph(aut, tgba::prop_set::all());
+      a = make_tgba_digraph(aut, twa::prop_set::all());
 
     return hoa_reachable(os, a, opt);
   }
diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc
index 66bbf73ae3445548bf8cf9ac0184e1178eb438a3..5d2ee43034534d5891512483e3d2653b1c4c4459 100644
--- a/src/tgbaalgos/neverclaim.cc
+++ b/src/tgbaalgos/neverclaim.cc
@@ -210,7 +210,7 @@ namespace spot
     never_claim_output d(os, options);
     auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
     if (!aut)
-      aut = make_tgba_digraph(g, tgba::prop_set::all());
+      aut = make_tgba_digraph(g, twa::prop_set::all());
     d.print(aut);
     return os;
   }
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 4a0c130a8f000c193e8778a9588ac7dac8d11300..b6a62f83a1009c8ddcb736967b54875f16925e0c 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -242,7 +242,7 @@ namespace spot
 	  }
 	else
 	  {
-	    a_ = make_tgba_digraph(in, tgba::prop_set::all());
+	    a_ = make_tgba_digraph(in, twa::prop_set::all());
 	    auto& acccond = a_->acc();
 	    for (auto& t: a_->transitions())
 	      t.acc = acccond.comp(t.acc);
diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc
index 916ef556f6309f2177bd73ed1da5102548dae97d..70f62077730b1a724eb2a62b7defa1fcaab89a25 100644
--- a/src/tgbaalgos/stutter.cc
+++ b/src/tgbaalgos/stutter.cc
@@ -203,11 +203,11 @@ namespace spot
     };
 
 
-    class tgbasl final : public tgba
+    class tgbasl final : public twa
     {
     public:
       tgbasl(const const_tgba_ptr& a, bdd atomic_propositions)
-	: tgba(a->get_dict()), a_(a), aps_(atomic_propositions)
+	: twa(a->get_dict()), a_(a), aps_(atomic_propositions)
       {
 	get_dict()->register_all_propositions_of(&a_, this);
 	assert(acc_.num_sets() == 0);
@@ -442,7 +442,7 @@ namespace spot
   tgba_digraph_ptr
   sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
   {
-    return sl2(make_tgba_digraph(a, tgba::prop_set::all()),
+    return sl2(make_tgba_digraph(a, twa::prop_set::all()),
 	       atomic_propositions);
   }
 
diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc
index 836b256e516b34f91dba75b206e0dbcf8d3b89b6..7e7ef0ee60ab519af616576f9f9a09d56b519189 100644
--- a/src/tgbatest/checkpsl.cc
+++ b/src/tgbatest/checkpsl.cc
@@ -94,10 +94,10 @@ main(int argc, char** argv)
 	{
 	  auto apos =
 	    scc_filter(make_tgba_digraph(ltl_to_taa(fpos, d),
-					 spot::tgba::prop_set::all()));
+					 spot::twa::prop_set::all()));
 	  auto aneg =
 	    scc_filter(make_tgba_digraph(ltl_to_taa(fneg, d),
-					 spot::tgba::prop_set::all()));
+					 spot::twa::prop_set::all()));
 	  if (!spot::product(apos, aneg)->is_empty())
 	    {
 	      std::cerr << "non-empty intersection between pos and neg (TAA)\n";
diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc
index af91044f465b4b0afa850aea4b7f412100ea94c9..33e4a9a767bbdc666879e7b47cb119577cfdd521 100644
--- a/src/tgbatest/emptchk.cc
+++ b/src/tgbatest/emptchk.cc
@@ -102,7 +102,7 @@ main(int argc, char** argv)
       {
 	auto a = spot::ltl_to_taa(f, d);
 	aut[0] = a;
-	auto all = spot::tgba::prop_set::all();
+	auto all = spot::twa::prop_set::all();
 	aut[1] = spot::degeneralize_tba(spot::make_tgba_digraph(a, all));
       }
       {
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 1c8fc23bf35c26694b6a6ffb53b7ac14158a13f5..78c23e647ac7fea7b7b7ce1f86f9a51c5518ed81 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -314,7 +314,7 @@ spot::tgba_digraph_ptr ensure_digraph(const spot::tgba_ptr& a)
   auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
   if (aa)
     return aa;
-  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
+  return spot::make_tgba_digraph(a, spot::twa::prop_set::all());
 }
 
 int
@@ -1323,10 +1323,10 @@ checked_main(int argc, char** argv)
 	case NoneDup:
 	  break;
 	case BFS:
-	  a = tgba_dupexp_bfs(a, spot::tgba::prop_set::all());
+	  a = tgba_dupexp_bfs(a, spot::twa::prop_set::all());
 	  break;
 	case DFS:
-	  a = tgba_dupexp_dfs(a, spot::tgba::prop_set::all());
+	  a = tgba_dupexp_dfs(a, spot::twa::prop_set::all());
 	  break;
 	}
 
diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index e4e8b4810fa8bb5971df84d6a7bf64fe85db35fb..ebb7df2b0e651d431d3c521a222465cd06da2aff 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -54,7 +54,7 @@ def _render_automaton_as_svg(a, opt=None):
     dotty_reachable(ostr, a, opt)
     return _ostream_to_svg(ostr)
 
-tgba._repr_svg_ = _render_automaton_as_svg
+twa._repr_svg_ = _render_automaton_as_svg
 ta._repr_svg_ = _render_automaton_as_svg
 
 def _render_formula_as_svg(a):
@@ -72,7 +72,7 @@ def _return_automaton_as_svg(a, opt=None):
     # installed.
     from IPython.display import SVG
     return SVG(_render_automaton_as_svg(a, opt))
-tgba.show = _return_automaton_as_svg
+twa.show = _return_automaton_as_svg
 ta.show = _return_automaton_as_svg
 
 def _formula_str_ctor(self, str):
@@ -100,7 +100,7 @@ formula.__init__ = _formula_str_ctor
 formula.to_str = _formula_to_str
 formula.show_ast = _render_formula_as_svg
 
-def _tgba_to_str(a, format='hoa', opt=None):
+def _twa_to_str(a, format='hoa', opt=None):
     format = format.lower()
     if format == 'hoa':
         ostr = ostringstream()
@@ -120,7 +120,7 @@ def _tgba_to_str(a, format='hoa', opt=None):
         return ostr.str()
     raise ValueError("unknown string format: " + format)
 
-def _tgba_save(a, filename, format='hoa', opt=None, append=False):
+def _twa_save(a, filename, format='hoa', opt=None, append=False):
     with open(filename, 'a' if append else 'w') as f:
         s = a.to_str(format, opt)
         f.write(s)
@@ -128,8 +128,8 @@ def _tgba_save(a, filename, format='hoa', opt=None, append=False):
             f.write('\n')
     return a
 
-tgba.to_str = _tgba_to_str
-tgba.save = _tgba_save
+twa.to_str = _twa_to_str
+twa.save = _twa_save
 
 def automata(*filenames):
     """Read automata from a list of filenames.
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index d4f6caccf28503ab6a3eb9ebbc936cd4cf43c2f9..4c7e8e9960c40d973aac97fa1cda5461650f85b2 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -48,7 +48,7 @@
 %shared_ptr(spot::tgta)
 %shared_ptr(spot::tgta_explicit)
 %shared_ptr(spot::bdd_dict)
-%shared_ptr(spot::tgba)
+%shared_ptr(spot::twa)
 %shared_ptr(spot::tgba_digraph)
 %shared_ptr(spot::tgba_product)
 %shared_ptr(spot::tgba_product_init)
@@ -381,7 +381,7 @@ ensure_digraph(const spot::tgba_ptr& a)
   auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
   if (aa)
     return aa;
-  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
+  return spot::make_tgba_digraph(a, spot::twa::prop_set::all());
 }
 
 std::ostream&