From b4c125c2b97a21dd12abfa1140810680c48ed0b1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 27 Jan 2014 00:00:22 +0100 Subject: [PATCH] Avoid calling done(), as enabled by last patch. * src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc, src/tgbaalgos/cycles.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/reachiter.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc: Avoid calls to done(). --- src/tgbaalgos/bfssteps.cc | 5 +- src/tgbaalgos/complete.cc | 19 ++++---- src/tgbaalgos/cycles.cc | 7 +-- src/tgbaalgos/dtgbacomp.cc | 8 ++-- src/tgbaalgos/gtec/gtec.cc | 38 ++++++++------- src/tgbaalgos/gv04.cc | 7 +-- src/tgbaalgos/isweakscc.cc | 6 +-- src/tgbaalgos/lbtt.cc | 5 +- src/tgbaalgos/neverclaim.cc | 9 ++-- src/tgbaalgos/reachiter.cc | 44 +++++++++-------- src/tgbaalgos/replayrun.cc | 96 +++++++++++++++++++------------------ src/tgbaalgos/safety.cc | 3 +- src/tgbaalgos/save.cc | 33 +++++++------ 13 files changed, 143 insertions(+), 137 deletions(-) diff --git a/src/tgbaalgos/bfssteps.cc b/src/tgbaalgos/bfssteps.cc index 3ca065434..eb9eb4db4 100644 --- a/src/tgbaalgos/bfssteps.cc +++ b/src/tgbaalgos/bfssteps.cc @@ -72,8 +72,7 @@ namespace spot { const state* src = todo.front(); todo.pop_front(); - tgba_succ_iterator* i = a_->succ_iter(src); - for (i->first(); !i->done(); i->next()) + for (auto i: a_->succ(src)) { const state* dest = filter(i->current_state()); @@ -88,7 +87,6 @@ namespace spot { // Found it! finalize(father, s, start, l); - a_->release_iter(i); return dest; } @@ -100,7 +98,6 @@ namespace spot father[dest] = s; } } - a_->release_iter(i); } return 0; } diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index ffee42406..b24b57465 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.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. // // This file is part of Spot, a model checking library. @@ -81,13 +81,16 @@ namespace spot // add a transition to a sink state if the state is not complete. bdd all = bddtrue; bdd acc = bddfalse; - i->first(); - // In case the automaton use state-based acceptance, propagate - // the acceptance of the first transition to the one we add. - if (!i->done()) - acc = i->current_acceptance_conditions(); - for (; !i->done(); i->next()) - all -= i->current_condition(); + if (i->first()) + { + // In case the automaton use state-based acceptance, propagate + // the acceptance of the first transition to the one we add. + acc = i->current_acceptance_conditions(); + + do + all -= i->current_condition(); + while (i->next()); + } if (all != bddfalse) { trans* t = out_->create_transition(n, 0); diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index ba2e937a9..f5537ca87 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -95,14 +95,15 @@ namespace spot while (keep_going && !dfs_.empty()) { dfs_entry& cur = dfs_.back(); + bool cont; if (cur.succ == 0) { cur.succ = aut_->succ_iter(cur.ts->first); - cur.succ->first(); + cont = cur.succ->first(); } else - cur.succ->next(); - if (!cur.succ->done()) + cont = cur.succ->next(); + if (cont) { // Explore one successor. diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index ec7c94762..bd3ef2c89 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.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. // // This file is part of Spot, a model checking library. @@ -78,8 +78,10 @@ namespace spot { // add a transition to a sink state if the state is not complete. bdd all = bddtrue; - for (i->first(); !i->done(); i->next()) - all -= i->current_condition(); + if (i->first()) + do + all -= i->current_condition(); + while (i->next()); if (all != bddfalse) { trans* t = out_->create_transition(n, 0); diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 03e44f6cf..035393b1c 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -115,27 +115,29 @@ namespace spot for (;;) { // Remove each destination of this iterator. - for (i->first(); !i->done(); i->next()) - { - inc_transitions(); + if (i->first()) + do + { + inc_transitions(); - state* s = i->current_state(); - numbered_state_heap::state_index_p spi = ecs_->h->index(s); + state* s = i->current_state(); + numbered_state_heap::state_index_p spi = ecs_->h->index(s); - // This state is not necessary in H, because if we were - // doing inclusion checking during the emptiness-check - // (redefining find()), the index `s' can be included in a - // larger state and will not be found by index(). We can - // safely ignore such states. - if (!spi.first) - continue; + // This state is not necessary in H, because if we were + // doing inclusion checking during the emptiness-check + // (redefining find()), the index `s' can be included in a + // larger state and will not be found by index(). We can + // safely ignore such states. + if (!spi.first) + continue; - if (*spi.second != -1) - { - *spi.second = -1; - to_remove.push(ecs_->aut->succ_iter(spi.first)); - } - } + if (*spi.second != -1) + { + *spi.second = -1; + to_remove.push(ecs_->aut->succ_iter(spi.first)); + } + } + while (i->next()); ecs_->aut->release_iter(i); if (to_remove.empty()) break; diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 245944cb6..5b65d66cd 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -106,17 +106,18 @@ namespace spot << ")" << std::endl; tgba_succ_iterator* iter = stack[dftop].lasttr; + bool cont; if (!iter) { iter = stack[dftop].lasttr = a_->succ_iter(stack[dftop].s); - iter->first(); + cont = iter->first(); } else { - iter->next(); + cont = iter->next(); } - if (iter->done()) + if (!cont) { trace << " No more successors" << std::endl; pop(); diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 72358270b..806489f83 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -134,10 +134,9 @@ namespace spot for (auto s: map.states_of(scc)) { tgba_succ_iterator* it = a->succ_iter(s); - it->first(); // If a state has no successors, the SCC is not complete. - if (it->done()) + if (!it->first()) { a->release_iter(it); return false; @@ -154,9 +153,8 @@ namespace spot next->destroy(); if (sumall == bddtrue) break; - it->next(); } - while (!it->done()); + while (it->next()); a->release_iter(it); if (sumall != bddtrue) diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 3c4c17e7c..44dd11d64 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -101,9 +101,8 @@ namespace spot // is not terribly efficient since we have to create the // iterator. tgba_succ_iterator* it = aut_->succ_iter(s); - it->first(); - bool accepting = - !it->done() && it->current_acceptance_conditions() == all_acc_conds_; + bool accepting = it->first() + && it->current_acceptance_conditions() == all_acc_conds_; aut_->release_iter(it); return accepting; } diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index ba36f1bde..9db285494 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -86,9 +86,8 @@ namespace spot // is not terribly efficient since we have to create the // iterator. tgba_succ_iterator* it = aut_->succ_iter(s); - it->first(); bool accepting = - !it->done() && it->current_acceptance_conditions() == all_acc_conds_; + it->first() && it->current_acceptance_conditions() == all_acc_conds_; aut_->release_iter(it); return accepting; } @@ -111,8 +110,7 @@ namespace spot if (state_is_accepting(s)) { tgba_succ_iterator* it = aut_->succ_iter(s); - it->first(); - if (it->done()) + if (!it->first()) label = "accept_S" + ns; else { @@ -136,8 +134,7 @@ namespace spot process_state(const state* s, int n, tgba_succ_iterator*) { tgba_succ_iterator* it = aut_->succ_iter(s); - it->first(); - if (it->done()) + if (!it->first()) { if (fi_needed_ != 0) os_ << " fi;\n"; diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index edc090065..d115c50c7 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -61,27 +61,29 @@ namespace spot int tn = seen[t]; tgba_succ_iterator* si = aut_->succ_iter(t); process_state(t, tn, si); - for (si->first(); !si->done(); si->next()) - { - const state* current = si->current_state(); - seen_map::const_iterator s = seen.find(current); - bool ws = want_state(current); - if (s == seen.end()) - { - seen[current] = ++n; - if (ws) - { - add_state(current); - process_link(t, tn, current, n, si); - } - } - else - { - if (ws) - process_link(t, tn, s->first, s->second, si); - current->destroy(); - } - } + if (si->first()) + do + { + const state* current = si->current_state(); + seen_map::const_iterator s = seen.find(current); + bool ws = want_state(current); + if (s == seen.end()) + { + seen[current] = ++n; + if (ws) + { + add_state(current); + process_link(t, tn, current, n, si); + } + } + else + { + if (ws) + process_link(t, tn, s->first, s->second, si); + current->destroy(); + } + } + while (si->next()); aut_->release_iter(si); } end(); diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index ed579f061..0d109bdab 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -62,14 +62,14 @@ namespace spot l = &run->cycle; in = "cycle"; if (!debug) - os << "No prefix.\nCycle:" << std::endl; + os << "No prefix.\nCycle:\n"; } else { l = &run->prefix; in = "prefix"; if (!debug) - os << "Prefix:" << std::endl; + os << "Prefix:\n"; } tgba_run::steps::const_iterator i = l->begin(); @@ -78,9 +78,9 @@ namespace spot { if (debug) os << "ERROR: First state of run (in " << in << "): " - << a->format_state(i->s) << std::endl - << "does not match initial state of automata: " - << a->format_state(s) << std::endl; + << a->format_state(i->s) + << "\ndoes not match initial state of automata: " + << a->format_state(s) << '\n'; s->destroy(); return false; } @@ -112,7 +112,7 @@ namespace spot { os << " "; } - os << a->format_state(s) << std::endl; + os << a->format_state(s) << '\n'; // expected outgoing transition bdd label = i->label; @@ -133,7 +133,7 @@ namespace spot in = "cycle"; i = l->begin(); if (!debug) - os << "Cycle:" << std::endl; + os << "Cycle:\n"; } next = l->begin()->s; } @@ -144,24 +144,26 @@ namespace spot // destroy it right now. if (!debug) s->destroy(); - for (j->first(); !j->done(); j->next()) - { - if (j->current_condition() != label - || j->current_acceptance_conditions() != acc) - continue; - - const state* s2 = j->current_state(); - if (s2->compare(next)) - { - s2->destroy(); + if (j->first()) + do + { + if (j->current_condition() != label + || j->current_acceptance_conditions() != acc) continue; - } - else - { - s = s2; - break; - } - } + + const state* s2 = j->current_state(); + if (s2->compare(next)) + { + s2->destroy(); + continue; + } + else + { + s = s2; + break; + } + } + while (j->next()); if (j->done()) { if (debug) @@ -170,24 +172,26 @@ namespace spot << bdd_format_formula(a->get_dict(), label) << " and acc=" << bdd_format_accset(a->get_dict(), acc) << " leaving state " << serial - << " for state " << a->format_state(next) - << std::endl + << " for state " << a->format_state(next) << '\n' << "The following transitions leave state " << serial - << ":" << std::endl; - for (j->first(); !j->done(); j->next()) - { - const state* s2 = j->current_state(); - os << " *"; - print_annotation(os, a, j); - os << " label=" - << bdd_format_formula(a->get_dict(), - j->current_condition()) - << " and acc=" - << bdd_format_accset(a->get_dict(), - j->current_acceptance_conditions()) - << " going to " << a->format_state(s2) << std::endl; - s2->destroy(); - } + << ":\n"; + if (j->first()) + do + { + const state* s2 = j->current_state(); + os << " *"; + print_annotation(os, a, j); + os << " label=" + << bdd_format_formula(a->get_dict(), + j->current_condition()) + << " and acc=" + << (bdd_format_accset + (a->get_dict(), + j->current_acceptance_conditions())) + << " going to " << a->format_state(s2) << '\n'; + s2->destroy(); + } + while (j->next()); } a->release_iter(j); s->destroy(); @@ -228,8 +232,7 @@ namespace spot if (debug) os << "all acceptance conditions (" << bdd_format_accset(a->get_dict(), all_acc) - << ") have been seen" - << std::endl; + << ") have been seen\n"; } } } @@ -238,11 +241,10 @@ namespace spot { if (debug) os << "ERROR: The cycle's acceptance conditions (" - << bdd_format_accset(a->get_dict(), all_acc) << ") do not" - << std::endl - << "match those of the automata (" + << bdd_format_accset(a->get_dict(), all_acc) + << ") do not\nmatch those of the automaton (" << bdd_format_accset(a->get_dict(), expected_all_acc) - << std::endl; + << ")\n"; return false; } diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 1c66609a2..6b04b5680 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -57,8 +57,7 @@ namespace spot assert(!it->done()); state* dest = it->current_state(); bdd cond = it->current_condition(); - it->next(); - result = (!dest->compare(s)) && it->done() && (cond == bddtrue); + result = (!it->next()) && (cond == bddtrue) && (!dest->compare(s)); dest->destroy(); aut->release_iter(it); } diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index c0f328718..327e478bc 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 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. +// 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. // @@ -51,17 +52,19 @@ namespace spot { const bdd_dict* d = aut_->get_dict(); std::string cur = escape_str(aut_->format_state(s)); - for (si->first(); !si->done(); si->next()) - { - state* dest = si->current_state(); - os_ << "\"" << cur << "\", \""; - escape_str(os_, aut_->format_state(dest)); - os_ << "\", \""; - escape_str(os_, bdd_format_formula(d, si->current_condition())); - os_ << "\","; - print_acc(si->current_acceptance_conditions()) << ";\n"; - dest->destroy(); - } + if (si->first()) + do + { + state* dest = si->current_state(); + os_ << "\"" << cur << "\", \""; + escape_str(os_, aut_->format_state(dest)); + os_ << "\", \""; + escape_str(os_, bdd_format_formula(d, si->current_condition())); + os_ << "\","; + print_acc(si->current_acceptance_conditions()) << ";\n"; + dest->destroy(); + } + while (si->next()); } private: