From bd870f9ab824243c55a28b15ed71138053f4b2fb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 Feb 2014 19:43:03 +0100 Subject: [PATCH] tgba: remove the global_state and global_automaton argument of succ_iter * iface/dve2/dve2.cc, src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, 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/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc: Here. * NEWS: Mention it. --- NEWS | 3 +++ iface/dve2/dve2.cc | 9 ++++----- src/kripke/kripkeexplicit.cc | 10 +++------- src/kripke/kripkeexplicit.hh | 4 +--- src/ta/tgtaexplicit.cc | 3 +-- src/ta/tgtaexplicit.hh | 3 +-- src/ta/tgtaproduct.cc | 5 ++--- src/ta/tgtaproduct.hh | 3 +-- src/tgba/taatgba.cc | 6 +----- src/tgba/taatgba.hh | 5 +---- src/tgba/tgba.hh | 23 +---------------------- src/tgba/tgbabddconcrete.cc | 14 ++------------ src/tgba/tgbabddconcrete.hh | 4 +--- src/tgba/tgbaexplicit.hh | 7 +------ src/tgba/tgbakvcomplement.cc | 14 ++++++-------- src/tgba/tgbakvcomplement.hh | 5 +---- src/tgba/tgbamask.cc | 8 +++----- src/tgba/tgbamask.hh | 6 ++---- src/tgba/tgbaproduct.cc | 22 ++++------------------ src/tgba/tgbaproduct.hh | 4 +--- src/tgba/tgbaproxy.cc | 6 ++---- src/tgba/tgbaproxy.hh | 4 +--- src/tgba/tgbasafracomplement.cc | 7 ++----- src/tgba/tgbasafracomplement.hh | 5 +---- src/tgba/tgbascc.cc | 6 ++---- src/tgba/tgbascc.hh | 5 +---- src/tgba/tgbasgba.cc | 12 +++--------- src/tgba/tgbasgba.hh | 5 +---- src/tgba/tgbatba.cc | 6 ++---- src/tgba/tgbatba.hh | 5 +---- src/tgba/tgbaunion.cc | 8 ++------ src/tgba/tgbaunion.hh | 4 +--- src/tgba/wdbacomp.cc | 11 ++++------- 33 files changed, 63 insertions(+), 179 deletions(-) diff --git a/NEWS b/NEWS index 22e7d793e..3060576bc 100644 --- a/NEWS +++ b/NEWS @@ -60,6 +60,9 @@ New in spot 1.2.3a (not yet released) methods have been removed from the TGBA interface and all subclasses. + - tgba::succ_iter() now takes only one argument. The optional + global_state and global_automaton arguments have been removed. + - The long unused interface for GreatSPN (or rather, interface to a non-public, customized version of GreatSPN) has been removed. As a consequence, the we could get rid of many cruft in the diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 2cedfc660..6cc9f46ad 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -848,11 +848,10 @@ namespace spot virtual dve2_succ_iterator* - succ_iter(const state* local_state, - const state*, const tgba*) const + succ_iter(const state* st) const { // This may also compute successors in state_condition_last_cc - bdd scond = compute_state_condition(local_state); + bdd scond = compute_state_condition(st); callback_context* cc; if (state_condition_last_cc_) @@ -863,11 +862,11 @@ namespace spot else { int t; - cc = build_cc(get_vars(local_state), t); + cc = build_cc(get_vars(st), t); // Add a self-loop to dead-states if we care about these. if (t == 0 && scond != bddfalse) - cc->transitions.push_back(local_state->clone()); + cc->transitions.push_back(st->clone()); } if (iter_cache_) diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index 990303a19..c0cbe9b7b 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.cc @@ -175,16 +175,12 @@ namespace spot return dict_; } - // FIXME : Change the bddtrue. + // FIXME: Change the bddtrue. kripke_explicit_succ_iterator* - kripke_explicit::succ_iter(const spot::state* local_state, - const spot::state* global_state, - const tgba* global_automaton) const + kripke_explicit::succ_iter(const spot::state* st) const { - const state_kripke* s = down_cast(local_state); + const state_kripke* s = down_cast(st); assert(s); - (void) global_state; - (void) global_automaton; state_kripke* it = const_cast(s); return new kripke_explicit_succ_iterator(it, bddtrue); } diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index a2162d0e2..9bf7d08cc 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -124,9 +124,7 @@ namespace spot /// \brief Allow to get an iterator on the state we passed in /// parameter. kripke_explicit_succ_iterator* - succ_iter(const spot::state* local_state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const spot::state* state) const; /// \brief Get the condition on the state bdd state_condition(const state* s) const; diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 628e7893b..bf99f3017 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -43,8 +43,7 @@ namespace spot } tgba_succ_iterator* - tgta_explicit::succ_iter(const spot::state* state, const spot::state*, - const tgba*) const + tgta_explicit::succ_iter(const spot::state* state) const { return ta_.succ_iter(state); } diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 53f2c8505..efb6bb327 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -46,8 +46,7 @@ namespace spot virtual spot::state* get_init_state() const; virtual tgba_succ_iterator* - succ_iter(const spot::state* local_state, const spot::state* global_state = - 0, const tgba* global_automaton = 0) const; + succ_iter(const spot::state* local_state) const; virtual bdd_dict* get_dict() const; diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index b11f7c6f3..65f46f859 100644 --- a/src/ta/tgtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -57,10 +57,9 @@ namespace spot } tgba_succ_iterator* - tgta_product::succ_iter(const state* local_state, const state*, - const tgba*) const + tgta_product::succ_iter(const state* state) const { - const state_product* s = down_cast (local_state); + const state_product* s = down_cast (state); assert(s); fixed_size_pool* p = const_cast (&pool_); diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 955797026..5f52b559f 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -39,8 +39,7 @@ namespace spot get_init_state() const; virtual tgba_succ_iterator* - succ_iter(const state* local_state, const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* local_state) const; }; /// \brief Iterate over the successors of a product computed on the fly. diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index c99b544a1..f0c16eb02 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -65,14 +65,10 @@ namespace spot } tgba_succ_iterator* - taa_tgba::succ_iter(const spot::state* state, - const spot::state* global_state, - const tgba* global_automaton) const + taa_tgba::succ_iter(const spot::state* state) const { const spot::set_state* s = down_cast(state); assert(s); - (void) global_state; - (void) global_automaton; return new taa_succ_iterator(s->get_state(), all_acceptance_conditions()); } diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 6763fdbcb..75ffe0fd8 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -54,10 +54,7 @@ namespace spot /// TGBA interface. virtual ~taa_tgba(); virtual spot::state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const spot::state* local_state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const spot::state* state) const; virtual bdd_dict* get_dict() const; virtual std::string format_state(const spot::state* state) const = 0; virtual bdd all_acceptance_conditions() const; diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index e9569e4dc..4f3d07f45 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -126,29 +126,8 @@ 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. - /// - /// During synchornized products, additional informations are - /// passed about the entire product and its state. Recall that - /// products can be nested, forming a tree of spot::tgba where - /// most values are computed on demand. \a global_automaton - /// designate the root spot::tgba, and \a global_state its - /// state. This two objects can be used by succ_iter() to - /// restrict the set of successors to compute. - /// - /// \param local_state The state whose successors are to be explored. - /// This pointer is not adopted in any way by \c succ_iter, and - /// it is still the caller's responsability to destroy it when - /// appropriate (this can be done during the lifetime of - /// the iterator). - /// \param global_state In a product, the state of the global - /// product automaton. Otherwise, 0. Like \a locale_state, - /// \a global_state is not adopted by \c succ_iter. - /// \param global_automaton In a product, the global - /// product automaton. Otherwise, 0. virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = nullptr, - const tgba* global_automaton = nullptr) const = 0; + succ_iter(const state* local_state) const = 0; #ifndef SWIG /// \brief Build an iterable over the successors of \a s. diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 8f4ae4626..bf0c70146 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -93,21 +93,11 @@ namespace spot } tgba_succ_iterator_concrete* - tgba_bdd_concrete::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_bdd_concrete::succ_iter(const state* state) const { - const state_bdd* s = down_cast(local_state); + const state_bdd* s = down_cast(state); assert(s); bdd succ_set = data_.relation & s->as_bdd(); - // If we are in a product, inject the local conditions of - // all other automata to limit the number of successors. - if (global_automaton) - { - bdd varused = bdd_support(succ_set); - bdd global_conds = global_automaton->support_conditions(global_state); - succ_set = bdd_appexcomp(succ_set, global_conds, bddop_and, varused); - } // Do not allocate an iterator if we can reuse one. if (iter_cache_) { diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index f631a5b6e..69dc1f8ec 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -62,9 +62,7 @@ namespace spot bdd get_init_bdd() const; virtual tgba_succ_iterator_concrete* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* local_state) const; virtual std::string format_state(const state* state) const; diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 48a97a48d..e21071c4a 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -505,16 +505,11 @@ namespace spot } virtual tgba_explicit_succ_iterator* - succ_iter(const spot::state* state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const + succ_iter(const spot::state* state) const { const State* s = down_cast(state); assert(s); - (void) global_state; - (void) global_automaton; - if (this->iter_cache_) { tgba_explicit_succ_iterator* it = diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index dbd497929..7ab10b56e 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -616,17 +616,15 @@ namespace spot } tgba_succ_iterator* - tgba_kv_complement::succ_iter(const state* local_state, - const state*, - const tgba*) const + tgba_kv_complement::succ_iter(const state* state) const { - const state_kv_complement* state = - down_cast(local_state); - assert(state); + const state_kv_complement* s = + down_cast(state); + assert(s); return new tgba_kv_complement_succ_iterator(automaton_, - the_acceptance_cond_, - acc_list_, state); + the_acceptance_cond_, + acc_list_, s); } bdd_dict* diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh index bdb1e239d..60959c6b7 100644 --- a/src/tgba/tgbakvcomplement.hh +++ b/src/tgba/tgbakvcomplement.hh @@ -91,10 +91,7 @@ namespace spot // tgba interface virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; virtual std::string format_state(const state* state) const; diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index 8557bbc14..cef84d23b 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -139,9 +139,7 @@ namespace spot } tgba_succ_iterator* - tgba_mask::succ_iter(const state* local_state, - const state*, - const tgba*) const + tgba_mask::succ_iter(const state* state) const { succ_iter_filtered* res; if (iter_cache_) @@ -153,9 +151,9 @@ namespace spot { res = new succ_iter_filtered; } - for (auto it: original_->succ(local_state)) + for (auto it: original_->succ(state)) { - const state* s = it->current_state(); + const spot::state* s = it->current_state(); if (!wanted(s)) { s->destroy(); diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh index 3ef8d4ae7..7c29299da 100644 --- a/src/tgba/tgbamask.hh +++ b/src/tgba/tgbamask.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -48,9 +48,7 @@ namespace spot virtual state* get_init_state() const; virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* local_state) const; virtual bool wanted(const state* s) const = 0; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index fd5eedfe2..f22268393 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -374,26 +374,12 @@ namespace spot } tgba_succ_iterator* - tgba_product::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_product::succ_iter(const state* state) const { - const state_product* s = - down_cast(local_state); + const state_product* s = down_cast(state); assert(s); - - // If global_automaton is not specified, THIS is the root of a - // product tree. - if (!global_automaton) - { - global_automaton = this; - global_state = local_state; - } - - tgba_succ_iterator* li = left_->succ_iter(s->left(), - global_state, global_automaton); - tgba_succ_iterator* ri = right_->succ_iter(s->right(), - global_state, global_automaton); + tgba_succ_iterator* li = left_->succ_iter(s->left()); + tgba_succ_iterator* ri = right_->succ_iter(s->right()); if (iter_cache_) { diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 136f403fd..fea330cf1 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -92,9 +92,7 @@ namespace spot virtual state* get_init_state() const; virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc index d6870553d..499fded5c 100644 --- a/src/tgba/tgbaproxy.cc +++ b/src/tgba/tgbaproxy.cc @@ -38,16 +38,14 @@ namespace spot } tgba_succ_iterator* - tgba_proxy::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_proxy::succ_iter(const state* state) const { if (iter_cache_) { original_->release_iter(iter_cache_); iter_cache_ = nullptr; } - return original_->succ_iter(local_state, global_state, global_automaton); + return original_->succ_iter(state); } bdd_dict* diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh index 4176b8d7d..c076cef17 100644 --- a/src/tgba/tgbaproxy.hh +++ b/src/tgba/tgbaproxy.hh @@ -44,9 +44,7 @@ namespace spot virtual state* get_init_state() const; virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 73de3d117..a8d33be36 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1161,13 +1161,10 @@ namespace spot /// @param local_state the state from which we want to compute the successors. /// tgba_succ_iterator* - tgba_safra_complement::succ_iter(const state* local_state, - const state* /* = 0 */, - const tgba* /* = 0 */) const + tgba_safra_complement::succ_iter(const state* state) const { const safra_tree_automaton* a = static_cast(safra_); - const state_complement* s = - down_cast(local_state); + const state_complement* s = down_cast(state); assert(s); safra_tree_automaton::automaton_t::const_iterator tr = a->automaton.find(const_cast(s->get_safra())); diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 0c0c98dc7..ffad857ea 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -55,10 +55,7 @@ namespace spot // tgba interface. virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; virtual std::string format_state(const state* state) const; diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc index 3c3f3e982..662d6d7e7 100644 --- a/src/tgba/tgbascc.cc +++ b/src/tgba/tgbascc.cc @@ -46,16 +46,14 @@ namespace spot } tgba_succ_iterator* - tgba_scc::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_scc::succ_iter(const state* state) const { if (iter_cache_) { aut_->release_iter(iter_cache_); iter_cache_ = nullptr; } - return aut_->succ_iter(local_state, global_state, global_automaton); + return aut_->succ_iter(state); } bdd_dict* diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh index cfe0d171c..28f45f30e 100644 --- a/src/tgba/tgbascc.hh +++ b/src/tgba/tgbascc.hh @@ -57,10 +57,7 @@ namespace spot // tgba. virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; virtual std::string diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index 7feeb0cfc..45b52c117 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -191,17 +191,11 @@ namespace spot } tgba_succ_iterator* - tgba_sgba_proxy::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_sgba_proxy::succ_iter(const state* state) const { - const state_sgba_proxy* s = - down_cast(local_state); + const state_sgba_proxy* s = down_cast(state); assert(s); - - tgba_succ_iterator* it = a_->succ_iter(s->real_state(), - global_state, global_automaton); - + tgba_succ_iterator* it = a_->succ_iter(s->real_state()); return new tgba_sgba_proxy_succ_iterator(it); } diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh index c591b1672..fecb77da2 100644 --- a/src/tgba/tgbasgba.hh +++ b/src/tgba/tgbasgba.hh @@ -42,10 +42,7 @@ namespace spot virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 1df89d561..69685b598 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -498,11 +498,9 @@ namespace spot } tgba_succ_iterator* - tgba_tba_proxy::succ_iter(const state* local_state, - const state*, const tgba*) const + tgba_tba_proxy::succ_iter(const state* st) const { - const state_tba_proxy* s = - down_cast(local_state); + const state_tba_proxy* s = down_cast(st); assert(s); const state* rs = s->real_state(); diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 004139057..ebd5aac92 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -58,10 +58,7 @@ namespace spot virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc index ae6427e84..89409c047 100644 --- a/src/tgba/tgbaunion.cc +++ b/src/tgba/tgbaunion.cc @@ -313,13 +313,9 @@ namespace spot } tgba_succ_iterator_union* - tgba_union::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + tgba_union::succ_iter(const state* st) const { - (void) global_state; - (void) global_automaton; - const state_union* s = down_cast(local_state); + const state_union* s = down_cast(st); assert(s); // Is it the initial state ? tgba_succ_iterator* li; diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh index aacfe6174..fab451928 100644 --- a/src/tgba/tgbaunion.hh +++ b/src/tgba/tgbaunion.hh @@ -124,9 +124,7 @@ namespace spot virtual state* get_init_state() const; virtual tgba_succ_iterator_union* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; + succ_iter(const state* state) const; virtual bdd_dict* get_dict() const; diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 8e85f4ea1..8642dcd9e 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -206,18 +206,16 @@ namespace spot } virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const + succ_iter(const state* st) const { const state_wdba_comp_proxy* s = - down_cast(local_state); + down_cast(st); assert(s); const state* o = s->real_state(); tgba_succ_iterator* it = nullptr; if (o) - it = a_->succ_iter(s->real_state(), global_state, global_automaton); + it = a_->succ_iter(s->real_state()); if (iter_cache_) { tgba_wdba_comp_proxy_succ_iterator* res = @@ -226,8 +224,7 @@ namespace spot iter_cache_ = nullptr; return res; } - return new tgba_wdba_comp_proxy_succ_iterator(it, - the_acceptance_cond_); + return new tgba_wdba_comp_proxy_succ_iterator(it, the_acceptance_cond_); } virtual bdd_dict*