diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 9ceead7ae..4adebdb92 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2013 Laboratoire de Recherche et +// Copyright (C) 2008, 2011, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis @@ -365,9 +365,7 @@ namespace spot state** state_array = 0; size_t size_states = 0; - tgba_succ_iterator* i = data_->operand->succ_iter(s->right()); - - for (i->first(); !i->done(); i->next()) + for (auto i: data_->operand->succ(s)) { all_conds_ = i->current_condition(); outside_ = !all_conds_; @@ -454,8 +452,6 @@ namespace spot free(props_[j].prop[conj]); free(props_[j].prop); } - - delete i; return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_, bdd_array, state_array, size_states, props_, diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 5cabb39b9..f3ec6a5ca 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Développement de +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -153,8 +153,7 @@ namespace spot todo.pop_front(); int src = bs2num[s]; - tgba_succ_iterator* i = a->succ_iter(a->get_state(s.s)); - for (i->first(); !i->done(); i->next()) + for (auto i: a->succ(a->get_state(s.s))) { int dlabel = label(a, i->current_state()); @@ -216,7 +215,6 @@ namespace spot t->condition = i->current_condition(); } } - delete i; } diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index a786125c3..204912b3c 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 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. // @@ -208,17 +208,14 @@ namespace spot { // Get successors states. bdd condition = it->first; - tgba_succ_iterator* iterator = - automaton_->succ_iter(origin_->get_state()); std::vector state_list; - for (iterator->first(); !iterator->done(); iterator->next()) - { - bdd c = iterator->current_condition(); - if ((c & condition) != bddfalse) - state_list.push_back(shared_state(iterator->current_state(), - shared_state_deleter)); - } - delete iterator; + for (auto iterator: automaton_->succ(origin_->get_state())) + { + bdd c = iterator->current_condition(); + if ((c & condition) != bddfalse) + state_list.push_back(shared_state(iterator->current_state(), + shared_state_deleter)); + } // Make the conjunction with ranks. std::vector current_ranks(state_list.size(), max_rank); @@ -292,14 +289,11 @@ namespace spot std::set atomics; delete_condition_list(); - tgba_succ_iterator* iterator = - automaton_->succ_iter(origin_->get_state()); - for (iterator->first(); !iterator->done(); iterator->next()) + for (auto iterator: automaton_->succ(origin_->get_state())) { bdd c = iterator->current_condition(); get_atomics(atomics, c); } - delete iterator; // Compute the conjunction of all those atomic properties. unsigned atomics_size = atomics.size(); diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 880ba11f5..ff29aa157 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -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) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -99,6 +99,73 @@ namespace spot //@} }; + + class tgba; + + namespace internal + { + struct SPOT_API succ_iterator + { + protected: + tgba_succ_iterator* it_; + public: + + succ_iterator(tgba_succ_iterator* it): + it_(it) + { + } + + bool operator==(succ_iterator o) const + { + return it_ == o.it_; + } + + bool operator!=(succ_iterator o) const + { + return it_ != o.it_; + } + + const tgba_succ_iterator* operator*() const + { + return it_; + } + + void operator++() + { + it_->next(); + if (it_->done()) + 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/tgba.hh b/src/tgba/tgba.hh index 3fd620cb6..2640587a7 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -1,8 +1,9 @@ -// 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, 2005 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. // @@ -23,12 +24,14 @@ # define SPOT_TGBA_TGBA_HH #include "state.hh" -#include "succiter.hh" #include "bdddict.hh" +#include "succiter.hh" namespace spot { - /// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata) + class tgba_succ_iterator; + + /// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata) /// /// Spot is centered around the spot::tgba type. This type and its /// cousins are listed \ref tgba_essentials "here". This is an @@ -42,15 +45,15 @@ namespace spot /// \ingroup tgba /// \ingroup tgba_essentials - /// \brief A Transition-based Generalized Büchi Automaton. + /// \brief A Transition-based Generalized Büchi Automaton. /// - /// The acronym TGBA (Transition-based Generalized Büchi Automaton) + /// The acronym TGBA (Transition-based Generalized Büchi Automaton) /// was coined by Dimitra Giannakopoulou and Flavio Lerda /// in "From States to Transitions: Improving Translation of LTL - /// Formulae to Büchi Automata". (FORTE'02) + /// Formulae to Büchi Automata". (FORTE'02) /// /// TGBAs are transition-based, meanings their labels are put - /// on arcs, not on nodes. They use Generalized Büchi acceptance + /// on arcs, not on nodes. They use Generalized Büchi acceptance /// conditions: there are several acceptance sets (of /// transitions), and a path can be accepted only if it traverses /// at least one transition of each set infinitely often. @@ -105,8 +108,18 @@ namespace spot /// product automaton. Otherwise, 0. virtual tgba_succ_iterator* succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const = 0; + const state* global_state = nullptr, + const tgba* global_automaton = nullptr) const = 0; + + /// \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(const state* s) const + { + return {this, succ_iter(s)}; + } /// \brief Get a formula that must hold whatever successor is taken. /// diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index bd0b86c84..b8b5cfd22 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -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. // @@ -325,13 +325,11 @@ namespace spot i != sr_map.end(); ++i) { - tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get()); - for (iterator->first(); !iterator->done(); iterator->next()) + for (auto iterator: automaton_->succ(i->first.get())) { bdd c = iterator->current_condition(); get_atomics(atomics, c); } - delete iterator; } // Compute the conjunction of all those atomic properties. @@ -433,8 +431,7 @@ namespace spot i != sr_map.end(); ++i) { - tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get()); - for (iterator->first(); !iterator->done(); iterator->next()) + for (auto iterator: automaton_->succ(i->first.get())) { bdd c = iterator->current_condition(); if ((c & condition) != bddfalse) @@ -449,7 +446,6 @@ namespace spot highest_current_ranks_[s] = i->second; } } - delete iterator; } // Highest $O$ set of the algorithm. @@ -460,8 +456,7 @@ namespace spot i != s_set.end(); ++i) { - tgba_succ_iterator* iterator = automaton_->succ_iter(i->get()); - for (iterator->first(); !iterator->done(); iterator->next()) + for (auto iterator: automaton_->succ(i->get())) { bdd c = iterator->current_condition(); if ((c & condition) != bddfalse) @@ -470,7 +465,6 @@ namespace spot highest_state_set_.insert(s); } } - delete iterator; } current_ranks_ = highest_current_ranks_; @@ -683,22 +677,18 @@ namespace spot bdd tgba_kv_complement::compute_support_conditions(const state* state) const { - tgba_succ_iterator* i = succ_iter(state); - bdd result = bddtrue; - for (i->first(); !i->done(); i->next()) + bdd result = bddfalse; + for (auto i: succ(state)) result |= i->current_condition(); - delete i; return result; } bdd tgba_kv_complement::compute_support_variables(const state* state) const { - tgba_succ_iterator* i = succ_iter(state); bdd result = bddtrue; - for (i->first(); !i->done(); i->next()) + for (auto i: succ(state)) result &= bdd_support(i->current_condition()); - delete i; return result; } diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index b5fb09a30..26844b934 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -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. @@ -36,8 +36,8 @@ namespace spot { ~succ_iter_filtered() { - for (first(); !done(); next()) - it_->dest->destroy(); + for (auto& t: trans_) + t.dest->destroy(); } void first() @@ -138,15 +138,11 @@ namespace spot tgba_succ_iterator* tgba_mask::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const + const state*, + const tgba*) const { - tgba_succ_iterator* it = original_->succ_iter(local_state, - global_state, - global_automaton); - succ_iter_filtered* res = new succ_iter_filtered; - for (it->first(); !it->done(); it->next()) + for (auto it: original_->succ(local_state)) { const state* s = it->current_state(); if (!wanted(s)) @@ -159,7 +155,6 @@ namespace spot it->current_acceptance_conditions() }; res->trans_.push_back(t); } - delete it; return res; } diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 1baaad3c7..68d29fc80 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 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. // @@ -153,10 +153,9 @@ namespace spot name = other.name; parent = 0; nodes = other.nodes; - for (child_list::const_iterator i = other.children.begin(); - i != other.children.end(); ++i) + for (auto i: other.children) { - safra_tree* c = new safra_tree(**i); + safra_tree* c = new safra_tree(*i); c->parent = this; children.push_back(c); } @@ -170,11 +169,10 @@ namespace spot safra_tree::~safra_tree() { - for (child_list::iterator i = children.begin(); i != children.end(); ++i) - delete *i; - - for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) - (*i)->destroy(); + for (auto c: children) + delete c; + for (auto n: nodes) + n->destroy(); } safra_tree& @@ -237,13 +235,10 @@ namespace spot hash ^= wang32_hash(name); hash ^= wang32_hash(marked); - for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i) - hash ^= (*i)->hash(); - - for (child_list::const_iterator i = children.begin(); - i != children.end(); - ++i) - hash ^= (*i)->hash(); + for (auto n: nodes) + hash ^= n->hash(); + for (auto c: children) + hash ^= c->hash(); return hash; } @@ -262,13 +257,12 @@ namespace spot safra_tree::max_name() const { int max_name = name; - for (child_list::const_iterator i = children.begin(); - i != children.end(); ++i) - max_name = std::max(max_name, (*i)->max_name()); + for (auto c: children) + max_name = std::max(max_name, c->max_name()); return max_name; } - /// \brief Get an unused name in the tree for a new node. + /// \brief Get a unused name in the tree for a new node. /// /// The root of the tree maintains a list of unused names. /// When this list is empty, new names are computed. @@ -287,9 +281,8 @@ namespace spot const safra_tree* current = queue.front(); queue.pop_front(); used_names.insert(current->name); - for (child_list::const_iterator i = current->children.begin(); - i != current->children.end(); ++i) - queue.push_back(*i); + for (auto c: current->children) + queue.push_back(c); } int l = 0; @@ -325,13 +318,13 @@ namespace spot safra_tree* safra_tree::branch_accepting(const sba& a) { - for (child_list::iterator i = children.begin(); i != children.end(); ++i) - (*i)->branch_accepting(a); + for (auto c: children) + c->branch_accepting(a); subset_t subset; - for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i) - if (a.state_is_accepting(*i)) - subset.insert(*i); + for (auto n: nodes) + if (a.state_is_accepting(n)) + subset.insert(n); if (!subset.empty()) children.push_back(new safra_tree(subset, this, get_new_name())); @@ -354,22 +347,20 @@ namespace spot { subset_t new_subset; - for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) + for (auto n: nodes) { - cache_t::const_iterator it = cache_transition.find(*i); + cache_t::const_iterator it = cache_transition.find(n); if (it == cache_transition.end()) continue; const tr_cache_t& transitions = it->second; - for (tr_cache_t::const_iterator t_it = transitions.begin(); - t_it != transitions.end(); - ++t_it) + for (auto t: transitions) { - if ((t_it->first & condition) != bddfalse) + if ((t.first & condition) != bddfalse) { - if (new_subset.find(t_it->second) == new_subset.end()) + if (new_subset.find(t.second) == new_subset.end()) { - const state* s = t_it->second->clone(); + const state* s = t.second->clone(); new_subset.insert(s); } } @@ -377,8 +368,8 @@ namespace spot } nodes = new_subset; - for (child_list::iterator i = children.begin(); i != children.end(); ++i) - (*i)->succ_create(condition, cache_transition); + for (auto c: children) + c->succ_create(condition, cache_transition); return this; } @@ -391,18 +382,16 @@ namespace spot safra_tree::normalize_siblings() { std::set node_set; - for (child_list::iterator child_it = children.begin(); - child_it != children.end(); - ++child_it) + for (auto c: children) { - subset_t::iterator node_it = (*child_it)->nodes.begin(); - while (node_it != (*child_it)->nodes.end()) + subset_t::iterator node_it = c->nodes.begin(); + while (node_it != c->nodes.end()) { if (!node_set.insert(*node_it).second) { const state* s = *node_it; - (*child_it)->remove_node_from_children(*node_it); - (*child_it)->nodes.erase(node_it++); + c->remove_node_from_children(*node_it); + c->nodes.erase(node_it++); s->destroy(); } else @@ -411,7 +400,7 @@ namespace spot } } - (*child_it)->normalize_siblings(); + c->normalize_siblings(); } return this; @@ -421,18 +410,16 @@ namespace spot void safra_tree::remove_node_from_children(const state* state) { - for (child_list::iterator child_it = children.begin(); - child_it != children.end(); - ++child_it) + for (auto c: children) { - subset_t::iterator it = (*child_it)->nodes.find(state); - if (it != (*child_it)->nodes.end()) + subset_t::iterator it = c->nodes.find(state); + if (it != c->nodes.end()) { const spot::state* s = *it; - (*child_it)->nodes.erase(it); + c->nodes.erase(it); s->destroy(); } - (*child_it)->remove_node_from_children(state); + c->remove_node_from_children(state); } } @@ -470,12 +457,10 @@ namespace spot safra_tree::mark() { std::set node_set; - for (child_list::const_iterator child_it = children.begin(); - child_it != children.end(); - ++child_it) + for (auto c: children) { - node_set.insert((*child_it)->nodes.begin(), (*child_it)->nodes.end()); - (*child_it)->mark(); + node_set.insert(c->nodes.begin(), c->nodes.end()); + c->mark(); } char same = node_set.size() == nodes.size(); @@ -500,10 +485,8 @@ namespace spot if (same) { marked = true; - for (child_list::iterator i = children.begin(); - i != children.end(); - ++i) - delete *i; + for (auto c: children) + delete c; children = child_list(); } @@ -526,10 +509,8 @@ namespace spot assert(bitset.size() > static_cast(name)); if (marked && !nodes.empty()) bitset.set(name); - for (child_list::const_iterator i = children.begin(); - i != children.end(); - ++i) - (*i)->getL(bitset); + for (auto c: children) + c->getL(bitset); } /// Returns in which sets U (the semantic differs according to Rabin or @@ -544,10 +525,8 @@ namespace spot assert(bitset.size() > static_cast(name)); if (!nodes.empty()) bitset.clear(name); - for (child_list::const_iterator i = children.begin(); - i != children.end(); - ++i) - (*i)->getU(bitset); + for (auto c: children) + c->getU(bitset); } bool @@ -632,12 +611,11 @@ namespace spot // Create successors of the Safra's tree. safra_tree_automaton::transition_list transitions; - for (conjunction_list_t::const_iterator i = conjunction.begin(); - i != conjunction.end(); ++i) + for (auto i: conjunction) { safra_tree* successor = new safra_tree(*current); successor->branch_accepting(*sba_aut); // Step 2 - successor->succ_create(*i, cache); // Step 3 + successor->succ_create(i, cache); // Step 3 successor->normalize_siblings(); // Step 4 successor->remove_empty(); // Step 5 successor->mark(); // Step 6 @@ -646,7 +624,7 @@ namespace spot safra_tree_ptr_equal comparator(successor); if (st->automaton.find(successor) != st->automaton.end()) { - transitions[*i] = st->automaton.find(successor)->first; + transitions[i] = st->automaton.find(successor)->first; } else { @@ -654,12 +632,12 @@ namespace spot std::find_if(queue.begin(), queue.end(), comparator); if (item_in_queue != queue.end()) { - transitions[*i] = *item_in_queue; + transitions[i] = *item_in_queue; } else { delete_this_successor = false; - transitions[*i] = successor; + transitions[i] = successor; queue.push_back(successor); } } @@ -672,13 +650,9 @@ namespace spot queue.pop_front(); - for (safra_tree::cache_t::iterator i = cache.begin(); - i != cache.end(); - ++i) - for (safra_tree::tr_cache_t::iterator j = i->second.begin(); - j != i->second.end(); - ++j) - j->second->destroy(); + for (auto i: cache) + for (auto j: i.second) + j.second->destroy(); // delete node; } @@ -694,21 +668,17 @@ namespace spot safra_tree::cache_t& cache, atomic_list_t& atomic_list) { - for (safra_tree::subset_t::iterator it = node->nodes.begin(); - it != node->nodes.end(); - ++it) + for (auto n: node->nodes) { safra_tree::tr_cache_t transitions; - tgba_succ_iterator* iterator = sba_aut->succ_iter(*it); - for (iterator->first(); !iterator->done(); iterator->next()) + for (auto iterator: sba_aut->succ(n)) { bdd condition = iterator->current_condition(); typedef std::pair bdd_state; transitions.insert(bdd_state(condition, iterator->current_state())); set_atomic_list(atomic_list, condition); } - delete iterator; - cache[*it] = transitions; + cache[n] = transitions; } } @@ -741,16 +711,15 @@ namespace spot { bdd result = bddtrue; unsigned position = 1; - for (atomic_list_t::const_iterator a_it = atomics.begin(); - a_it != atomics.end(); - ++a_it, position <<= 1) + for (auto a: atomics) { bdd this_atomic; if (position & i) - this_atomic = bdd_ithvar(*a_it); + this_atomic = bdd_ithvar(a); else - this_atomic = bdd_nithvar(*a_it); - result = bdd_apply(result, this_atomic, bddop_and); + this_atomic = bdd_nithvar(a); + result &= this_atomic; + position <<= 1; } list.insert(result); } @@ -787,14 +756,12 @@ namespace spot std::cout << "node" << this_node << "[label=\""; std::cout << this_node->name << "|"; - for (safra_tree::subset_t::const_iterator j = this_node->nodes.begin(); - j != this_node->nodes.end(); - ++j) + for (auto j: this_node->nodes) { - stnum_t::const_iterator it = node_names.find(*j); + stnum_t::const_iterator it = node_names.find(j); int name; if (it == node_names.end()) - name = node_names[*j] = current_node++; + name = node_names[j] = current_node++; else name = it->second; std::cout << name << ", "; @@ -820,8 +787,6 @@ namespace spot { typedef safra_tree_automaton::automaton_t::reverse_iterator automaton_cit; - typedef safra_tree_automaton::transition_list::const_iterator - trans_cit; stnum_t node_names; int current_node = 0; int nb_accepting_conditions = a->get_nb_acceptance_pairs(); @@ -840,20 +805,19 @@ namespace spot std::cout << "}" << std::endl; // Successors. - for (trans_cit j = i->second.begin(); j != i->second.end(); ++j) + for (const auto& j: i->second) std::cout << "node" << i->first << "->" - << "node" << j->second << - " [label=\"" << bddset << j->first << "\"];" << std::endl; + << "node" << j.second << + " [label=\"" << bddset << j.first << "\"];" << std::endl; } // Output the real name of all states. std::cout << "{ rank=sink; legend [shape=none,margin=0,label=<\n" << "\n"; - for (stnum_t::const_iterator it = node_names.begin(); - it != node_names.end(); ++it) - std::cout << "\n"; std::cout << "
" << it->second << "" - << a->get_sba()->format_state(it->first) + for (const auto& nn: node_names) + std::cout << "
" << nn.second << "" + << a->get_sba()->format_state(nn.first) << "
\n" << ">]}" << std::endl; @@ -1008,8 +972,8 @@ namespace spot virtual ~tgba_safra_complement_succ_iterator() { - for (succ_list_t::iterator i = list_.begin(); i != list_.end(); ++i) - delete i->second; + for (auto& p: list_) + delete p.second; } virtual void first(); @@ -1076,12 +1040,8 @@ namespace spot safra_tree_automaton::~safra_tree_automaton() { - for (automaton_t::iterator i = automaton.begin(); - i != automaton.end(); - ++i) - { - delete i->first; - } + for (auto& p: automaton) + delete p.first; delete a_; } @@ -1092,10 +1052,8 @@ namespace spot return max_nb_pairs_; int max = -1; - for (automaton_t::const_iterator i = automaton.begin(); - i != automaton.end(); - ++i) - max = std::max(max, i->first->max_name()); + for (auto& p: automaton) + max = std::max(max, p.first->max_name()); return max_nb_pairs_ = max + 1; } @@ -1215,8 +1173,6 @@ namespace spot safra_tree_automaton::automaton_t::const_iterator tr = a->automaton.find(const_cast(s->get_safra())); - typedef safra_tree_automaton::transition_list::const_iterator trans_iter; - if (tr != a->automaton.end()) { bdd condition = bddfalse; @@ -1226,14 +1182,14 @@ namespace spot if (!s->get_use_bitset()) // if \delta'(q, a) { - for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + for (auto& p: tr->second) { state_complement* s1 = new state_complement(e->clone(), e->clone(), - i->second, false); + p.second, false); state_complement* s2 = new state_complement(e->clone(), e->clone(), - i->second, true); - succ_list.insert(std::make_pair(i->first, s1)); - succ_list.insert(std::make_pair(i->first, s2)); + p.second, true); + succ_list.insert(std::make_pair(p.first, s1)); + succ_list.insert(std::make_pair(p.first, s2)); } } else @@ -1254,19 +1210,19 @@ namespace spot // \delta'((q, I, J), a) if I'\subseteq J' if (newI->is_subset_of(*newJ)) { - for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + for (auto& p: tr->second) { - st = new state_complement(e->clone(), e->clone(), i->second, true); - succ_list.insert(std::make_pair(i->first, st)); + st = new state_complement(e->clone(), e->clone(), p.second, true); + succ_list.insert(std::make_pair(p.first, st)); } condition = the_acceptance_cond_; } else // \delta'((q, I, J), a) { - for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + for (auto& p: tr->second) { - st = new state_complement(newI, newJ, i->second, true); - succ_list.insert(std::make_pair(i->first, st)); + st = new state_complement(newI, newJ, p.second, true); + succ_list.insert(std::make_pair(p.first, st)); } } delete newI; @@ -1277,11 +1233,11 @@ namespace spot bitvect* pending = S.clone(); *pending |= *l; *pending -= *u; - for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + for (auto& p: tr->second) { st = new state_complement(pending->clone(), e->clone(), - i->second, true); - succ_list.insert(std::make_pair(i->first, st)); + p.second, true); + succ_list.insert(std::make_pair(p.first, st)); } delete pending; @@ -1341,16 +1297,14 @@ namespace spot const state_complement* s = down_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; - typedef safra_tree_automaton::transition_list::const_iterator trans_it; auto_it node(a->automaton.find(const_cast(s->get_safra()))); if (node == a->automaton.end()) return bddtrue; bdd res = bddtrue; - trans_it i; - for (i = node->second.begin(); i != node->second.end(); ++i) - res |= i->first; + for (auto& i: node->second) + res |= i.first; return res; } @@ -1361,16 +1315,14 @@ namespace spot const state_complement* s = down_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; - typedef safra_tree_automaton::transition_list::const_iterator trans_it; auto_it node(a->automaton.find(const_cast(s->get_safra()))); if (node == a->automaton.end()) return bddtrue; bdd res = bddtrue; - trans_it i; - for (i = node->second.begin(); i != node->second.end(); ++i) - res &= bdd_support(i->first); + for (auto& i: node->second) + res &= bdd_support(i.first); return res; } diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index e055439a0..201ae93f5 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita. // 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. +// 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. // @@ -517,10 +518,12 @@ namespace spot return i->second; bdd common = a_->all_acceptance_conditions(); - tgba_succ_iterator* it = a_->succ_iter(s); - for (it->first(); !it->done() && common != bddfalse; it->next()) - common &= it->current_acceptance_conditions(); - delete it; + for (auto it: a_->succ(s)) + { + common &= it->current_acceptance_conditions(); + if (common == bddfalse) + break; + } // Populate cache accmap_[s->clone()] = common; @@ -537,10 +540,8 @@ namespace spot return i->second; bdd common = bddfalse; - tgba_succ_iterator* it = a_->succ_iter(s); - for (it->first(); !it->done(); it->next()) + for (auto it: a_->succ(s)) common |= it->current_acceptance_conditions(); - delete it; // Populate cache accmapu_[s->clone()] = common; @@ -618,8 +619,7 @@ namespace spot bdd all = a->all_acceptance_conditions(); state* init = a->get_init_state(); - tgba_succ_iterator* it = a->succ_iter(init); - for (it->first(); !it->done(); it->next()) + for (auto it: a->succ(init)) { // Look only for transitions that are accepting. if (all != it->current_acceptance_conditions()) @@ -635,13 +635,11 @@ namespace spot // The cycle_start_ points to the right starting // point already, so just return. dest->destroy(); - delete it; init->destroy(); return; } dest->destroy(); } - delete it; init->destroy(); } diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 7e1fdd013..d52dea40b 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -277,8 +277,7 @@ namespace spot const state* rs = p.second; int src = seen[p]; - tgba_succ_iterator* li = left->succ_iter(ls); - for (li->first(); !li->done(); li->next()) + for (auto li: left->succ(ls)) { state_pair d(li->current_state(), ris); bdd lc = li->current_condition(); diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index 28bc5aecc..417491682 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -55,8 +55,7 @@ namespace spot { cur = tovisit.front(); tovisit.pop(); - tgba_succ_iterator* sit = a->succ_iter(cur); - for (sit->first(); !sit->done(); sit->next()) + for (auto sit: a->succ(cur)) { cur_format = a->format_state(cur); state* dst = sit->current_state(); @@ -78,7 +77,6 @@ namespace spot dst->destroy(); } } - delete sit; } return sub_a; } diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index c649b52e5..a25d579fe 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -88,8 +88,7 @@ namespace spot unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0; bdd common = a_->all_acceptance_conditions(); bdd union_ = bddfalse; - tgba_succ_iterator* it = a_->succ_iter(s); - for (it->first(); !it->done(); it->next()) + for (auto it: a_->succ(s)) { // Ignore transitions that leave the SCC of s. const state* d = it->current_state(); @@ -102,7 +101,6 @@ namespace spot common &= set; union_ |= set; } - delete it; cache_entry e(common, union_); return cache_.insert(std::make_pair(s, e)).first; } @@ -150,8 +148,7 @@ namespace spot if (p.second) { bdd all = a_->all_acceptance_conditions(); - tgba_succ_iterator* it = a_->succ_iter(s); - for (it->first(); !it->done(); it->next()) + for (auto it: a_->succ(s)) { // Look only for transitions that are accepting. if (all != it->current_acceptance_conditions()) @@ -164,7 +161,6 @@ namespace spot break; } } - delete it; } return p.first->second; } @@ -387,8 +383,7 @@ namespace spot if (use_scc) s_scc = m.scc_of_state(s.first); - tgba_succ_iterator* i = a->succ_iter(s.first); - for (i->first(); !i->done(); i->next()) + for (auto i: a->succ(s.first)) { degen_state d(uniq(i->current_state()), 0); @@ -576,7 +571,6 @@ namespace spot t->condition |= i->current_condition(); } } - delete i; tr_cache.clear(); } diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 02b391682..3ded8d290 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 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. @@ -345,29 +345,26 @@ namespace spot next = l->begin()->s; } - // browse the actual outgoing transitions - tgba_succ_iterator* j = a->succ_iter(s); - s->destroy(); // FIXME: is it always legitimate to destroy s before j? - for (j->first(); !j->done(); j->next()) + // browse the actual outgoing transitions and + // look for next; + const state* the_next = nullptr; + for (auto j: a->succ(s)) { if (j->current_condition() != label || j->current_acceptance_conditions() != acc) continue; const state* s2 = j->current_state(); - if (s2->compare(next) != 0) + if (s2->compare(next) == 0) { - s2->destroy(); - continue; - } - else - { - s = s2; - break; - } + the_next = s2; + break; + } + s2->destroy(); } - assert(!j->done()); - delete j; + assert(res); + s->destroy(); + s = the_next; state_map::const_iterator its = seen.find(next); if (its == seen.end()) diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc index 447e33f82..ee2c4654c 100644 --- a/src/tgbaalgos/isdet.cc +++ b/src/tgbaalgos/isdet.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -44,10 +44,9 @@ namespace spot const state* src = todo.front(); todo.pop_front(); - tgba_succ_iterator* i = aut->succ_iter(src); bool nondeterministic = false; bdd available = bddtrue; - for (i->first(); !i->done(); i->next()) + for (auto i: aut->succ(src)) { // If we know the state is nondeterministic, just skip the // test for the remaining transitions. But don't break @@ -67,7 +66,6 @@ namespace spot else dst->destroy(); } - delete i; res += nondeterministic; if (!count && nondeterministic) break; @@ -110,9 +108,8 @@ namespace spot const state* src = todo.front(); todo.pop_front(); - tgba_succ_iterator* i = aut->succ_iter(src); bdd available = bddtrue; - for (i->first(); !i->done(); i->next()) + for (auto i: aut->succ(src)) { available -= i->current_condition(); const state* dst = i->current_state(); @@ -121,7 +118,6 @@ namespace spot else dst->destroy(); } - delete i; if (available != bddfalse) { complete = false; diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 99bd3dc13..5f94801b3 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 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. @@ -152,8 +152,8 @@ namespace spot ~translate_dict() { fv_map::iterator i; - for (i = next_map.begin(); i != next_map.end(); ++i) - i->first->destroy(); + for (auto& i: next_map) + i.first->destroy(); dict->unregister_all_my_variables(this); flagged_formula_to_bdd_map::iterator j = ltl_bdd_.begin(); @@ -306,10 +306,10 @@ namespace spot { fv_map::const_iterator fi; os << "Next Variables:" << std::endl; - for (fi = next_map.begin(); fi != next_map.end(); ++fi) + for (auto& fi: next_map) { - os << " " << fi->second << ": Next["; - to_string(fi->first, os) << "]" << std::endl; + os << " " << fi.second << ": Next["; + to_string(fi.first, os) << "]" << std::endl; } os << "Shared Dict:" << std::endl; dict->dump(os); @@ -1005,9 +1005,8 @@ namespace spot ratexp_to_dfa::~ratexp_to_dfa() { - std::vector::const_iterator it; - for (it = automata_.begin(); it != automata_.end(); ++it) - delete *it; + for (auto i: automata_) + delete i; } tgba_explicit_formula* @@ -1087,13 +1086,12 @@ namespace spot // SCC are numbered in topological order for (unsigned n = 0; n < scc_count; ++n) { - bool coacc = false; - const std::list& st = sm->states_of(n); // The SCC is coaccessible if any of its states // is final (i.e., it accepts [*0])... - std::list::const_iterator it; - for (it = st.begin(); it != st.end(); ++it) - if (a->get_label(*it)->accepts_eword()) + bool coacc = false; + const std::list& st = sm->states_of(n); + for (auto l: st) + if (a->get_label(l)->accepts_eword()) { coacc = true; break; @@ -1101,10 +1099,8 @@ namespace spot if (!coacc) { // ... or if any of its successors is coaccessible. - const scc_map::succ_type& succ = sm->succ(n); - for (scc_map::succ_type::const_iterator i = succ.begin(); - i != succ.end(); ++i) - if (coaccessible[i->first]) + for (auto& i: sm->succ(n)) + if (coaccessible[i.first]) { coacc = true; break; @@ -1113,13 +1109,13 @@ namespace spot if (!coacc) { // Mark all formulas of this SCC as useless. - for (it = st.begin(); it != st.end(); ++it) - f2a_[a->get_label(*it)] = 0; + for (auto f: st) + f2a_[a->get_label(f)] = nullptr; } else { - for (it = st.begin(); it != st.end(); ++it) - f2a_[a->get_label(*it)] = a; + for (auto f: st) + f2a_[a->get_label(f)] = a; } coaccessible[n] = coacc; } @@ -1136,6 +1132,7 @@ namespace spot } } + // FIXME: use the new tgba::succ() interface tgba_succ_iterator* ratexp_to_dfa::succ(const formula* f) { diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index a5248f161..fefffdbb9 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -93,26 +93,24 @@ namespace spot tovisit.push(init); seen->insert(init); while (!tovisit.empty()) - { - const state* src = tovisit.front(); - tovisit.pop(); - - tgba_succ_iterator* sit = a->succ_iter(src); - for (sit->first(); !sit->done(); sit->next()) { - const state* dst = sit->current_state(); - // Is it a new state ? - if (seen->find(dst) == seen->end()) + const state* src = tovisit.front(); + tovisit.pop(); + + for (auto sit: a->succ(src)) { - // Register the successor for later processing. - tovisit.push(dst); - seen->insert(dst); + const state* dst = sit->current_state(); + // Is it a new state ? + if (seen->find(dst) == seen->end()) + { + // Register the successor for later processing. + tovisit.push(dst); + seen->insert(dst); + } + else + dst->destroy(); } - else - dst->destroy(); } - delete sit; - } } // From the base automaton and the list of sets, build the minimal @@ -128,13 +126,13 @@ namespace spot std::list::iterator sit; unsigned num = 0; for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - for (hit = h->begin(); hit != h->end(); ++hit) - state_num[*hit] = num; - ++num; - } + { + hash_set::iterator hit; + hash_set* h = *sit; + for (hit = h->begin(); hit != h->end(); ++hit) + state_num[*hit] = num; + ++num; + } typedef state_explicit_number::transition trs; sba_explicit_number* res = new sba_explicit_number(a->get_dict()); // For each transition in the initial automaton, add the corresponding @@ -142,31 +140,29 @@ namespace spot if (!final->empty()) res->declare_acceptance_condition(ltl::constant::true_instance()); for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; + { + hash_set::iterator hit; + hash_set* h = *sit; - // Pick one state. - const state* src = *h->begin(); - unsigned src_num = state_num[src]; - bool accepting = (final->find(src) != final->end()); + // Pick one state. + const state* src = *h->begin(); + unsigned src_num = state_num[src]; + bool accepting = (final->find(src) != final->end()); - // Connect it to all destinations. - tgba_succ_iterator* succit = a->succ_iter(src); - for (succit->first(); !succit->done(); succit->next()) - { - const state* dst = succit->current_state(); - hash_map::const_iterator i = state_num.find(dst); - dst->destroy(); - if (i == state_num.end()) // Ignore useless destinations. - continue; - trs* t = res->create_transition(src_num, i->second); - res->add_conditions(t, succit->current_condition()); - if (accepting) - res->add_acceptance_condition(t, ltl::constant::true_instance()); - } - delete succit; - } + // Connect it to all destinations. + for (auto succit: a->succ(src)) + { + const state* dst = succit->current_state(); + hash_map::const_iterator i = state_num.find(dst); + dst->destroy(); + if (i == state_num.end()) // Ignore useless destinations. + continue; + trs* t = res->create_transition(src_num, i->second); + res->add_conditions(t, succit->current_condition()); + if (accepting) + res->add_acceptance_condition(t, ltl::constant::true_instance()); + } + } res->merge_transitions(); const state* init_state = a->get_init_state(); unsigned init_num = state_num[init_state]; @@ -362,8 +358,7 @@ namespace spot { const state* src = *hi; bdd f = bddfalse; - tgba_succ_iterator* si = det_a->succ_iter(src); - for (si->first(); !si->done(); si->next()) + for (auto si: det_a->succ(src)) { const state* dst = si->current_state(); hash_map::const_iterator i = state_set_map.find(dst); @@ -378,7 +373,6 @@ namespace spot continue; f |= (bdd_ithvar(i->second) & si->current_condition()); } - delete si; // Have we already seen this formula ? bdd_states_map::iterator bsi = bdd_map.find(f); diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 1dedc06a1..1dd2c5e0d 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -72,8 +72,8 @@ namespace spot bdd all_vars = bddtrue; power_state::const_iterator i; - for (i = src.begin(); i != src.end(); ++i) - all_vars &= aut->support_variables(*i); + for (auto s: src) + all_vars &= aut->support_variables(s); // Compute all possible combinations of these variables. bdd all_conds = bddtrue; @@ -84,17 +84,10 @@ namespace spot // Construct the set of all states reachable via COND. power_state dest; - for (i = src.begin(); i != src.end(); ++i) - { - tgba_succ_iterator *si = aut->succ_iter(*i); - for (si->first(); !si->done(); si->next()) - if ((cond >> si->current_condition()) == bddtrue) - { - const state* s = pm.canonicalize(si->current_state()); - dest.insert(s); - } - delete si; - } + for (auto s: src) + for (auto si: aut->succ(s)) + if ((cond >> si->current_condition()) == bddtrue) + dest.insert(pm.canonicalize(si->current_state())); if (dest.empty()) continue; // Add that transition. @@ -177,10 +170,8 @@ namespace spot // } bdd acc = aut_->all_acceptance_conditions(); - for (trans_set::iterator i = all_.begin(); i != all_.end(); ++i) - { - (*i)->acceptance_conditions = acc; - } + for (auto i: all_) + i->acceptance_conditions = acc; return threshold_ != 0 && cycles_left_ == 0; } @@ -213,17 +204,13 @@ namespace spot // start of the loop in the determinized automaton. const power_map::power_state& ps = refmap_.states_of(a->get_label(begin->ts->first)); - for (power_map::power_state::const_iterator it = ps.begin(); - it != ps.end() && !accepting; ++it) + for (auto s: ps) { // Construct a product between - // LOOP_A, and ORIG_A starting in *IT. - - tgba* p = new tgba_product_init(&loop_a, ref_, - loop_a_init, *it); + // LOOP_A, and ORIG_A starting in S. + tgba* p = new tgba_product_init(&loop_a, ref_, loop_a_init, s); //spot::dotty_reachable(std::cout, p); - couvreur99_check* ec = down_cast(couvreur99(p)); assert(ec); emptiness_check_result* res = ec->check(); @@ -232,6 +219,8 @@ namespace spot delete res; delete ec; delete p; + if (accepting) + break; } loop_a_init->destroy(); @@ -242,8 +231,8 @@ namespace spot print_set(std::ostream& o, const trans_set& s) const { o << "{ "; - for (trans_set::const_iterator i = s.begin(); i != s.end(); ++i) - o << *i << " "; + for (auto i: s) + o << i << " "; o << "}"; return o; } @@ -272,15 +261,11 @@ namespace spot } else { - for (trans_set::const_iterator i = ts.begin(); i != ts.end(); ++i) + for (auto t: ts) { - trans* t = *i; reject_.insert(t); - for (set_set::iterator j = accept_.begin(); - j != accept_.end(); ++j) - { - j->erase(t); - } + for (auto& j: accept_) + j.erase(t); all_.erase(t); } } diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 7d61cc531..f373c4f42 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -85,8 +85,7 @@ namespace spot const state* s = todo.front(); todo.pop_front(); - tgba_succ_iterator* it = aut->succ_iter(s); - for (it->first(); !it->done(); it->next()) + for (auto it: aut->succ(s)) { bdd acc = it->current_acceptance_conditions(); if (acc != all_acc) @@ -97,7 +96,6 @@ namespace spot if (const state* d = seen.is_new(it->current_state())) todo.push_back(d); } - delete it; } return all_accepting; } diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index dee758b3e..2f64694f4 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -156,12 +156,10 @@ namespace spot void add_to_map(const std::list& list, map_constraint& feed_me) { - for (std::list::const_iterator it = list.begin(); - it != list.end(); - ++it) + for (auto& p: list) { - if (feed_me.find(it->first) == feed_me.end()) - feed_me[it->first] = it->second; + if (feed_me.find(p.first) == feed_me.end()) + feed_me[p.first] = p.second; } } @@ -434,13 +432,8 @@ namespace spot // We fetch the result the run of acc_compl_automaton which // has recorded all the state in a hash table, and we set all // to init. - for (map_state_bdd::iterator it - = acc_compl.previous_class_.begin(); - it != acc_compl.previous_class_.end(); - ++it) - { - previous_class_[it->first] = init; - } + for (auto& p: acc_compl.previous_class_) + previous_class_[p.first] = init; // Put all the anonymous variable in a queue, and record all // of these in a variable all_class_var_ which will be used @@ -481,26 +474,21 @@ namespace spot // We run through the map bdd/list, and we update // the previous_class_ with the new data. - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + for (auto& p: bdd_lstate_) { - for (std::list::iterator it_s = it->second.begin(); - it_s != it->second.end(); - ++it_s) - { - // If the signature of a state is bddfalse (no - // transitions) the class of this state is bddfalse - // instead of an anonymous variable. It allows - // simplifications in the signature by removing a - // transition which has as a destination a state with - // no outgoing transition. - if (it->first == bddfalse) - previous_class_[*it_s] = bddfalse; - else - previous_class_[*it_s] = *it_bdd; - } - ++it_bdd; + // If the signature of a state is bddfalse (no + // transitions) the class of this state is bddfalse + // instead of an anonymous variable. It allows + // simplifications in the signature by removing a + // transition which has as a destination a state with + // no outgoing transition. + if (p.first == bddfalse) + for (auto s: p.second) + previous_class_[s] = bddfalse; + else + for (auto s: p.second) + previous_class_[s] = *it_bdd; + ++it_bdd; } } @@ -533,10 +521,9 @@ namespace spot // Take a state and compute its signature. bdd compute_sig(const state* src) { - tgba_succ_iterator* sit = a_->succ_iter(src); bdd res = bddfalse; - for (sit->first(); !sit->done(); sit->next()) + for (auto sit: a_->succ(src)) { const state* dst = sit->current_state(); bdd acc = bddtrue; @@ -574,7 +561,6 @@ namespace spot if (Cosimulation && initial_state == src) res |= bdd_initial; - delete sit; return res; } @@ -585,12 +571,9 @@ namespace spot // all the reachable states of this automaton. We do not // have to make (again) a traversal. We just have to run // through this map. - for (std::list::const_iterator it = order_.begin(); - it != order_.end(); - ++it) + for (auto s: order_) { - const state* src = previous_class_.find(*it)->first; - + const state* src = previous_class_.find(s)->first; bdd_lstate_[compute_sig(src)].push_back(src); } } @@ -636,22 +619,17 @@ namespace spot std::list::iterator it_bdd = used_var_.begin(); - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + for (auto& p: bdd_lstate_) { - // If the signature of a state is bddfalse (which is - // roughly equivalent to no transition) the class of - // this state is bddfalse instead of an anonymous - // variable. It allows simplifications in the signature - // by removing a transition which has as a destination a - // state with no outgoing transition. - if (it->first == bddfalse) - now_to_next[it->first] = bddfalse; - else - now_to_next[it->first] = *it_bdd; - - ++it_bdd; + // If the signature of a state is bddfalse (no + // transitions) the class of this state is bddfalse + // instead of an anonymous variable. It allows + // simplifications in the signature by removing a + // transition which has as a destination a state with + // no outgoing transition. + now_to_next[p.first] = + (p.first == bddfalse) ? bddfalse : *it_bdd; + ++it_bdd; } update_po(now_to_next, relation_); @@ -745,11 +723,10 @@ namespace spot bdd nonapvars = sup_all_acc & bdd_support(all_class_var_); // Create one state per partition. - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); ++it) + for (auto& p: bdd_lstate_) { res->add_state(++current_max); - bdd part = previous_class_[*it->second.begin()]; + bdd part = previous_class_[*p.second.begin()]; // The difference between the two next lines is: // the first says "if you see A", the second "if you @@ -771,12 +748,10 @@ namespace spot // For each partition, we will create // all the transitions between the states. - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + for (auto& p: bdd_lstate_) { // Get the signature. - bdd sig = compute_sig(*(it->second.begin())); + bdd sig = compute_sig(*(p.second.begin())); if (Cosimulation) sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); @@ -840,7 +815,7 @@ namespace spot // know the source, we must take a random state in // the list which is in the class we currently // work on. - int src = bdd2state[previous_class_[*it->second.begin()]]; + int src = bdd2state[previous_class_[*p.second.begin()]]; int dst = bdd2state[dest]; if (Cosimulation) @@ -875,15 +850,13 @@ namespace spot for (unsigned snum = current_max; snum > 0; --snum) { const state* s = res->get_state(snum); - tgba_succ_iterator* it = res->succ_iter(s); bdd acc = accst[snum]; - for (it->first(); !it->done(); it->next()) + for (auto it: res->succ(s)) { tgba_explicit_number::transition* t = res->get_transition(it); t->acceptance_conditions = acc; } - delete it; } res_is_deterministic = nb_minato == nb_satoneset; @@ -899,33 +872,23 @@ namespace spot // where is the new class name. void print_partition() { - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + for (auto& p: bdd_lstate_) { std::cerr << "partition: " - << bdd_format_isop(a_->get_dict(), it->first) + << bdd_format_isop(a_->get_dict(), p.first) << std::endl; - - for (std::list::iterator it_s = it->second.begin(); - it_s != it->second.end(); - ++it_s) - { - std::cerr << " - " - << a_->format_state(*it_s) << std::endl; - } + for (auto s: p.second) + std::cerr << " - " << a_->format_state(s) << '\n'; } std::cerr << "\nPrevious iteration\n" << std::endl; - for (map_state_bdd::const_iterator it = previous_class_.begin(); - it != previous_class_.end(); - ++it) + for (auto p: previous_class_) { - std::cerr << a_->format_state(it->first) + std::cerr << a_->format_state(p.first) << " was in " - << bdd_format_set(a_->get_dict(), it->second) - << std::endl; + << bdd_format_set(a_->get_dict(), p.second) + << '\n'; } } @@ -1039,13 +1002,12 @@ namespace spot // signature later. bdd dont_care_compute_sig(const state* src) { - tgba_succ_iterator* sit = a_->succ_iter(src); bdd res = bddfalse; unsigned scc = scc_map_->scc_of_state(old_name_[src]); bool sccacc = scc_map_->accepting(scc); - for (sit->first(); !sit->done(); sit->next()) + for (auto sit: a_->succ(src)) { const state* dst = sit->current_state(); bdd cl = previous_class_[dst]; @@ -1061,8 +1023,6 @@ namespace spot bdd to_add = acc & sit->current_condition() & relation_[cl]; res |= to_add; } - - delete sit; return res; } @@ -1315,22 +1275,15 @@ namespace spot } // Iterate over the transitions of both states. - for (map_bdd_bdd::const_iterator lit = sigl_map.begin(); - lit != sigl_map.end(); ++lit) - for (map_bdd_bdd::iterator rit = sigr_map.begin(); - rit != sigr_map.end(); ++rit) - { - // And create constraints if any of the transitions - // is out of the SCC and the left could imply the right. - if ((is_out_scc(lit->second) || is_out_scc(rit->second)) - && (bdd_exist(lit->first, on_cycle_) == - bdd_exist(rit->first, on_cycle_))) - { - create_simple_constraint(lit->second, rit->second, - left, right, res); - } - } - + for (auto lp: sigl_map) + for (auto rp: sigr_map) + // And create constraints if any of the transitions + // is out of the SCC and the left could imply the right. + if ((is_out_scc(lp.second) || is_out_scc(rp.second)) + && (bdd_exist(lp.first, on_cycle_) == + bdd_exist(rp.first, on_cycle_))) + create_simple_constraint(lp.second, rp.second, + left, right, res); return res; } @@ -1358,11 +1311,9 @@ namespace spot bdd_lstate_.clear(); // Compute the don't care signature for all the states. - for (std::list::const_iterator my_it = order_.begin(); - my_it != order_.end(); - ++my_it) + for (auto s: order_) { - map_state_bdd::iterator it = previous_class_.find(*my_it); + map_state_bdd::iterator it = previous_class_.find(s); const state* src = it->first; bdd sig = dont_care_compute_sig(src); @@ -1384,12 +1335,8 @@ namespace spot constraint_list cc; - for (map_bdd_bdd::iterator it = relation.begin(); - it != relation.end(); - ++it) - { - revert_relation_[it->second] = class2state[it->first]; - } + for (auto p: relation) + revert_relation_[p.second] = class2state[p.first]; int number_constraints = 0; relation_ = relation; @@ -1397,11 +1344,9 @@ namespace spot // order_ is here for the determinism. Here we make the diff // between the two tables: imply and could_imply. - for (std::list::const_iterator my_it = order_.begin(); - my_it != order_.end(); - ++my_it) + for (auto s: order_) { - map_state_bdd::iterator it = previous_class_.find(*my_it); + map_state_bdd::iterator it = previous_class_.find(s); assert(relation.find(it->second) != relation.end()); assert(dont_care_relation.find(it->second) != dont_care_relation.end()); diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 3be52ccc7..c57236b04 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.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 +// Developpement 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. @@ -189,8 +189,7 @@ namespace spot << std::endl; typename heap::color_ref c = h.get_color_ref(f.s); assert(!c.is_white()); - tgba_succ_iterator* i = a_->succ_iter(f.s); - for (i->first(); !i->done(); i->next()) + for (auto i: a_->succ(f.s)) { inc_transitions(); const state *s_prime = i->current_state(); @@ -211,7 +210,6 @@ namespace spot dfs_red(acu); } } - delete i; if (c.get_acc() == all_cond) { trace << "DFS_BLUE propagation is successful, report a" diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc index 5a5f75022..17b882f5c 100644 --- a/src/tgbatest/explicit2.cc +++ b/src/tgbatest/explicit2.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,16 +39,13 @@ create_tgba_explicit_string(bdd_dict* d) tgba->create_transition(s1, s2); (void) t; - tgba_explicit_succ_iterator* it - = tgba->succ_iter(tgba->get_init_state()); - for (it->first(); !it->done(); it->next()) + for (auto it: tgba->succ(tgba->get_init_state())) { - state_explicit_string* se = it->current_state(); + state_explicit_string* se = + down_cast(it->current_state()); std::cout << se->label() << std::endl; se->destroy(); } - delete it; - delete tgba; } @@ -63,16 +61,13 @@ create_tgba_explicit_number(bdd_dict* d) tgba->create_transition(s1, s2); (void) t; - tgba_explicit_succ_iterator* it = - tgba->succ_iter(tgba->get_init_state()); - for (it->first(); !it->done(); it->next()) + for (auto it: tgba->succ(tgba->get_init_state())) { - state_explicit_number* s = it->current_state(); + state_explicit_number* s = + down_cast(it->current_state()); std::cout << s->label() << std::endl; s->destroy(); } - - delete it; delete tgba; } @@ -89,16 +84,13 @@ create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) tgba->create_transition(s1, s2); (void) t; - tgba_explicit_succ_iterator* it = - tgba->succ_iter(tgba->get_init_state()); - for (it->first(); !it->done(); it->next()) + for (auto it: tgba->succ(tgba->get_init_state())) { - state_explicit_formula* s = it->current_state(); + state_explicit_formula* s = + down_cast(it->current_state()); to_string(s->label(), std::cout) << std::endl; s->destroy(); } - - delete it; delete tgba; }