diff --git a/NEWS b/NEWS index ed07a01af..20c027cbb 100644 --- a/NEWS +++ b/NEWS @@ -50,6 +50,7 @@ New in spot 1.99.5a (not yet released) * Renamings: is_guarantee_automaton() -> is_terminal_automaton() + tgba_run -> twa_run Python: * Add bindings for is_unambiguous(). diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index e3e9be924..a7247ec33 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -178,7 +178,7 @@ public: { auto run = res->accepting_run(); assert(run); - spot::tgba_word w(run->reduce()); + spot::twa_word w(run->reduce()); w.simplify(); std::ostringstream out; w.print(out, aut->get_dict()); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index a7eb6ce88..13b9e5885 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -693,7 +693,7 @@ namespace { std::cerr << "; both automata accept the infinite word\n" << " "; - spot::tgba_word w(run->reduce()); + spot::twa_word w(run->reduce()); w.simplify(); w.print(example(), prod->get_dict()) << '\n'; } diff --git a/src/twaalgos/word.cc b/src/twaalgos/word.cc index 6306a1d59..f708c16b5 100644 --- a/src/twaalgos/word.cc +++ b/src/twaalgos/word.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,18 +23,16 @@ namespace spot { - tgba_word::tgba_word(const twa_run_ptr run) + twa_word::twa_word(const twa_run_ptr run) { - for (twa_run::steps::const_iterator i = run->prefix.begin(); - i != run->prefix.end(); ++i) - prefix.push_back(i->label); - for (twa_run::steps::const_iterator i = run->cycle.begin(); - i != run->cycle.end(); ++i) - cycle.push_back(i->label); + for (auto& i: run->prefix) + prefix.push_back(i.label); + for (auto& i: run->cycle) + cycle.push_back(i.label); } void - tgba_word::simplify() + twa_word::simplify() { // If all the formulas on the cycle are compatible, reduce the // cycle to a simple conjunction. @@ -45,8 +43,8 @@ namespace spot // !a|!b; b; a&b; cycle{a&b} { bdd all = bddtrue; - for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i) - all &= *i; + for (auto& i: cycle) + all &= i; if (all != bddfalse) { cycle.clear(); @@ -76,35 +74,32 @@ namespace spot // !a|!b; cycle{a&b} // can be reduced to // !a&!b; cycle{a&b} - for (seq_t::iterator i = prefix.begin(); i != prefix.end(); ++i) - *i = bdd_satone(*i); - for (seq_t::iterator i = cycle.begin(); i != cycle.end(); ++i) - *i = bdd_satone(*i); - + for (auto& i: prefix) + i = bdd_satone(i); + for (auto& i: cycle) + i = bdd_satone(i); } std::ostream& - tgba_word::print(std::ostream& os, const bdd_dict_ptr& d) const + twa_word::print(std::ostream& os, const bdd_dict_ptr& d) const { if (!prefix.empty()) - for (seq_t::const_iterator i = prefix.begin(); i != prefix.end(); ++i) + for (auto& i: prefix) { - bdd_print_formula(os, d, *i); + bdd_print_formula(os, d, i); os << "; "; } assert(!cycle.empty()); bool notfirst = false; os << "cycle{"; - for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i) + for (auto& i: cycle) { if (notfirst) os << "; "; notfirst = true; - bdd_print_formula(os, d, *i); + bdd_print_formula(os, d, i); } os << '}'; return os; } - - } diff --git a/src/twaalgos/word.hh b/src/twaalgos/word.hh index 8e832ba74..7b97fdc4a 100644 --- a/src/twaalgos/word.hh +++ b/src/twaalgos/word.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -26,9 +26,9 @@ namespace spot class bdd_dict; /// \brief An infinite word stored as a lasso. - struct SPOT_API tgba_word + struct SPOT_API twa_word { - tgba_word(const twa_run_ptr run); + twa_word(const twa_run_ptr run); void simplify(); std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const;