From 0fba428cd9d048faa81f36d239478b62c38ac586 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 Feb 2014 16:34:12 +0100 Subject: [PATCH] tgba: remove the support_variable() method. * src/kripke/fairkripke.cc, src/kripke/fairkripke.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc, 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/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: Remove anything related to support_variables() and compute_support_variables(). * NEWS: Mention it. * src/tgbaalgos/powerset.cc: Adjust the computation of all possible conditions. --- NEWS | 4 ++++ src/kripke/fairkripke.cc | 11 +++-------- src/kripke/fairkripke.hh | 3 +-- src/ta/tgtaexplicit.cc | 11 ++--------- src/ta/tgtaexplicit.hh | 5 ++--- src/tgba/taatgba.cc | 16 ---------------- src/tgba/taatgba.hh | 1 - src/tgba/tgba.cc | 17 ----------------- src/tgba/tgba.hh | 19 ------------------- src/tgba/tgbabddconcrete.cc | 21 --------------------- src/tgba/tgbabddconcrete.hh | 10 +++++----- src/tgba/tgbaexplicit.hh | 18 +----------------- src/tgba/tgbakvcomplement.cc | 9 --------- src/tgba/tgbakvcomplement.hh | 5 ++--- src/tgba/tgbaproduct.cc | 15 --------------- src/tgba/tgbaproduct.hh | 5 ++--- src/tgba/tgbaproxy.cc | 6 ------ src/tgba/tgbaproxy.hh | 7 +++---- src/tgba/tgbasafracomplement.cc | 18 ------------------ src/tgba/tgbasafracomplement.hh | 5 ++--- src/tgba/tgbascc.cc | 6 ------ src/tgba/tgbascc.hh | 5 ++--- src/tgba/tgbasgba.cc | 13 ------------- src/tgba/tgbasgba.hh | 8 ++++---- src/tgba/tgbatba.cc | 12 +----------- src/tgba/tgbatba.hh | 5 ++--- src/tgba/tgbaunion.cc | 14 -------------- src/tgba/tgbaunion.hh | 1 - src/tgba/wdbacomp.cc | 12 ------------ src/tgbaalgos/powerset.cc | 7 +++---- 30 files changed, 39 insertions(+), 250 deletions(-) diff --git a/NEWS b/NEWS index a3393663c..22e7d793e 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,10 @@ New in spot 1.2.3a (not yet released) Where the virtual calls to done() and delete have been avoided. + - tgba::support_variables() and tgba::compute_support_variables() + methods have been removed from the TGBA interface and all + subclasses. + - 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/src/kripke/fairkripke.cc b/src/kripke/fairkripke.cc index 5f59b29f8..10671d494 100644 --- a/src/kripke/fairkripke.cc +++ b/src/kripke/fairkripke.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement -// de l'Epita +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et +// Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -53,10 +54,4 @@ namespace spot return state_condition(s); } - bdd - fair_kripke::compute_support_variables(const state* s) const - { - return bdd_support(state_condition(s)); - } - } diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 59b8d9de6..af6d23917 100644 --- a/src/kripke/fairkripke.hh +++ b/src/kripke/fairkripke.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -101,7 +101,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* s) const; - virtual bdd compute_support_variables(const state* s) const; }; } diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 91d70b430..628e7893b 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -56,14 +57,6 @@ namespace spot return ta_.get_tgba()->support_conditions(s->get_tgba_state()); } - bdd - tgta_explicit::compute_support_variables(const spot::state* in) const - { - const state_ta_explicit* s = down_cast(in); - assert(s); - return ta_.get_tgba()->support_variables(s->get_tgba_state()); - } - bdd_dict* tgta_explicit::get_dict() const { diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 34a66b7b3..53f2c8505 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -64,7 +64,6 @@ namespace spot succ_iter_by_changeset(const spot::state* s, bdd change_set) const; protected: virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; ta_explicit ta_; }; diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 4ea2d75a0..c99b544a1 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -116,22 +116,6 @@ namespace spot return res; } - bdd - taa_tgba::compute_support_variables(const spot::state* s) const - { - const spot::set_state* se = down_cast(s); - assert(se); - const state_set* ss = se->get_state(); - - bdd res = bddtrue; - taa_tgba::state_set::const_iterator i; - taa_tgba::state::const_iterator j; - for (i = ss->begin(); i != ss->end(); ++i) - for (j = (*i)->begin(); j != (*i)->end(); ++j) - res &= bdd_support((*j)->condition); - return res; - } - /*----------. | state_set | `----------*/ diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 50e5e4fba..6763fdbcb 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -65,7 +65,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; typedef std::vector ss_vec; diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 56c5bc9a7..bb9a1ff7d 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -27,7 +27,6 @@ namespace spot tgba::tgba() : iter_cache_(nullptr), last_support_conditions_input_(0), - last_support_variables_input_(0), num_acc_(-1) { } @@ -36,8 +35,6 @@ namespace spot { if (last_support_conditions_input_) last_support_conditions_input_->destroy(); - if (last_support_variables_input_) - last_support_variables_input_->destroy(); delete iter_cache_; } @@ -55,20 +52,6 @@ namespace spot return last_support_conditions_output_; } - bdd - tgba::support_variables(const state* state) const - { - if (!last_support_variables_input_ - || last_support_variables_input_->compare(state) != 0) - { - last_support_variables_output_ = compute_support_variables(state); - if (last_support_variables_input_) - last_support_variables_input_->destroy(); - last_support_variables_input_ = state->clone(); - } - return last_support_variables_output_; - } - state* tgba::project_state(const state* s, const tgba* t) const { diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 3c68652ed..e9569e4dc 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -189,20 +189,6 @@ namespace spot /// last return value for efficiency. bdd support_conditions(const state* state) const; - /// \brief Get the conjunctions of variables tested by - /// the outgoing transitions of \a state. - /// - /// All variables tested by outgoing transitions must be - /// returned. This is mandatory. - /// - /// This is used as an hint by some \c succ_iter() to reduce the - /// number of successor to compute in a product. - /// - /// Sub classes should implement compute_support_variables(), - /// this function is just a wrapper that will cache the - /// last return value for efficiency. - bdd support_variables(const state* state) const; - /// \brief Get the dictionary associated to the automaton. /// /// Atomic propositions and acceptance conditions are represented @@ -280,14 +266,9 @@ namespace spot protected: /// Do the actual computation of tgba::support_conditions(). virtual bdd compute_support_conditions(const state* state) const = 0; - /// Do the actual computation of tgba::support_variables(). - virtual bdd compute_support_variables(const state* state) const = 0; - protected: mutable const state* last_support_conditions_input_; - mutable const state* last_support_variables_input_; private: mutable bdd last_support_conditions_output_; - mutable bdd last_support_variables_output_; mutable int num_acc_; }; diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 1d180a53f..8f4ae4626 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -128,27 +128,6 @@ namespace spot return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set); } - bdd - tgba_bdd_concrete::compute_support_variables(const state* st) const - { - const state_bdd* s = down_cast(st); - assert(s); - bdd succ_set = data_.relation & s->as_bdd(); - // bdd_support must be called BEFORE bdd_exist - // because bdd_exist(bdd_support((a&Next[f])|(!a&Next[g])),Next[*]) - // is obviously not the same as bdd_support(a|!a). - // In other words: we cannot reuse compute_support_conditions() for - // this computation. - // - // Also we need to inject the support of acceptance conditions, because a - // "Next[f]" that looks like one transition might in fact be two - // transitions if the acceptance condition distinguish between - // letters, e.g. "Next[f] & ((a & Acc[1]) | (!a))" - return bdd_exist(bdd_support(succ_set) - & data_.acceptance_conditions_support, - data_.notvar_set); - } - std::string tgba_bdd_concrete::format_state(const state* state) const { diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 4f9334e85..f631a5b6e 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -85,7 +86,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; tgba_bdd_core_data data_; ///< Core data associated to the automaton. bdd init_; ///< Initial state. diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 1eadd08eb..48a97a48d 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -491,10 +491,9 @@ namespace spot } this->dict_->unregister_all_my_variables(this); - // These have already been destroyed by subclasses. + // Thus has already been destroyed by subclasses. // Prevent destroying by tgba::~tgba. this->last_support_conditions_input_ = 0; - this->last_support_variables_input_ = 0; } virtual State* get_init_state() const @@ -682,21 +681,6 @@ namespace spot return res; } - virtual bdd compute_support_variables(const spot::state* in) const - { - const State* s = down_cast(in); - assert(s); - const transitions_t& st = s->successors; - - bdd res = bddtrue; - - typename transitions_t::const_iterator i; - for (i = st.begin(); i != st.end(); ++i) - res &= bdd_support(i->condition); - - return res; - } - ls_map ls_; alias_map alias_; sl_map sl_; diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index c9f953c53..dbd497929 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -685,13 +685,4 @@ namespace spot return result; } - bdd - tgba_kv_complement::compute_support_variables(const state* state) const - { - bdd result = bddtrue; - for (auto i: succ(state)) - result &= bdd_support(i->current_condition()); - return result; - } - } // end namespace spot. diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh index 8a1f429a2..bdb1e239d 100644 --- a/src/tgba/tgbakvcomplement.hh +++ b/src/tgba/tgbakvcomplement.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -102,7 +102,6 @@ namespace spot virtual bdd neg_acceptance_conditions() const; protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; private: /// Retrieve all the atomic acceptance conditions of the automaton. /// They are inserted into \a acc_list_. diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 896570b6e..fd5eedfe2 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -363,11 +363,6 @@ namespace spot last_support_conditions_input_->destroy(); last_support_conditions_input_ = 0; } - if (last_support_variables_input_) - { - last_support_variables_input_->destroy(); - last_support_variables_input_ = 0; - } } state* @@ -430,16 +425,6 @@ namespace spot return lsc & rsc; } - bdd - tgba_product::compute_support_variables(const state* in) const - { - const state_product* s = down_cast(in); - assert(s); - bdd lsc = left_->support_variables(s->left()); - bdd rsc = right_->support_variables(s->right()); - return lsc & rsc; - } - bdd_dict* tgba_product::get_dict() const { diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index d14749ce8..136f403fd 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -110,7 +110,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; protected: bdd_dict* dict_; diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc index 888ca6363..d6870553d 100644 --- a/src/tgba/tgbaproxy.cc +++ b/src/tgba/tgbaproxy.cc @@ -91,11 +91,5 @@ namespace spot { return original_->support_conditions(state); } - - bdd - tgba_proxy::compute_support_variables(const state* state) const - { - return original_->support_variables(state); - } } diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh index 2fcdb5914..4176b8d7d 100644 --- a/src/tgba/tgbaproxy.hh +++ b/src/tgba/tgbaproxy.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -62,8 +63,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; - const tgba* original_; }; } diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 14fd488fd..73de3d117 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1307,24 +1307,6 @@ namespace spot return res; } - bdd - tgba_safra_complement::compute_support_variables(const state* state) const - { - const safra_tree_automaton* a = static_cast(safra_); - const state_complement* s = down_cast(state); - assert(s); - typedef safra_tree_automaton::automaton_t::const_iterator auto_it; - auto_it node(a->automaton.find(const_cast(s->get_safra()))); - - if (node == a->automaton.end()) - return bddtrue; - - bdd res = bddtrue; - for (auto& i: node->second) - res &= bdd_support(i.first); - return res; - } - // display_safra: debug routine. ////////////////////////////// void display_safra(const tgba_safra_complement* a) diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 16ed2f664..0c0c98dc7 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -72,7 +72,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; private: const tgba* automaton_; void* safra_; diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc index 8b7e93fe6..3c3f3e982 100644 --- a/src/tgba/tgbascc.cc +++ b/src/tgba/tgbascc.cc @@ -108,10 +108,4 @@ namespace spot return aut_->support_conditions(state); } - bdd - tgba_scc::compute_support_variables - (const state* state) const - { - return aut_->support_variables(state); - } } diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh index f6b47b174..cfe0d171c 100644 --- a/src/tgba/tgbascc.hh +++ b/src/tgba/tgbascc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013 Laboratoire de recherche et développement -// de l'Epita. +// Copyright (C) 2009, 2013, 2014 Laboratoire de recherche et +// développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -70,7 +70,6 @@ namespace spot virtual bdd neg_acceptance_conditions() const; virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; protected: const tgba* aut_; // The wrapped TGBA. diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index c5b876906..7feeb0cfc 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -264,17 +264,4 @@ namespace spot return acceptance_condition_; return a_->support_conditions(s->real_state()); } - - bdd - tgba_sgba_proxy::compute_support_variables(const state* state) const - { - const state_sgba_proxy* s = - down_cast(state); - assert(s); - - if (emulate_acc_cond_) - return bdd_support(acceptance_condition_); - return a_->support_variables(s->real_state()); - } - } diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh index 665a401c1..c591b1672 100644 --- a/src/tgba/tgbasgba.hh +++ b/src/tgba/tgbasgba.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -27,7 +28,7 @@ namespace spot /// \ingroup tgba_on_the_fly_algorithms /// \brief Change the labeling-mode of spot::tgba on the fly, producing a - /// state-based generalized Büchi automaton. + /// state-based generalized Büchi automaton. /// /// This class acts as a proxy in front of a spot::tgba, that should /// label on states on-the-fly. The result is still a spot::tgba, @@ -57,7 +58,6 @@ namespace spot bdd state_acceptance_conditions(const state* state) const; protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; private: const tgba* a_; diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 803ba77d2..1df89d561 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -471,10 +471,9 @@ namespace spot } delete m; - // These have already been destroyed. + // This has already been destroyed. // Prevent destroying by tgba::~tgba. this->last_support_conditions_input_ = 0; - this->last_support_variables_input_ = 0; } state* @@ -611,15 +610,6 @@ namespace spot return a_->support_conditions(s->real_state()); } - bdd - tgba_tba_proxy::compute_support_variables(const state* state) const - { - const state_tba_proxy* s = - down_cast(state); - assert(s); - return a_->support_variables(s->real_state()); - } - //////////////////////////////////////////////////////////////////////// // tgba_sba_proxy diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index f21cde793..004139057 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita. // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -104,7 +104,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; cycle_list acc_cycle_; const tgba* a_; diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc index d727de92a..ae6427e84 100644 --- a/src/tgba/tgbaunion.cc +++ b/src/tgba/tgbaunion.cc @@ -376,20 +376,6 @@ namespace spot return right_->support_conditions(s->right()); } - bdd - tgba_union::compute_support_variables(const state* in) const - { - const state_union* s = down_cast(in); - assert(s); - if (!s->left() && !s->right()) - return (left_->support_variables(left_->get_init_state()) - & right_->support_variables(right_->get_init_state())); - if (s->left()) - return left_->support_variables(s->left()); - else - return right_->support_variables(s->right()); - } - bdd_dict* tgba_union::get_dict() const { diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh index b520da5bd..aacfe6174 100644 --- a/src/tgba/tgbaunion.hh +++ b/src/tgba/tgbaunion.hh @@ -139,7 +139,6 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; private: bdd_dict* dict_; diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 7a23d363c..8e85f4ea1 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -280,18 +280,6 @@ namespace spot return bddtrue; } - virtual bdd compute_support_variables(const state* ostate) const - { - const state_wdba_comp_proxy* s = - down_cast(ostate); - assert(s); - const state* rs = s->real_state(); - if (rs) - return a_->support_variables(rs); - else - return bddtrue; - } - const tgba* a_; private: bdd the_acceptance_cond_; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 214d3db90..75cace0bc 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -70,13 +70,12 @@ namespace spot todo.pop_front(); // Compute all variables occurring on outgoing arcs. bdd all_vars = bddtrue; - power_state::const_iterator i; - for (auto s: src) - all_vars &= aut->support_variables(s); + for (auto i: aut->succ(s)) + all_vars &= bdd_support(i->current_condition()); - // Compute all possible combinations of these variables. bdd all_conds = bddtrue; + // Iterate over all possible conditions while (all_conds != bddfalse) { bdd cond = bdd_satoneset(all_conds, all_vars, bddtrue);