From 5d9778474fd6d843005719f57fea40b65050a411 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Apr 2015 19:34:51 +0200 Subject: [PATCH] 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 | 2 +- src/dstarparse/nra2nba.cc | 2 +- src/kripke/fairkripke.hh | 2 +- src/kripke/kripke.hh | 2 +- src/kripke/kripkeprint.cc | 6 ++-- src/ta/ta.hh | 2 +- src/ta/taproduct.hh | 2 +- src/ta/tgta.hh | 2 +- src/ta/tgtaexplicit.cc | 4 +-- src/ta/tgtaexplicit.hh | 4 +-- src/ta/tgtaproduct.cc | 2 +- src/ta/tgtaproduct.hh | 8 ++--- src/taalgos/emptinessta.cc | 2 +- src/taalgos/reachiter.hh | 2 +- src/taalgos/tgba2ta.cc | 18 +++++----- src/tgba/taatgba.cc | 2 +- src/tgba/taatgba.hh | 4 +-- src/tgba/tgba.cc | 2 +- src/tgba/tgba.hh | 26 +++++++------- src/tgba/tgbagraph.hh | 12 +++---- src/tgba/tgbamask.cc | 4 +-- src/tgba/tgbaproduct.cc | 60 ++++++++++++++++----------------- src/tgba/tgbaproduct.hh | 4 +-- src/tgba/tgbaproxy.cc | 4 +-- src/tgba/tgbaproxy.hh | 4 +-- src/tgba/tgbasafracomplement.cc | 4 +-- src/tgba/tgbasafracomplement.hh | 2 +- src/tgbaalgos/bfssteps.hh | 2 +- src/tgbaalgos/compsusp.cc | 2 +- src/tgbaalgos/dupexp.cc | 4 +-- src/tgbaalgos/gtec/gtec.cc | 14 ++++---- src/tgbaalgos/gtec/gtec.hh | 4 +-- src/tgbaalgos/gv04.cc | 4 +-- src/tgbaalgos/lbtt.cc | 6 ++-- src/tgbaalgos/magic.cc | 2 +- src/tgbaalgos/ndfs_result.hxx | 8 ++--- src/tgbaalgos/reachiter.cc | 14 ++++---- src/tgbaalgos/reachiter.hh | 18 +++++----- src/tgbaalgos/replayrun.cc | 4 +-- src/tgbaalgos/scc.cc | 6 ++-- src/tgbaalgos/scc.hh | 2 +- src/tgbaalgos/se05.cc | 2 +- src/tgbaalgos/stats.cc | 6 ++-- src/tgbaalgos/stutter.cc | 8 ++--- src/tgbaalgos/tau03.cc | 2 +- src/tgbaalgos/tau03opt.cc | 2 +- 46 files changed, 149 insertions(+), 149 deletions(-) diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index 4daa8ca9d..f6ffdc082 100644 --- a/src/dstarparse/dra2ba.cc +++ b/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); diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 2aab4b54a..9fb87864d 100644 --- a/src/dstarparse/nra2nba.cc +++ b/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); diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 6f33c2eec..4c6b0a920 100644 --- a/src/kripke/fairkripke.hh +++ b/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 diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh index cf3b6dc3a..47b05e8b3 100644 --- a/src/kripke/kripke.hh +++ b/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 diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index 65ec3cb7e..2a50ac130 100644 --- a/src/kripke/kripkeprint.cc +++ b/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; } diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 83d881a9e..30724d356 100644 --- a/src/ta/ta.hh +++ b/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 diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index df4b644c0..cb786b285 100644 --- a/src/ta/taproduct.hh +++ b/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_; diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh index 8c309924d..c12e31861 100644 --- a/src/ta/tgta.hh +++ b/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; }; diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 77ec99f86..d940ba43e 100644 --- a/src/ta/tgtaexplicit.cc +++ b/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); diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 87e0627f8..84fbf0c22 100644 --- a/src/ta/tgtaexplicit.hh +++ b/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; diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index 4b4157c0a..4825a0c98 100644 --- a/src/ta/tgtaproduct.cc +++ b/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 (state); diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 9620abff6..f58186903 100644 --- a/src/ta/tgtaproduct.hh +++ b/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_; - tgba_succ_iterator* kripke_succ_it_; + twa_succ_iterator* tgta_succ_it_; + twa_succ_iterator* kripke_succ_it_; state_product* current_state_; bdd current_condition_; acc_cond::mark_t current_acceptance_conditions_; diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 1b562d14b..10afe8e98 100644 --- a/src/taalgos/emptinessta.cc +++ b/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. diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh index f092c2148..dc5cf6683 100644 --- a/src/taalgos/reachiter.hh +++ b/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); diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index fc38d3808..eb0c054e9 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -45,7 +45,7 @@ namespace spot namespace { - typedef std::pair pair_state_iter; + typedef std::pair 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()) diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 827bca021..9badf2890 100644 --- a/src/tgba/taatgba.cc +++ b/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(state); diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index e58fd7a88..21b8fc527 100644 --- a/src/tgba/taatgba.hh +++ b/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); diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index bcdd2c31b..aa9d6b43b 100644 --- a/src/tgba/tgba.cc +++ b/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 ""; } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index edc5cea15..0221d5419 100644 --- a/src/tgba/tgba.hh +++ b/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. /// diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index f3bf0808d..9db68d81f 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -106,7 +106,7 @@ namespace spot template 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(state_from_number(init_number_)); } - virtual tgba_succ_iterator* + virtual twa_succ_iterator* succ_iter(const state* st) const { auto s = down_cast(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*>(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*>(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*>(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*>(it); return g_.trans_storage(i->pos()); diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index b1d13665a..c445ed1da 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -32,7 +32,7 @@ namespace spot }; typedef std::vector 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; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index f53813d61..0aa2be032 100644 --- a/src/tgba/tgbaproduct.cc +++ b/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, - tgba_succ_iterator* right, + twa_succ_iterator_product_common(twa_succ_iterator* left, + 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, - const_tgba_ptr r, tgba_succ_iterator* right) + void recycle(const const_tgba_ptr& l, twa_succ_iterator* left, + 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_; - tgba_succ_iterator* right_; + twa_succ_iterator* left_; + 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, - tgba_succ_iterator* right, + twa_succ_iterator_product(twa_succ_iterator* left, + 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: - public tgba_succ_iterator_product_common + class twa_succ_iterator_product_kripke: + public twa_succ_iterator_product_common { public: - tgba_succ_iterator_product_kripke(tgba_succ_iterator* left, - tgba_succ_iterator* right, + twa_succ_iterator_product_kripke(twa_succ_iterator* left, + 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(state); assert(s); - tgba_succ_iterator* li = left_->succ_iter(s->left()); - tgba_succ_iterator* ri = right_->succ_iter(s->right()); + twa_succ_iterator* li = left_->succ_iter(s->left()); + twa_succ_iterator* ri = right_->succ_iter(s->right()); if (iter_cache_) { - tgba_succ_iterator_product_common* it = - down_cast(iter_cache_); + twa_succ_iterator_product_common* it = + down_cast(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(&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 = - down_cast(t); + const twa_succ_iterator_product_common* i = + down_cast(t); assert(i); std::string left = left_->transition_annotation(i->left_); std::string right = right_->transition_annotation(i->right_); diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 8d5c0fc2e..15181b1e2 100644 --- a/src/tgba/tgbaproduct.hh +++ b/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; diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc index 2b8e2deca..73b2c822d 100644 --- a/src/tgba/tgbaproxy.cc +++ b/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); } diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh index 8fb2055a3..6bcbf98ff 100644 --- a/src/tgba/tgbaproxy.hh +++ b/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; diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index e190a223c..e5a5fad8e 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/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 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_); diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index c47cf04e6..1078bdd1f 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/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; diff --git a/src/tgbaalgos/bfssteps.hh b/src/tgbaalgos/bfssteps.hh index 1c22a887c..49f70a1ce 100644 --- a/src/tgbaalgos/bfssteps.hh +++ b/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(). /// diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 07e4aef39..e91e6a2e0 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/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) { diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index de20804de..14e0fb506 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/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(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(), diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 997b02864..bd49c2a67 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -37,7 +37,7 @@ namespace spot { namespace { - typedef std::pair pair_state_iter; + typedef std::pair 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 to_remove; + std::stack 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(); diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 155e579c1..4e1a3d2b0 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/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. /// diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index defb43df2..b41859bd5 100644 --- a/src/tgbaalgos/gv04.cc +++ b/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) { diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index acae023c6..2ea28f760 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/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_) diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index b3fbae189..973d9d319 100644 --- a/src/tgbaalgos/magic.cc +++ b/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); } diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 3949baabd..856de2459 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/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); } diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index dc2e95a2e..2c625b584 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/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*) { } diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index cd213661d..10cfe7841 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/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. - virtual void process_state(const state* s, int n, tgba_succ_iterator* si); + /// \param si The spot::twa_succ_iterator for \a s. + 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. - virtual void process_state(const state* s, int n, tgba_succ_iterator* si); + /// \param si The spot::twa_succ_iterator for \a s. + 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 todo; ///< the DFS stack diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 88357e573..592f017a1 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/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) diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 83d40005e..a10aa4f65 100644 --- a/src/tgbaalgos/scc.cc +++ b/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; diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 3c314f126..040db759b 100644 --- a/src/tgbaalgos/scc.hh +++ b/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 pair_state_iter; + typedef std::pair pair_state_iter; std::stack todo_; // DFS stack. Holds (STATE, // ITERATOR) pairs where // ITERATOR is an iterator over diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 53a4e9110..107a8239f 100644 --- a/src/tgbaalgos/se05.cc +++ b/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); } diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index cf39a728c..2ea5ed343 100644 --- a/src/tgbaalgos/stats.cc +++ b/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; diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index ca33bca72..439c4d196 100644 --- a/src/tgbaalgos/stutter.cc +++ b/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(state); assert(s); diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index b89be1e89..4d3bc601d 100644 --- a/src/tgbaalgos/tau03.cc +++ b/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); } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 46f7812c4..4f98a5367 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/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); }