From 06c69f88ffe7a0e11da0fc1f3087b140432f05f1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 26 Jan 2014 15:26:09 +0100 Subject: [PATCH] Introduce tgba::release_iter(). Instead of "delete iter;" we now do "aut->release_iter(iter);" to give the iterator back to the automaton. The TGBA classes now reuse a previously returned tgba_succ_iterator to answer a succ_iter() call, therefore avoiding (1) memory allocation, as well as (2) vtable and other constant member initialization. * src/tgba/tgba.hh, src/tgba/tgba.cc (release_iter, iter_cache_): Implement a release_iter() that stores the released iterator in iter_cache_. * src/tgba/succiter.hh (internal::succ_iterable): Move... * src/tgba/tgba.hh (tgba::succ_iterable): ... here. And use release_iter(). * iface/dve2/dve2.cc, src/kripke/kripke.cc, src/kripke/kripke.hh, src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbamask.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbaproxy.cc, src/tgba/tgbascc.cc, src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc, src/tgbaalgos/bfssteps.cc, src/tgbaalgos/compsusp.cc, src/tgbaalgos/cycles.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/reachiter.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Use release_iter() instead of deleting iterators, and used recycle iter_cache_ in implementations of tgba::succ_iter(). --- iface/dve2/dve2.cc | 27 ++++++++++-- src/kripke/kripke.cc | 9 ++-- src/kripke/kripke.hh | 13 +++++- src/tgba/succiter.hh | 32 +------------- src/tgba/succiterconcrete.cc | 14 ++----- src/tgba/succiterconcrete.hh | 16 ++++++- src/tgba/taatgba.hh | 2 +- src/tgba/tgba.cc | 9 ++-- src/tgba/tgba.hh | 56 ++++++++++++++++++++++++- src/tgba/tgbabddconcrete.cc | 16 +++++-- src/tgba/tgbaexplicit.hh | 18 +++++++- src/tgba/tgbamask.cc | 11 ++++- src/tgba/tgbaproduct.cc | 27 ++++++++++-- src/tgba/tgbaproxy.cc | 8 +++- src/tgba/tgbascc.cc | 7 +++- src/tgba/tgbatba.cc | 44 +++++++++++++------- src/tgba/tgbaunion.cc | 78 ++++++++++++++++++++--------------- src/tgba/tgbaunion.hh | 5 ++- src/tgba/wdbacomp.cc | 20 +++++++-- src/tgbaalgos/bfssteps.cc | 6 +-- src/tgbaalgos/compsusp.cc | 3 +- src/tgbaalgos/cycles.cc | 4 +- src/tgbaalgos/dtbasat.cc | 14 ++----- src/tgbaalgos/dtgbasat.cc | 10 +---- src/tgbaalgos/gtec/gtec.cc | 21 +++++----- src/tgbaalgos/gv04.cc | 8 ++-- src/tgbaalgos/isweakscc.cc | 26 +++++------- src/tgbaalgos/lbtt.cc | 10 ++--- src/tgbaalgos/ltl2tgba_fm.cc | 18 ++++---- src/tgbaalgos/magic.cc | 10 ++--- src/tgbaalgos/ndfs_result.hxx | 16 +++---- src/tgbaalgos/neverclaim.cc | 17 ++++---- src/tgbaalgos/reachiter.cc | 11 ++--- src/tgbaalgos/replayrun.cc | 8 ++-- src/tgbaalgos/safety.cc | 2 +- src/tgbaalgos/scc.cc | 6 +-- src/tgbaalgos/se05.cc | 10 ++--- src/tgbaalgos/simulation.cc | 6 +-- src/tgbaalgos/tau03.cc | 6 +-- src/tgbaalgos/tau03opt.cc | 10 ++--- 40 files changed, 386 insertions(+), 248 deletions(-) diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index f323e76eb..42958fee5 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -214,9 +214,8 @@ namespace spot ~callback_context() { - callback_context::transitions_t::const_iterator it; - for (it = transitions.begin(); it != transitions.end(); ++it) - (*it)->destroy(); + for (auto t: transitions) + t->destroy(); } }; @@ -260,6 +259,13 @@ namespace spot { } + void recycle(const callback_context* cc, bdd cond) + { + delete cc_; + cc_ = cc; + kripke_succ_iterator::recycle(cond); + } + ~dve2_succ_iterator() { delete cc_; @@ -661,6 +667,11 @@ namespace spot ~dve2_kripke() { + if (iter_cache_) + { + delete iter_cache_; + iter_cache_ = nullptr; + } delete[] format_filter_; delete[] vname_; if (compress_) @@ -857,6 +868,14 @@ namespace spot cc->transitions.push_back(local_state->clone()); } + if (iter_cache_) + { + dve2_succ_iterator* it = + down_cast(iter_cache_); + it->recycle(cc, scond); + iter_cache_ = nullptr; + return it; + } return new dve2_succ_iterator(cc, scond); } diff --git a/src/kripke/kripke.cc b/src/kripke/kripke.cc index 0be019031..1dd937cf3 100644 --- a/src/kripke/kripke.cc +++ b/src/kripke/kripke.cc @@ -1,4 +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. // @@ -20,11 +22,6 @@ namespace spot { - kripke_succ_iterator::kripke_succ_iterator(const bdd& cond) - : cond_(cond) - { - } - kripke_succ_iterator::~kripke_succ_iterator() { } diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh index 608b50891..066e0dedd 100644 --- a/src/kripke/kripke.hh +++ b/src/kripke/kripke.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. @@ -48,7 +48,16 @@ namespace spot /// /// The \a cond argument will be the one returned /// by kripke_succ_iterator::current_condition(). - kripke_succ_iterator(const bdd& cond); + kripke_succ_iterator(const bdd& cond) + : cond_(cond) + { + } + + void recycle(const bdd& cond) + { + cond_ = cond; + } + virtual ~kripke_succ_iterator(); virtual bdd current_condition() const; diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index ff29aa157..94030f295 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -27,6 +27,8 @@ namespace spot { + class tgba; + /// \ingroup tgba_essentials /// \brief Iterate over the successors of a state. /// @@ -100,8 +102,6 @@ namespace spot //@} }; - class tgba; - namespace internal { struct SPOT_API succ_iterator @@ -137,34 +137,6 @@ namespace spot it_ = nullptr; } }; - - class SPOT_API succ_iterable - { - protected: - const tgba* aut_; - tgba_succ_iterator* it_; - public: - succ_iterable(const tgba* aut, tgba_succ_iterator* it) - : aut_(aut), it_(it) - { - } - - ~succ_iterable() - { - delete it_; - } - - succ_iterator begin() - { - it_->first(); - return it_->done() ? nullptr : it_; - } - - succ_iterator end() - { - return nullptr; - } - }; } } diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 7c27e655c..58b4b84f0 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -24,15 +25,6 @@ namespace spot { - tgba_succ_iterator_concrete::tgba_succ_iterator_concrete - (const tgba_bdd_core_data& d, bdd successors) - : data_(d), - succ_set_(successors), - succ_set_left_(successors), - current_(bddfalse) - { - } - tgba_succ_iterator_concrete::~tgba_succ_iterator_concrete() { } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 7b1a8b08f..f69bd6d35 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -45,7 +45,19 @@ namespace spot /// \param d The core data of the automata. /// These contains sets of variables useful to split a BDD, and /// compute acceptance conditions. - tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors); + tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors) + : data_(d) + { + recycle(successors); + } + + void recycle(bdd successors) + { + succ_set_ = successors; + succ_set_left_ = successors; + current_ = bddfalse; + } + virtual ~tgba_succ_iterator_concrete(); // iteration diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index cea12ab05..66dbeb464 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 264fe426c..56c5bc9a7 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -24,7 +25,8 @@ namespace spot { tgba::tgba() - : last_support_conditions_input_(0), + : iter_cache_(nullptr), + last_support_conditions_input_(0), last_support_variables_input_(0), num_acc_(-1) { @@ -36,6 +38,7 @@ namespace spot last_support_conditions_input_->destroy(); if (last_support_variables_input_) last_support_variables_input_->destroy(); + delete iter_cache_; } bdd diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 2640587a7..b419382a1 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -71,8 +71,48 @@ namespace spot { protected: tgba(); + // Any iterator returned via release_iter. + mutable tgba_succ_iterator* iter_cache_; public: + +#ifndef SWIG + class succ_iterable + { + protected: + const tgba* aut_; + tgba_succ_iterator* it_; + public: + succ_iterable(const tgba* aut, tgba_succ_iterator* it) + : aut_(aut), it_(it) + { + } + + succ_iterable(succ_iterable&& other) + : aut_(other.aut_), it_(other.it_) + { + other.it_ = nullptr; + } + + ~succ_iterable() + { + if (it_) + aut_->release_iter(it_); + } + + internal::succ_iterator begin() + { + it_->first(); + return it_->done() ? nullptr : it_; + } + + internal::succ_iterator end() + { + return nullptr; + } + }; +#endif + virtual ~tgba(); /// \brief Get the initial state of the automaton. @@ -111,15 +151,29 @@ namespace spot const state* global_state = nullptr, const tgba* global_automaton = nullptr) const = 0; +#ifndef SWIG /// \brief Build an iterable over the successors of \a s. /// /// This is meant to be used as /// for (auto i: aut->out(s)) { /* i->current_state() */ }. - internal::succ_iterable + succ_iterable succ(const state* s) const { return {this, succ_iter(s)}; } +#endif + + /// \brief Release an iterator after usage. + /// + /// This iterator can then be reused by succ_iter() to avoid + /// memory allocation. + void release_iter(tgba_succ_iterator* i) const + { + if (iter_cache_) + delete i; + else + iter_cache_ = i; + } /// \brief Get a formula that must hold whatever successor is taken. /// diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index a8aa096c2..1d180a53f 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -107,6 +108,15 @@ namespace spot 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_) + { + tgba_succ_iterator_concrete* res = + down_cast(iter_cache_); + iter_cache_ = nullptr; + res->recycle(succ_set); + return res; + } return new tgba_succ_iterator_concrete(data_, succ_set); } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index d15e59b06..bfa82230b 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita. +// Copyright (C) 2009, 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. @@ -202,6 +202,12 @@ namespace spot { } + void recycle(const State* start, bdd all_acc) + { + start_ = start; + all_acceptance_conditions_ = all_acc; + } + virtual void first() { it_ = start_->successors.begin(); @@ -508,6 +514,14 @@ namespace spot (void) global_state; (void) global_automaton; + if (this->iter_cache_) + { + tgba_explicit_succ_iterator* it = + down_cast*>(this->iter_cache_); + it->recycle(s, this->all_acceptance_conditions()); + this->iter_cache_ = nullptr; + return it; + } return new tgba_explicit_succ_iterator(s, this diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index 26844b934..23bfc24f8 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -141,7 +141,16 @@ namespace spot const state*, const tgba*) const { - succ_iter_filtered* res = new succ_iter_filtered; + succ_iter_filtered* res; + if (iter_cache_) + { + res = down_cast(iter_cache_); + iter_cache_ = nullptr; + } + else + { + res = new succ_iter_filtered; + } for (auto it: original_->succ(local_state)) { const state* s = it->current_state(); diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 28641feb0..073a792be 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012, 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. +// Paris 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. // @@ -88,6 +89,15 @@ namespace spot { } + void recycle(const tgba* l, tgba_succ_iterator* left, + const tgba* r, tgba_succ_iterator* right) + { + l->release_iter(left_); + left_ = left; + r->release_iter(right_); + right_ = right; + } + virtual ~tgba_succ_iterator_product_common() { delete left_; @@ -390,6 +400,15 @@ namespace spot tgba_succ_iterator* ri = right_->succ_iter(s->right(), global_state, global_automaton); + if (iter_cache_) + { + tgba_succ_iterator_product_common* it = + down_cast(iter_cache_); + it->recycle(left_, li, right_, ri); + iter_cache_ = nullptr; + return it; + } + fixed_size_pool* p = const_cast(&pool_); if (left_kripke_) return new tgba_succ_iterator_product_kripke(li, ri, p); diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc index c9360784a..888ca6363 100644 --- a/src/tgba/tgbaproxy.cc +++ b/src/tgba/tgbaproxy.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2013 Laboratoire de Recherche et +// -*- 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. @@ -41,6 +42,11 @@ namespace spot const state* global_state, const tgba* global_automaton) const { + if (iter_cache_) + { + original_->release_iter(iter_cache_); + iter_cache_ = nullptr; + } return original_->succ_iter(local_state, global_state, global_automaton); } diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc index fd3d821fa..8b7e93fe6 100644 --- a/src/tgba/tgbascc.cc +++ b/src/tgba/tgbascc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013 Laboratoire de recherche et +// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de recherche et // développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -50,6 +50,11 @@ namespace spot const state* global_state, const tgba* global_automaton) const { + if (iter_cache_) + { + aut_->release_iter(iter_cache_); + iter_cache_ = nullptr; + } return aut_->succ_iter(local_state, global_state, global_automaton); } diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 201ae93f5..89660b031 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -170,14 +170,29 @@ namespace spot typedef tgba_tba_proxy::cycle_list::const_iterator iterator; public: tgba_tba_proxy_succ_iterator(const state* rs, - tgba_succ_iterator* it, + tgba::succ_iterable&& iterable, iterator expected, const list& cycle, bdd the_acceptance_cond, const tgba_tba_proxy* aut) : the_acceptance_cond_(the_acceptance_cond) { - for (it->first(); !it->done(); it->next()) + recycle(rs, std::move(iterable), expected, cycle, aut); + } + + void recycle(const state* rs, + tgba::succ_iterable&& iterable, + iterator expected, + const list& cycle, + const tgba_tba_proxy* aut) + { + if (!transmap_.empty()) + { + translist_.clear(); + transmap_.clear(); + } + + for (auto it: iterable) { bool accepting; bdd acc = it->current_acceptance_conditions(); @@ -324,20 +339,11 @@ namespace spot dest->destroy(); } } - delete it; } virtual ~tgba_tba_proxy_succ_iterator() { - for (transmap_t::const_iterator i = transmap_.begin(); - i != transmap_.end();) - { - const state* d = i->first.first; - // Advance i before deleting d. - ++i; - d->destroy(); - } } // iteration @@ -492,17 +498,23 @@ namespace spot tgba_succ_iterator* tgba_tba_proxy::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + const state*, const tgba*) const { const state_tba_proxy* s = down_cast(local_state); assert(s); - const state* rs = s->real_state(); - tgba_succ_iterator* it = a_->succ_iter(rs, global_state, global_automaton); - return new tgba_tba_proxy_succ_iterator(rs, it, + if (iter_cache_) + { + tgba_tba_proxy_succ_iterator* res = + down_cast(iter_cache_); + res->recycle(rs, a_->succ(rs), + s->acceptance_iterator(), acc_cycle_, this); + iter_cache_ = nullptr; + return res; + } + return new tgba_tba_proxy_succ_iterator(rs, a_->succ(rs), s->acceptance_iterator(), acc_cycle_, the_acceptance_cond_, this); diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc index c1597462e..a8cf690c9 100644 --- a/src/tgba/tgbaunion.cc +++ b/src/tgba/tgbaunion.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -94,6 +95,16 @@ namespace spot { } + void + tgba_succ_iterator_union::recycle(const tgba* l, tgba_succ_iterator* left, + const tgba* r, tgba_succ_iterator* right) + { + l->release_iter(left_); + left_ = left; + r->release_iter(right_); + right_ = right; + } + tgba_succ_iterator_union::~tgba_succ_iterator_union() { delete left_; @@ -278,44 +289,45 @@ namespace spot (void) global_automaton; const state_union* s = down_cast(local_state); assert(s); - tgba_succ_iterator_union* res = 0; // Is it the initial state ? + tgba_succ_iterator* li; + tgba_succ_iterator* ri; if (!s->left() && !s->right()) - { - // Yes, create an iterator with both initial states. - state* left_init = left_->get_init_state(); - state* right_init = right_->get_init_state(); - tgba_succ_iterator* li = left_->succ_iter(left_init); - tgba_succ_iterator* ri = right_->succ_iter(right_init); - res = new tgba_succ_iterator_union(li, ri, left_acc_missing_, - right_acc_missing_, - left_var_missing_, - right_var_missing_); - left_init->destroy(); - right_init->destroy(); - } + { + // Yes, create an iterator with both initial states. + state* left_init = left_->get_init_state(); + state* right_init = right_->get_init_state(); + li = left_->succ_iter(left_init); + ri = right_->succ_iter(right_init); + left_init->destroy(); + right_init->destroy(); + } + // No, create an iterator based on the corresponding state + // in the left or in the right automaton. + else if (s->left()) + { + li = left_->succ_iter(s->left()); + ri = nullptr; + } else - { - // No, create an iterator based on the corresponding state - // in the left or in the right automaton. - if (s->left()) { - tgba_succ_iterator* li = left_->succ_iter(s->left()); - res = new tgba_succ_iterator_union(li, 0, left_acc_missing_, - right_acc_missing_, - left_var_missing_, - right_var_missing_); + li = nullptr; + ri = right_->succ_iter(s->right()); } - else + + if (iter_cache_) { - tgba_succ_iterator* ri = right_->succ_iter(s->right()); - res = new tgba_succ_iterator_union(0, ri, left_acc_missing_, - right_acc_missing_, - left_var_missing_, - right_var_missing_); + tgba_succ_iterator_union* res = + down_cast(iter_cache_); + res->recycle(left_, li, right_, ri); + iter_cache_ = nullptr; + return res; } - } - return res; + return new tgba_succ_iterator_union(li, ri, + left_acc_missing_, + right_acc_missing_, + left_var_missing_, + right_var_missing_); } bdd diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh index cf7ca5fee..3e9a5f15c 100644 --- a/src/tgba/tgbaunion.hh +++ b/src/tgba/tgbaunion.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -84,6 +84,9 @@ namespace spot bdd left_missing, bdd right_missing, bdd left_var, bdd right_var); + void recycle(const tgba* l, tgba_succ_iterator* left, + const tgba* r, tgba_succ_iterator* right); + virtual ~tgba_succ_iterator_union(); // iteration diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 3d0e72c65..30c54dc48 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -95,6 +95,12 @@ namespace spot { } + void recycle(const tgba* a, tgba_succ_iterator* it) + { + a->release_iter(it_); + it_ = it; + } + virtual ~tgba_wdba_comp_proxy_succ_iterator() { @@ -197,9 +203,17 @@ namespace spot assert(s); const state* o = s->real_state(); - tgba_succ_iterator* it = 0; + 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(), global_state, global_automaton); + if (iter_cache_) + { + tgba_wdba_comp_proxy_succ_iterator* res = + down_cast(iter_cache_); + res->recycle(a_, it); + iter_cache_ = nullptr; + return res; + } return new tgba_wdba_comp_proxy_succ_iterator(it, the_acceptance_cond_); } diff --git a/src/tgbaalgos/bfssteps.cc b/src/tgbaalgos/bfssteps.cc index 0a5504f40..3ca065434 100644 --- a/src/tgbaalgos/bfssteps.cc +++ b/src/tgbaalgos/bfssteps.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2014 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -88,7 +88,7 @@ namespace spot { // Found it! finalize(father, s, start, l); - delete i; + a_->release_iter(i); return dest; } @@ -100,7 +100,7 @@ namespace spot father[dest] = s; } } - delete i; + a_->release_iter(i); } return 0; } diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index d52dea40b..4f6bd839f 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -339,7 +339,8 @@ namespace spot else break; } - delete ri; + if (ri) + right->release_iter(ri); } } delete left; diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index e67a66b26..ba2e937a9 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -136,7 +136,7 @@ namespace spot // No more successors. bool f = cur.f; tagged_state v = cur.ts; - delete cur.succ; + aut_->release_iter(cur.succ); dfs_.pop_back(); if (f) @@ -158,7 +158,7 @@ namespace spot // returned false. while (!dfs_.empty()) { - delete dfs_.back().succ; + aut_->release_iter(dfs_.back().succ); dfs_.pop_back(); } diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 5ae9b9eae..95303447d 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -438,8 +438,7 @@ namespace spot dout << "(3) augmenting paths based on Cand[" << q1 << "] and Ref[" << q1p << "]\n"; - tgba_succ_iterator* it = ref->succ_iter(d.int_to_state[q1p]); - for (it->first(); !it->done(); it->next()) + for (auto it: ref->succ(d.int_to_state[q1p])) { const state* dps = it->current_state(); int dp = d.state_to_int[dps]; @@ -469,7 +468,6 @@ namespace spot } } } - delete it; } bdd all_acc = ref->all_acceptance_conditions(); @@ -502,9 +500,7 @@ namespace spot else pid1 = d.pathid_ref[p1]; - tgba_succ_iterator* it = - ref->succ_iter(d.int_to_state[q2p]); - for (it->first(); !it->done(); it->next()) + for (auto it: ref->succ(d.int_to_state[q2p])) { const state* dps = it->current_state(); // Skip destinations not in the SCC. @@ -567,7 +563,6 @@ namespace spot } } } - delete it; } } } @@ -598,9 +593,7 @@ namespace spot else pid1 = d.pathid_cand[p1]; - tgba_succ_iterator* it = - ref->succ_iter(d.int_to_state[q2p]); - for (it->first(); !it->done(); it->next()) + for (auto it: ref->succ(d.int_to_state[q2p])) { const state* dps = it->current_state(); // Skip destinations not in the SCC. @@ -665,7 +658,6 @@ namespace spot } } } - delete it; } } } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 4b1b67224..f0aca39e2 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -582,8 +582,7 @@ namespace spot path p1(q1, q1p); int p1id = d.pathid[p1]; - tgba_succ_iterator* it = ref->succ_iter(d.int_to_state[q1p]); - for (it->first(); !it->done(); it->next()) + for (auto it: ref->succ(d.int_to_state[q1p])) { const state* dps = it->current_state(); int dp = d.state_to_int[dps]; @@ -612,7 +611,6 @@ namespace spot } } } - delete it; } bdd all_acc = ref->all_acceptance_conditions(); @@ -645,10 +643,7 @@ namespace spot int pid = d.pathid[p]; - tgba_succ_iterator* it = - ref->succ_iter(d.int_to_state[q2p]); - - for (it->first(); !it->done(); it->next()) + for (auto it: ref->succ(d.int_to_state[q2p])) { const state* dps = it->current_state(); // Skip destinations not in the SCC. @@ -836,7 +831,6 @@ namespace spot } } } - delete it; } } } diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 0b8621af7..03e44f6cf 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2011, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Paris 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. // @@ -135,7 +136,7 @@ namespace spot to_remove.push(ecs_->aut->succ_iter(spi.first)); } } - delete i; + ecs_->aut->release_iter(i); if (to_remove.empty()) break; i = to_remove.top(); @@ -212,8 +213,7 @@ namespace spot remove_component(curr); ecs_->root.pop(); } - - delete succ; + ecs_->aut->release_iter(succ); // Do not destroy CURR: it is a key in H. continue; } @@ -288,7 +288,7 @@ namespace spot // Release all iterators in TODO. while (!todo.empty()) { - delete todo.top().second; + ecs_->aut->release_iter(todo.top().second); todo.pop(); dec_depth(); } @@ -325,14 +325,13 @@ namespace spot couvreur99_check_shy* shy) : s(s), n(n) { - tgba_succ_iterator* iter = shy->ecs_->aut->succ_iter(s); - for (iter->first(); !iter->done(); iter->next(), shy->inc_transitions()) + for (auto iter: shy->ecs_->aut->succ(s)) { q.push_back(successor(iter->current_acceptance_conditions(), iter->current_state())); shy->inc_depth(); + shy->inc_transitions(); } - delete iter; } couvreur99_check_shy::couvreur99_check_shy(const tgba* a, diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 1eac8722c..245944cb6 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013 Laboratoire de recherche et -// développement de l'Epita (LRDE). +// Copyright (C) 2008, 2010, 2011, 2013, 2014 Laboratoire de recherche +// et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -80,7 +80,7 @@ namespace spot ~gv04() { for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i) - delete i->lasttr; + a_->release_iter(i->lasttr); hash_type::const_iterator s = h.begin(); while (s != h.end()) { @@ -203,7 +203,7 @@ namespace spot assert(static_cast(top + 1) == stack.size()); for (int i = top; i >= dftop; --i) { - delete stack[i].lasttr; + a_->release_iter(stack[i].lasttr); stack.pop_back(); dec_depth(); } diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 7c1b09c1e..72358270b 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -96,12 +97,10 @@ namespace spot if (!aut) return false; - const std::list states = map.states_of(scc); - std::list::const_iterator it; - for (it = states.begin(); it != states.end(); ++it) + for (auto ss: map.states_of(scc)) { const state_explicit_formula* s = - down_cast(*it); + down_cast(ss); assert(s); if (aut->get_label(s)->is_syntactic_persistence()) return true; @@ -117,12 +116,10 @@ namespace spot if (!aut) return false; - const std::list states = map.states_of(scc); - std::list::const_iterator it; - for (it = states.begin(); it != states.end(); ++it) + for (auto ss: map.states_of(scc)) { const state_explicit_formula* s = - down_cast(*it); + down_cast(ss); assert(s); if (aut->get_label(s)->is_syntactic_guarantee()) return true; @@ -134,18 +131,15 @@ namespace spot is_complete_scc(scc_map& map, unsigned scc) { const spot::tgba *a = map.get_aut(); - const std::list states = map.states_of(scc); - std::list::const_iterator it; - for (it = states.begin(); it != states.end(); ++it) + for (auto s: map.states_of(scc)) { - const state *s = *it; tgba_succ_iterator* it = a->succ_iter(s); it->first(); // If a state has no successors, the SCC is not complete. if (it->done()) { - delete it; + a->release_iter(it); return false; } @@ -163,7 +157,7 @@ namespace spot it->next(); } while (!it->done()); - delete it; + a->release_iter(it); if (sumall != bddtrue) return false; diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 36f0e40a0..3c4c17e7c 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris +// 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. // @@ -104,7 +104,7 @@ namespace spot it->first(); bool accepting = !it->done() && it->current_acceptance_conditions() == all_acc_conds_; - delete it; + aut_->release_iter(it); return accepting; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 5f94801b3..167495ba7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -110,7 +110,7 @@ namespace spot { public: ratexp_to_dfa(translate_dict& dict); - tgba_succ_iterator* succ(const formula* f); + std::pair succ(const formula* f); const formula* get_label(const formula* f, const state* s) const; ~ratexp_to_dfa(); @@ -1133,7 +1133,7 @@ namespace spot } // FIXME: use the new tgba::succ() interface - tgba_succ_iterator* + std::pair ratexp_to_dfa::succ(const formula* f) { f2a_t::const_iterator it = f2a_.find(f); @@ -1145,13 +1145,11 @@ namespace spot // If a is nul, f has an empty language. if (!a) - return 0; + return {nullptr, nullptr}; assert(a->has_state(f)); // This won't create a new state. - const state* s = a->add_state(f); - - return a->succ_iter(s); + return {a, a->add_state(f)}; } const formula* @@ -1364,12 +1362,11 @@ namespace spot { // rat_seen_ = true; const formula* f = node->child(); - tgba_succ_iterator* i = dict_.transdfa.succ(f); + auto p = dict_.transdfa.succ(f); res_ = bddfalse; - - if (!i) + if (!p.first) break; - for (i->first(); !i->done(); i->next()) + for (auto i: p.first->succ(p.second)) { bdd label = i->current_condition(); state* s = i->current_state(); @@ -1391,7 +1388,6 @@ namespace spot res_ |= label & bdd_ithvar(x); } } - delete i; } break; diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 40bec93a5..e682285cc 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -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) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -68,13 +68,13 @@ namespace spot while (!st_blue.empty()) { h.pop_notify(st_blue.front().s); - delete st_blue.front().it; + a_->release_iter(st_blue.front().it); st_blue.pop_front(); } while (!st_red.empty()) { h.pop_notify(st_red.front().s); - delete st_red.front().it; + a_->release_iter(st_red.front().it); st_red.pop_front(); } } @@ -159,7 +159,7 @@ namespace spot void pop(stack_type& st) { dec_depth(); - delete st.front().it; + a_->release_iter(st.front().it); st.pop_front(); } diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index bff3c3cc9..0333b2026 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -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) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -230,11 +230,11 @@ namespace spot typedef std::unordered_set state_set; - void clean(stack_type& st1, state_set& seen, state_set& dead) + void clean(const tgba* a, stack_type& st1, state_set& seen, state_set& dead) { while (!st1.empty()) { - delete st1.front().it; + a->release_iter(st1.front().it); st1.pop_front(); } for (state_set::iterator i = seen.begin(); i != seen.end();) @@ -309,7 +309,7 @@ namespace spot covered_acc |= acc; if (covered_acc == a_->all_acceptance_conditions()) { - clean(st1, seen, dead); + clean(a_, st1, seen, dead); s_prime->destroy(); return true; } @@ -334,7 +334,7 @@ namespace spot ndfsr_trace << " all the successors have been visited" << std::endl; stack_item f_dest(f); - delete st1.front().it; + a_->release_iter(st1.front().it); st1.pop_front(); if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) { @@ -351,7 +351,7 @@ namespace spot covered_acc |= f_dest.acc; if (covered_acc == a_->all_acceptance_conditions()) { - clean(st1, seen, dead); + clean(a_, st1, seen, dead); return true; } } @@ -364,7 +364,7 @@ namespace spot } } - clean(st1, seen, dead); + clean(a_, st1, seen, dead); return false; } diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 42cb53140..ba36f1bde 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -88,7 +89,7 @@ namespace spot it->first(); bool accepting = !it->done() && it->current_acceptance_conditions() == all_acc_conds_; - delete it; + aut_->release_iter(it); return accepting; } @@ -123,7 +124,7 @@ namespace spot label = "accept_all"; current->destroy(); } - delete it; + aut_->release_iter(it); } else label = "T0_S" + ns; @@ -149,7 +150,7 @@ namespace spot } else { - state* current =it->current_state(); + state* current = it->current_state(); if (state_is_accepting(s) && it->current_condition() == bddtrue && s->compare(init_) != 0 @@ -167,8 +168,8 @@ namespace spot } current->destroy(); } - delete it; - } + aut_->release_iter(it); + } void process_link(const state*, int in, const state*, int out, diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 6fb676dbb..edc090065 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -81,7 +82,7 @@ namespace spot current->destroy(); } } - delete si; + aut_->release_iter(si); } end(); } @@ -174,7 +175,7 @@ namespace spot void tgba_reachable_iterator_depth_first::pop() { - delete todo.back().it; + aut_->release_iter(todo.back().it); todo.pop_back(); if (!todo.empty()) todo.back().it->next(); diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index cab0320ee..ed579f061 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -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) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -189,7 +189,7 @@ namespace spot s2->destroy(); } } - delete j; + a->release_iter(j); s->destroy(); return false; } @@ -211,7 +211,7 @@ namespace spot bdd_print_accset(os, a->get_dict(), acc); os << std::endl; } - delete j; + a->release_iter(j); // Sum acceptance conditions. // diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index f373c4f42..1c66609a2 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -60,7 +60,7 @@ namespace spot it->next(); result = (!dest->compare(s)) && it->done() && (cond == bddtrue); dest->destroy(); - delete it; + aut->release_iter(it); } // Free the scc_map if we created it. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 3ec480ead..18ba54e3e 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita. +// Copyright (C) 2008, 2009, 2011, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -199,7 +199,7 @@ namespace spot root_.front().succ.insert(std::make_pair(num, cond)); } - delete succ; + aut_->release_iter(succ); // Do not destroy CURR: it is a key in H. continue; } diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 1c6392a2e..a17055bf3 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -68,13 +68,13 @@ namespace spot while (!st_blue.empty()) { h.pop_notify(st_blue.front().s); - delete st_blue.front().it; + a_->release_iter(st_blue.front().it); st_blue.pop_front(); } while (!st_red.empty()) { h.pop_notify(st_red.front().s); - delete st_red.front().it; + a_->release_iter(st_red.front().it); st_red.pop_front(); } } @@ -159,7 +159,7 @@ namespace spot void pop(stack_type& st) { dec_depth(); - delete st.front().it; + a_->release_iter(st.front().it); st.pop_front(); } diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 2f64694f4..583d5bb5a 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -335,14 +335,12 @@ namespace spot // the acceptance of the destination state on its incoming // arcs (which now become outgoing args after // transposition). - tgba_succ_iterator* it = out_->succ_iter(out_s); - it->first(); - if (!it->done()) + for (auto it: out_->succ(out_s)) { bdd acc = ac_.complement(it->current_acceptance_conditions()); t->acceptance_conditions = acc; + break; } - delete it; } } diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index c57236b04..579017311 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -68,13 +68,13 @@ namespace spot while (!st_blue.empty()) { h.pop_notify(st_blue.front().s); - delete st_blue.front().it; + a_->release_iter(st_blue.front().it); st_blue.pop_front(); } while (!st_red.empty()) { h.pop_notify(st_red.front().s); - delete st_red.front().it; + a_->release_iter(st_red.front().it); st_red.pop_front(); } } @@ -133,7 +133,7 @@ namespace spot void pop(stack_type& st) { dec_depth(); - delete st.front().it; + a_->release_iter(st.front().it); st.pop_front(); } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 07bf37fb2..bcedc9e37 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -93,13 +93,13 @@ namespace spot while (!st_blue.empty()) { h.pop_notify(st_blue.front().s); - delete st_blue.front().it; + a_->release_iter(st_blue.front().it); st_blue.pop_front(); } while (!st_red.empty()) { h.pop_notify(st_red.front().s); - delete st_red.front().it; + a_->release_iter(st_red.front().it); st_red.pop_front(); } } @@ -158,7 +158,7 @@ namespace spot void pop(stack_type& st) { dec_depth(); - delete st.front().it; + a_->release_iter(st.front().it); st.pop_front(); }