diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index faa545236..e6551571f 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -53,8 +53,8 @@ namespace spot for (set_type::iterator i = y->second.b.begin(); i != y->second.b.end(); ++i) { - tagged_state x = tags.find(*i); - assert(x != tags.end()); + tagged_state x = tags_.find(*i); + assert(x != tags_.end()); // insert y in A(x) x->second.del.erase(y->first); @@ -71,7 +71,7 @@ namespace spot enumerate_cycles::tag_state(const state* s) { std::pair p = - tags.insert(std::make_pair(s, state_info())); + tags_.insert(std::make_pair(s, state_info())); if (p.second) s->destroy(); return p.first; @@ -86,7 +86,7 @@ namespace spot e.ts = ts; e.succ = 0; e.f = false; - dfs.push_back(e); + dfs_.push_back(e); } void @@ -96,9 +96,9 @@ namespace spot push_state(tag_state(sm_.one_state_of(scc)->clone())); - while (keep_going && !dfs.empty()) + while (keep_going && !dfs_.empty()) { - dfs_entry& cur = dfs.back(); + dfs_entry& cur = dfs_.back(); if (cur.succ == 0) { cur.succ = aut_->succ_iter(cur.ts->first); @@ -142,46 +142,45 @@ namespace spot tagged_state v = cur.ts; delete cur.succ; - dfs.pop_back(); + dfs_.pop_back(); if (f) unmark(v); v->second.reach = true; // Update the predecessor in the stack if there is one. - if (!dfs.empty()) + if (!dfs_.empty()) { if (f) - dfs.back().f = true; + dfs_.back().f = true; else - nocycle(dfs.back().ts, v); + nocycle(dfs_.back().ts, v); } } } - // Purge the dfs stack, in case we aborted because cycle_found() - // said so. - while (!dfs.empty()) + // Purge the dfs_ stack, in case we aborted because cycle_found() + // returned false. + while (!dfs_.empty()) { - delete dfs.back().succ; - dfs.pop_back(); + delete dfs_.back().succ; + dfs_.pop_back(); } - - hash_type::iterator i = tags.begin(); - while (i != tags.end()) + hash_type::iterator i = tags_.begin(); + while (i != tags_.end()) { hash_type::iterator old = i; ++i; old->first->destroy(); } - tags.clear(); - dfs.clear(); + tags_.clear(); + dfs_.clear(); } bool enumerate_cycles::cycle_found(const state* start) { - dfs_stack::const_iterator i = dfs.begin(); + dfs_stack::const_iterator i = dfs_.begin(); while (i->ts->first != start) ++i; do @@ -189,7 +188,7 @@ namespace spot std::cout << aut_->format_state(i->ts->first) << " "; ++i; } - while (i != dfs.end()); + while (i != dfs_.end()); std::cout << "\n"; return true; } diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 53d0fff42..77d29d431 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -24,15 +24,13 @@ #include "scc.hh" #include "misc/hash.hh" #include -#include namespace spot { - - /// \brief Enumerate cycles from a SCC. - /// - /// This implements the algorithm on page 170 of: + /// \brief Enumerate elementary cycles in a SCC. /// + /// This class implements a non-recursive version of the algorithm + /// on page 170 of: /// \verbatim /// @Article{loizou.82.is, /// author = {George Loizou and Peter Thanisch}, @@ -46,25 +44,45 @@ namespace spot /// month = aug /// } /// \endverbatim + /// (the additional preprocessings described later in that paper are + /// not implemented). /// - /// (the additional preprocessing described in that paper is not - /// implemented). + /// It should be noted that although the above paper does not + /// consider multiple arcs and self-loops in its definitions, the + /// algorithm they present works as expected in these cases. /// - /// The class constructor takes an automaton, and an scc_map that - /// should already have been built for for automaton. Calling + /// For our purpose an elementary cycle is a sequence of transitions + /// that form a cycle and that visit a state at most once. We may + /// have two cycles that visit the same states in the same order if + /// some pair of states are connected by several transitions. Also + /// A cycle may visit only one state if it is a self-loop. + /// + /// We represent a cycle by a sequence of succ_iterator objects + /// positioned on the transition contributing to the cycle. These + /// succ_itertor are stored, along with their source state, in the + /// dfs_ stack. Only the last portion of this stack may form a + /// cycle. + /// + /// The class constructor takes an automaton and an scc_map that + /// should already have been built for that automaton. Calling /// run(n) will enumerate all elementary cycles in SCC #n. Each - /// time an SCC is found, the method cycle_found() is called with - /// the initial state of the cycle (the cycle is constituted from - /// all the states that are on the dfs stack after this starting - /// state). When if cycle_found() returns false, the run() method - /// will terminate. If it returns true, the run() method will - /// search the next elementary cycle. + /// time an SCC is found, the method cycle_found(s) is called with + /// the initial state s of the cycle: the cycle is constituted from + /// all the states that are on the dfs_ stack after s (including s). + /// + /// You should inherit from this class and redefine the + /// cycle_found() method to perform any work you would like to do on + /// the enumerated cycles. If cycle_found() returns false, the + /// run() method will terminate. If it returns true, the run() + /// method will search for the next elementary cycle and call + /// cycle_found() again if it finds another cycle. class enumerate_cycles { protected: typedef Sgi::hash_set set_type; + // Extra information required for the algorithm for each state. struct state_info { // Whether the state has already left the stack at least once. @@ -77,38 +95,31 @@ namespace spot bool mark; // Deleted successors (in the paper, states deleted from A(x)) set_type del; - // Predecessors of the current states, that could not yet // contribute to a cycle. set_type b; }; + // Store the state_info for all visited states. typedef Sgi::hash_map hash_type; + hash_type tags_; + // A tagged_state s is a state* (s->first) associated to its + // state_info (s->second). We usually handled tagged_state in the + // algorithm to avoid repeated lookup of the state_info data. typedef hash_type::iterator tagged_state; - public: - enumerate_cycles(const tgba* aut, const scc_map& map); - - // Run in SCC scc, and call cycle_found() for any new elementary - // cycle found. - void run(unsigned scc); - - void nocycle(tagged_state x, tagged_state y); - void unmark(tagged_state y); - - // Called whenever a cycle was found. The cycles uses all the - // states from the dfs stack, starting from \a start. - virtual bool cycle_found(const state* start); - - tagged_state tag_state(const state* s); - void push_state(tagged_state ts); - - protected: + // The automaton we are working on. const tgba* aut_; + // The SCC map built for aut_. const scc_map& 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 + // cycle_found()). struct dfs_entry { tagged_state ts; @@ -116,9 +127,43 @@ namespace spot bool f; }; typedef std::deque dfs_stack; - dfs_stack dfs; + dfs_stack dfs_; - hash_type tags; + public: + enumerate_cycles(const tgba* aut, const scc_map& map); + + /// \brief Run in SCC scc, and call \a cycle_found() for any new + /// elementary cycle found. + /// + /// It is safe to call this method multiple times, for instance to + /// enumerate the cycle of each SCC. + void run(unsigned scc); + + + /// \brief Called whenever a cycle was found. + /// + /// The cycle uses all the states from the dfs stack, starting + /// from the one labeled \a start. The iterators in the DFS stack + /// are all pointing to the transition considered for the cycle. + /// + /// This method is not const so you can modify private variables + /// to your subclass, but it should definitely NOT modify the dfs + /// stack or the tags map. + /// + /// The default implementation, not very useful, will print the + /// states in the cycle on std::cout. + virtual bool cycle_found(const state* 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); + // 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); + // unmark the state y (sub-procedure from the paper) + void unmark(tagged_state y); }; } diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 5409fdd17..5a9dc13c7 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -27,6 +27,7 @@ namespace spot { namespace { + // Look for a non-accepting cycle. class weak_checker: public enumerate_cycles { public: @@ -40,16 +41,16 @@ namespace spot virtual bool cycle_found(const state* start) { - dfs_stack::const_iterator i = dfs.begin(); + dfs_stack::const_reverse_iterator i = dfs_.rbegin(); bdd acc = bddfalse; - while (i->ts->first != start) - ++i; - do + for (;;) { acc |= i->succ->current_acceptance_conditions(); + if (i->ts->first == start) + break; ++i; + assert(i != dfs_.rend()); } - while (i != dfs.end()); if (acc != aut_->all_acceptance_conditions()) { // We have found an non-accepting cycle, so the SCC is not diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index b52f06c57..931bb333d 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -30,14 +30,14 @@ namespace spot /// \brief Whether the SCC number \a scc in \a aut is weak. /// - /// An SCC is weak if its cycles are all accepting, or the are all - /// non-accepting. + /// An SCC is weak if either its cycles are all accepting, or they + /// are all non-accepting. /// /// The scc_map \a map should have been built already. The absence /// of accepting cycle is easy to check (the scc_map can tell /// whether the SCC is non-accepting already). For the accepting - /// SCC, this function works by enumerating all cycles in the given - /// SCC (it stops if it find a non-accepting cycle). + /// SCCs, this function enumerates all cycles in the given SCC (it + /// stops if it find a non-accepting cycle). bool is_weak_scc(const tgba* aut, scc_map& map, unsigned scc); /// @}