From a3e0c8624e9e4b1e0ad8383ed63df7e0f2df8ad0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Feb 2016 10:45:05 +0100 Subject: [PATCH] remove twa::compute_support_conditions Fixes #148. * spot/twa/twa.hh, spot/twa/twa.cc, spot/kripke/fairkripke.hh, spot/kripke/fairkripke.cc, spot/ta/tgtaexplicit.hh, spot/ta/tgtaexplicit.cc, spot/twa/twagraph.hh, spot/twa/twaproduct.hh, spot/twa/twaproduct.cc, spot/twaalgos/stutter.cc, spot/twa/taatgba.hh, spot/twa/taatgba.cc: Remove the method. * spot/taalgos/tgba2ta.cc: Emulate it with a simple loop. * NEWS: Mention the removal. --- NEWS | 3 ++- spot/kripke/fairkripke.cc | 9 +-------- spot/kripke/fairkripke.hh | 3 --- spot/ta/tgtaexplicit.cc | 12 ++---------- spot/ta/tgtaexplicit.hh | 6 ++---- spot/taalgos/tgba2ta.cc | 8 +++++++- spot/twa/taatgba.cc | 16 ---------------- spot/twa/taatgba.hh | 2 -- spot/twa/twa.cc | 19 +------------------ spot/twa/twa.hh | 20 -------------------- spot/twa/twagraph.hh | 11 ----------- spot/twa/twaproduct.cc | 17 ----------------- spot/twa/twaproduct.hh | 3 --- spot/twaalgos/stutter.cc | 6 ------ 14 files changed, 15 insertions(+), 120 deletions(-) diff --git a/NEWS b/NEWS index 62148aec3..871325fad 100644 --- a/NEWS +++ b/NEWS @@ -82,7 +82,8 @@ New in spot 1.99.7a (not yet released) * The twa_safra_complement class has been removed. Use tgba_determinize() and dtwa_complement() instead. - * The twa::transition_annotation() method has been removed. + * The twa::transition_annotation() and + twa::compute_support_conditions() methods have been removed. Python: diff --git a/spot/kripke/fairkripke.cc b/spot/kripke/fairkripke.cc index 69d409417..5d8c059cc 100644 --- a/spot/kripke/fairkripke.cc +++ b/spot/kripke/fairkripke.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -47,11 +47,4 @@ namespace spot // this function on a state without successor. return acc_cond_; } - - bdd - fair_kripke::compute_support_conditions(const state* s) const - { - return state_condition(s); - } - } diff --git a/spot/kripke/fairkripke.hh b/spot/kripke/fairkripke.hh index 0542d6bea..090709214 100644 --- a/spot/kripke/fairkripke.hh +++ b/spot/kripke/fairkripke.hh @@ -100,8 +100,5 @@ namespace spot /// \brief The set of acceptance conditions that label the state \a s. virtual acc_cond::mark_t state_acceptance_conditions(const state* s) const = 0; - - protected: - virtual bdd compute_support_conditions(const state* s) const; }; } diff --git a/spot/ta/tgtaexplicit.cc b/spot/ta/tgtaexplicit.cc index 110f4e109..32861d1a2 100644 --- a/spot/ta/tgtaexplicit.cc +++ b/spot/ta/tgtaexplicit.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de +// Recherche et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -44,14 +44,6 @@ namespace spot return ta_->succ_iter(state); } - bdd - tgta_explicit::compute_support_conditions(const spot::state* in) const - { - const state_ta_explicit* s = down_cast(in); - assert(s); - return ta_->get_tgba()->support_conditions(s->get_tgba_state()); - } - bdd_dict_ptr tgta_explicit::get_dict() const { diff --git a/spot/ta/tgtaexplicit.hh b/spot/ta/tgtaexplicit.hh index 7665708c5..52a285dfc 100644 --- a/spot/ta/tgtaexplicit.hh +++ b/spot/ta/tgtaexplicit.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -58,8 +58,6 @@ namespace spot 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; - ta_explicit_ptr ta_; }; diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index 1d98e93de..48d30fb14 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -413,7 +413,13 @@ namespace spot // build Initial states set: auto tgba_init_state = tgba_->get_init_state(); - bdd tgba_condition = tgba_->support_conditions(tgba_init_state); + bdd tgba_condition = [&]() + { + bdd cond = bddfalse; + for (auto i: tgba_->succ(tgba_init_state)) + cond |= i->cond(); + return cond; + }(); bool is_acc = false; if (degeneralized) diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc index 3cfd38c29..8b72d6be6 100644 --- a/spot/twa/taatgba.cc +++ b/spot/twa/taatgba.cc @@ -66,22 +66,6 @@ namespace spot return new taa_succ_iterator(s->get_state(), acc()); } - bdd - taa_tgba::compute_support_conditions(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 |= (*j)->condition; - return res; - } - /*----------. | state_set | `----------*/ diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index 2139009d2..949b36e40 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -58,8 +58,6 @@ namespace spot virtual std::string format_state(const spot::state* state) const = 0; protected: - virtual bdd compute_support_conditions(const spot::state* state) - const final; typedef std::vector ss_vec; diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index bcf3f85fa..7ee84aea3 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -30,8 +30,7 @@ namespace spot { twa::twa(const bdd_dict_ptr& d) : iter_cache_(nullptr), - dict_(d), - last_support_conditions_input_(nullptr) + dict_(d) { props = 0U; bddaps_ = bddtrue; @@ -39,27 +38,11 @@ namespace spot twa::~twa() { - if (last_support_conditions_input_) - last_support_conditions_input_->destroy(); delete iter_cache_; release_named_properties(); get_dict()->unregister_all_my_variables(this); } - bdd - twa::support_conditions(const state* state) const - { - if (!last_support_conditions_input_ - || last_support_conditions_input_->compare(state) != 0) - { - last_support_conditions_output_ = compute_support_conditions(state); - if (last_support_conditions_input_) - last_support_conditions_input_->destroy(); - last_support_conditions_input_ = state->clone(); - } - return last_support_conditions_output_; - } - state* twa::project_state(const state* s, const const_twa_ptr& t) const diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 900bb0126..982196ed0 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -687,21 +687,6 @@ namespace spot iter_cache_ = i; } - /// \brief Get a formula that must hold whatever successor is taken. - /// - /// \return A formula which must be verified for all successors - /// of \a state. - /// - /// This can be as simple as \c bddtrue, or more precisely - /// the disjunction of the condition of all successors. This - /// is used as an hint by \c succ_iter() to reduce the number - /// of successor to compute in a product. - /// - /// Sub classes should implement compute_support_conditions(), - /// this function is just a wrapper that will cache the - /// last return value for efficiency. - bdd support_conditions(const state* state) const; - /// \brief Get the dictionary associated to the automaton. /// /// Automata are labeled by Boolean formulas over atomic @@ -901,12 +886,7 @@ namespace spot return acc_.mark(0); } - protected: - /// Do the actual computation of tgba::support_conditions(). - virtual bdd compute_support_conditions(const state* state) const = 0; - mutable const state* last_support_conditions_input_; private: - mutable bdd last_support_conditions_output_; std::vector aps_; bdd bddaps_; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 3df6fdfd3..21e139763 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -202,9 +202,6 @@ namespace spot virtual ~twa_graph() { - // Prevent this state from being destroyed by ~twa(), - // as the state will be destroyed when g_ is destroyed. - last_support_conditions_input_ = nullptr; } #ifndef SWIG @@ -425,14 +422,6 @@ namespace spot SPOT_RETURN(g_.is_dead_edge(t)); #endif - virtual bdd compute_support_conditions(const state* s) const - { - bdd sum = bddfalse; - for (auto& t: out(state_number(s))) - sum |= t.cond; - return sum; - } - /// Iterate over all edges, and merge those with compatible /// extremities and acceptance. void merge_edges(); diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 09df23a21..94af3c309 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -318,13 +318,6 @@ namespace spot twa_product::~twa_product() { - // Prevent these states from being destroyed by ~tgba(): they - // will be destroyed before when the pool is destructed. - if (last_support_conditions_input_) - { - last_support_conditions_input_->destroy(); - last_support_conditions_input_ = nullptr; - } } const state* @@ -359,16 +352,6 @@ namespace spot return new twa_succ_iterator_product(li, ri, this, p); } - bdd - twa_product::compute_support_conditions(const state* in) const - { - const state_product* s = down_cast(in); - assert(s); - bdd lsc = left_->support_conditions(s->left()); - bdd rsc = right_->support_conditions(s->right()); - return lsc & rsc; - } - const acc_cond& twa_product::left_acc() const { return left_->acc(); diff --git a/spot/twa/twaproduct.hh b/spot/twa/twaproduct.hh index 6ec28040e..59dc188ab 100644 --- a/spot/twa/twaproduct.hh +++ b/spot/twa/twaproduct.hh @@ -102,9 +102,6 @@ namespace spot const acc_cond& left_acc() const; const acc_cond& right_acc() const; - protected: - virtual bdd compute_support_conditions(const state* state) const; - protected: const_twa_ptr left_; const_twa_ptr right_; diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 8b03e79c4..654b46c35 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -236,12 +236,6 @@ namespace spot + bdd_format_formula(a_->get_dict(), s->cond())); } - protected: - virtual bdd compute_support_conditions(const state*) const override - { - return bddtrue; - } - private: const_twa_ptr a_; bdd aps_;