diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index df408d6cb..74a17560b 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,23 +23,25 @@ namespace spot { enumerate_cycles::enumerate_cycles(const scc_info& map) - : aut_(map.get_aut()), sm_(map) + : aut_(map.get_aut()), + info_(aut_->num_states(), aut_->num_states()), + sm_(map) { } void - enumerate_cycles::nocycle(tagged_state x, tagged_state y) + enumerate_cycles::nocycle(unsigned x, unsigned y) { // insert x in B(y) - y->second.b.insert(x->first); + info_[y].b.push_back(x); // remove y from A(x) - x->second.del.insert(y->first); + info_[x].del[y] = true; } void - enumerate_cycles::unmark(tagged_state y) + enumerate_cycles::unmark(unsigned y) { - std::deque q; + std::vector q; q.push_back(y); while (!q.empty()) @@ -47,102 +49,82 @@ namespace spot y = q.back(); q.pop_back(); - y->second.mark = false; - for (auto s: y->second.b) + info_[y].mark = false; + for (auto x: info_[y].b) { - tagged_state x = tags_.find(s); - assert(x != tags_.end()); + assert(info_[x].seen); // insert y in A(x) - x->second.del.erase(y->first); + info_[x].del[y] = false; // unmark x recursively if marked - if (x->second.mark) + if (info_[x].mark) q.push_back(x); } // empty B(y) - y->second.b.clear(); + info_[y].b.clear(); } } - enumerate_cycles::tagged_state - enumerate_cycles::tag_state(const state* s) - { - auto p = tags_.emplace(s, state_info()); - if (!p.second) - s->destroy(); - return p.first; - } - void - enumerate_cycles::push_state(tagged_state ts) + enumerate_cycles::push_state(unsigned s) { - ts->second.mark = true; - - dfs_entry e; - e.ts = ts; - e.succ = 0; - e.f = false; - dfs_.push_back(e); + info_[s].mark = true; + dfs_.emplace_back(s); } - // FIXME: Recode this algorithm using unsigned states. void enumerate_cycles::run(unsigned scc) { bool keep_going = true; - push_state(tag_state(aut_->state_from_number(sm_.one_state_of(scc)))); + { + unsigned s = sm_.one_state_of(scc); + info_[s].seen = true; + push_state(s); + } while (keep_going && !dfs_.empty()) { dfs_entry& cur = dfs_.back(); - bool cont; if (cur.succ == 0) - { - cur.succ = aut_->succ_iter(cur.ts->first); - cont = cur.succ->first(); - } + cur.succ = aut_->get_graph().state_storage(cur.s).succ; else - cont = cur.succ->next(); - if (cont) + cur.succ = aut_->trans_storage(cur.succ).next_succ; + if (cur.succ) { // Explore one successor. // Ignore those that are not on the SCC, or destination // that have been "virtually" deleted from A(v). - state* s = cur.succ->current_state(); - if ((sm_.scc_of(aut_->state_number(s)) != scc) - || (cur.ts->second.del.find(s) != cur.ts->second.del.end())) - { - s->destroy(); - continue; - } + unsigned s = aut_->trans_storage(cur.succ).dst; - tagged_state w = tag_state(s); - if (!w->second.mark) + if ((sm_.scc_of(s) != scc) || (info_[cur.s].del[s])) + continue; + + info_[s].seen = true; + if (!info_[s].mark) { - push_state(w); + push_state(s); } - else if (!w->second.reach) + else if (!info_[s].reach) { - keep_going = cycle_found(w->first); + keep_going = cycle_found(s); cur.f = true; } else { - nocycle(cur.ts, w); + nocycle(cur.s, s); } } else { // No more successors. bool f = cur.f; - tagged_state v = cur.ts; - aut_->release_iter(cur.succ); + unsigned v = cur.s; dfs_.pop_back(); if (f) unmark(v); - v->second.reach = true; + info_[v].reach = true; // Update the predecessor in the stack if there is one. if (!dfs_.empty()) @@ -150,39 +132,25 @@ namespace spot if (f) dfs_.back().f = true; else - nocycle(dfs_.back().ts, v); + nocycle(dfs_.back().s, v); } } } // Purge the dfs_ stack, in case we aborted because cycle_found() // returned false. - while (!dfs_.empty()) - { - aut_->release_iter(dfs_.back().succ); - dfs_.pop_back(); - } - - hash_type::iterator i = tags_.begin(); - while (i != tags_.end()) - { - hash_type::iterator old = i; - ++i; - old->first->destroy(); - } - tags_.clear(); dfs_.clear(); } bool - enumerate_cycles::cycle_found(const state* start) + enumerate_cycles::cycle_found(unsigned start) { dfs_stack::const_iterator i = dfs_.begin(); - while (i->ts->first != start) + while (i->s != start) ++i; do { - std::cout << aut_->format_state(i->ts->first) << ' '; + std::cout << i->s << ' '; ++i; } while (i != dfs_.end()); diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 387c65833..0ad06b571 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -80,10 +80,11 @@ namespace spot // Extra information required for the algorithm for each state. struct state_info { - state_info() - : reach(false), mark(false) + state_info(unsigned num) + : seen(false), reach(false), mark(false), del(num) { } + bool seen; // Whether the state has already left the stack at least once. bool reach; // set to true when the state current state w is stacked, and @@ -93,39 +94,34 @@ namespace spot // that a contributed to a contributed to a cycle. bool mark; // Deleted successors (in the paper, states deleted from A(x)) - state_set del; + std::vector del; // Predecessors of the current states, that could not yet // contribute to a cycle. - state_set b; + std::vector b; }; - // Store the state_info for all visited states. - typedef std::unordered_map hash_type; - hash_type tags_; - - // A tagged_state s is a state* (s->first) associated to its - // state_info (s->second). We usually handle tagged_state in the - // algorithm to avoid repeated lookup of the state_info data. - typedef hash_type::iterator tagged_state; - // The automaton we are working on. const_tgba_digraph_ptr aut_; + // Store the state_info for all visited states. + std::vector info_; // The SCC map built for aut_. const scc_info& sm_; - // The DFS stack. Each entry contains a tagged state, an iterator - // on the transitions leaving that state, and a Boolean f - // indicating whether this state as already contributed to a cycle - // (f is updated when backtracking, so it should not be used by + // The DFS stack. Each entry contains a state, an iterator on the + // transitions leaving that state, and a Boolean f indicating + // whether this state as already contributed to a cycle (f is + // updated when backtracking, so it should not be used by // cycle_found()). struct dfs_entry { - tagged_state ts; - tgba_succ_iterator* succ; - bool f; + unsigned s; + unsigned succ = 0U; + bool f = false; + dfs_entry(unsigned s): s(s) + { + } }; - typedef std::deque dfs_stack; + typedef std::vector dfs_stack; dfs_stack dfs_; public: @@ -155,18 +151,16 @@ namespace spot /// /// This method method should return false iff no more cycles need /// should be enumerated by run(). - virtual bool cycle_found(const state* start); + virtual bool cycle_found(unsigned start); private: - // introduce a new state to the tags map. - tagged_state tag_state(const state* s); // add a new state to the dfs_ stack - void push_state(tagged_state ts); + void push_state(unsigned s); // block the edge (x,y) because it cannot contribute to a new // cycle currently (sub-procedure from the paper) - void nocycle(tagged_state x, tagged_state y); + void nocycle(unsigned x, unsigned y); // unmark the state y (sub-procedure from the paper) - void unmark(tagged_state y); + void unmark(unsigned y); }; } diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 63f609963..edcf540ae 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,7 +26,7 @@ namespace spot namespace { // Look for a non-accepting cycle. - class weak_checker: public enumerate_cycles + class weak_checker final : public enumerate_cycles { public: bool result; @@ -37,14 +37,14 @@ namespace spot } virtual bool - cycle_found(const state* start) + cycle_found(unsigned start) override { dfs_stack::const_reverse_iterator i = dfs_.rbegin(); acc_cond::mark_t acc = 0U; for (;;) { - acc |= i->succ->current_acceptance_conditions(); - if (i->ts->first == start) + acc |= aut_->trans_storage(i->succ).acc; + if (i->s == start) break; ++i; // The const cast is here to please old g++ versions. diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 04af51319..f5c1c7adf 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -228,7 +228,7 @@ namespace spot namespace { - class fix_scc_acceptance: protected enumerate_cycles + class fix_scc_acceptance final: protected enumerate_cycles { public: typedef dfs_stack::const_iterator cycle_iter; @@ -304,9 +304,7 @@ namespace spot // Iterate on each original state corresponding to the // start of the loop in the determinized automaton. - const power_map::power_state& ps = - refmap_.states_of(a->state_number(begin->ts->first)); - for (auto s: ps) + for (auto s: refmap_.states_of(begin->s)) { // Check the product between LOOP_A, and ORIG_A starting // in S. @@ -330,22 +328,16 @@ namespace spot } virtual bool - cycle_found(const state* start) + cycle_found(unsigned start) override { cycle_iter i = dfs_.begin(); - while (i->ts->first != start) + while (i->s != start) ++i; trans_set ts; bool is_acc = is_cycle_accepting(i, ts); do - { - // std::cerr << aut_->format_state(i->ts->first) << ' '; - ++i; - } + ++i; while (i != dfs_.end()); - // std::cerr << " acc=" << is_acc << " ("; - // bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") "; - // print_set(std::cerr, ts) << '\n'; if (is_acc) { accept_.push_back(ts);