diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index ca380967e..616c12ef4 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -148,7 +148,7 @@ namespace spot // could be improved. { state_set keep(sl.begin(), sl.end()); - auto masked = build_tgba_mask_keep(dra->aut, keep, sl.front()); + auto masked = build_twa_mask_keep(dra->aut, keep, sl.front()); if (!nra_to_nba(dra, masked)->is_empty()) // This SCC is not DBA-realizable. return false; @@ -187,7 +187,7 @@ namespace spot //std::cerr << "unknown\n"; // Build a sub-automaton for just the unknown states, // starting from any state in the SCC. - auto scc_mask = build_tgba_mask_keep(aut, unknown, *unknown.begin()); + auto scc_mask = build_twa_mask_keep(aut, unknown, *unknown.begin()); state_list local_final; state_list local_nonfinal; bool dbarealizable = diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index daa591f73..c3082a5ca 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -84,14 +84,14 @@ namespace spot /// /// This is an abstract class. You should inherit from it and /// supply a wanted() method to specify which states to keep. - class tgba_mask: public twa_proxy + class twa_mask: public twa_proxy { protected: /// \brief Constructor. /// \param masked The automaton to mask /// \param init Any state to use as initial state. This state will be /// destroyed by the destructor. - tgba_mask(const const_twa_ptr& masked, const state* init = 0): + twa_mask(const const_twa_ptr& masked, const state* init = 0): twa_proxy(masked), init_(init) { @@ -101,7 +101,7 @@ namespace spot public: - virtual ~tgba_mask() + virtual ~twa_mask() { init_->destroy(); } @@ -146,14 +146,14 @@ namespace spot const state* init_; }; - class tgba_mask_keep: public tgba_mask + class twa_mask_keep: public twa_mask { const state_set& mask_; public: - tgba_mask_keep(const const_twa_ptr& masked, + twa_mask_keep(const const_twa_ptr& masked, const state_set& mask, const state* init) - : tgba_mask(masked, init), + : twa_mask(masked, init), mask_(mask) { } @@ -165,14 +165,14 @@ namespace spot } }; - class tgba_mask_ignore: public tgba_mask + class twa_mask_ignore: public twa_mask { const state_set& mask_; public: - tgba_mask_ignore(const const_twa_ptr& masked, + twa_mask_ignore(const const_twa_ptr& masked, const state_set& mask, const state* init) - : tgba_mask(masked, init), + : twa_mask(masked, init), mask_(mask) { } @@ -184,14 +184,14 @@ namespace spot } }; - class tgba_mask_acc_ignore: public tgba_mask + class twa_mask_acc_ignore: public twa_mask { unsigned mask_; public: - tgba_mask_acc_ignore(const const_twa_ptr& masked, + twa_mask_acc_ignore(const const_twa_ptr& masked, unsigned mask, const state* init) - : tgba_mask(masked, init), + : twa_mask(masked, init), mask_(mask) { } @@ -205,27 +205,27 @@ namespace spot } const_twa_ptr - build_tgba_mask_keep(const const_twa_ptr& to_mask, + build_twa_mask_keep(const const_twa_ptr& to_mask, const state_set& to_keep, const state* init) { - return std::make_shared(to_mask, to_keep, init); + return std::make_shared(to_mask, to_keep, init); } const_twa_ptr - build_tgba_mask_ignore(const const_twa_ptr& to_mask, + build_twa_mask_ignore(const const_twa_ptr& to_mask, const state_set& to_ignore, const state* init) { - return std::make_shared(to_mask, to_ignore, init); + return std::make_shared(to_mask, to_ignore, init); } const_twa_ptr - build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask, + build_twa_mask_acc_ignore(const const_twa_ptr& to_mask, unsigned to_ignore, const state* init) { - return std::make_shared(to_mask, to_ignore, init); + return std::make_shared(to_mask, to_ignore, init); } } diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh index 49261c705..94ca2803f 100644 --- a/src/tgba/tgbamask.hh +++ b/src/tgba/tgbamask.hh @@ -32,7 +32,7 @@ namespace spot /// states from \a to_keep. The initial state /// can optionally be reset to \a init. SPOT_API const_twa_ptr - build_tgba_mask_keep(const const_twa_ptr& to_mask, + build_twa_mask_keep(const const_twa_ptr& to_mask, const state_set& to_keep, const state* init = 0); @@ -43,7 +43,7 @@ namespace spot /// in \a to_ignore. The initial state can optionally be reset to /// \a init. SPOT_API const_twa_ptr - build_tgba_mask_ignore(const const_twa_ptr& to_mask, + build_twa_mask_ignore(const const_twa_ptr& to_mask, const state_set& to_ignore, const state* init = 0); @@ -60,7 +60,7 @@ namespace spot /// function is only needed in graph algorithms that do not call /// all_acceptance_conditions(). SPOT_API const_twa_ptr - build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask, + build_twa_mask_acc_ignore(const const_twa_ptr& to_mask, unsigned to_ignore, const state* init = 0); }