Commit 92e37998 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Better documentation for the cycle enumeration algorithms.

* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/isweakscc.hh: Improve .doc
* src/tgbaalgos/isweakscc.cc (weak_checker::cycle_found):
Scan the DFS backward so we only look at the cycle part.
parent 420fcd62
...@@ -53,8 +53,8 @@ namespace spot ...@@ -53,8 +53,8 @@ namespace spot
for (set_type::iterator i = y->second.b.begin(); for (set_type::iterator i = y->second.b.begin();
i != y->second.b.end(); ++i) i != y->second.b.end(); ++i)
{ {
tagged_state x = tags.find(*i); tagged_state x = tags_.find(*i);
assert(x != tags.end()); assert(x != tags_.end());
// insert y in A(x) // insert y in A(x)
x->second.del.erase(y->first); x->second.del.erase(y->first);
...@@ -71,7 +71,7 @@ namespace spot ...@@ -71,7 +71,7 @@ namespace spot
enumerate_cycles::tag_state(const state* s) enumerate_cycles::tag_state(const state* s)
{ {
std::pair<tagged_state, bool> p = std::pair<tagged_state, bool> p =
tags.insert(std::make_pair(s, state_info())); tags_.insert(std::make_pair(s, state_info()));
if (p.second) if (p.second)
s->destroy(); s->destroy();
return p.first; return p.first;
...@@ -86,7 +86,7 @@ namespace spot ...@@ -86,7 +86,7 @@ namespace spot
e.ts = ts; e.ts = ts;
e.succ = 0; e.succ = 0;
e.f = false; e.f = false;
dfs.push_back(e); dfs_.push_back(e);
} }
void void
...@@ -96,9 +96,9 @@ namespace spot ...@@ -96,9 +96,9 @@ namespace spot
push_state(tag_state(sm_.one_state_of(scc)->clone())); 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) if (cur.succ == 0)
{ {
cur.succ = aut_->succ_iter(cur.ts->first); cur.succ = aut_->succ_iter(cur.ts->first);
...@@ -142,46 +142,45 @@ namespace spot ...@@ -142,46 +142,45 @@ namespace spot
tagged_state v = cur.ts; tagged_state v = cur.ts;
delete cur.succ; delete cur.succ;
dfs.pop_back(); dfs_.pop_back();
if (f) if (f)
unmark(v); unmark(v);
v->second.reach = true; v->second.reach = true;
// Update the predecessor in the stack if there is one. // Update the predecessor in the stack if there is one.
if (!dfs.empty()) if (!dfs_.empty())
{ {
if (f) if (f)
dfs.back().f = true; dfs_.back().f = true;
else else
nocycle(dfs.back().ts, v); nocycle(dfs_.back().ts, v);
} }
} }
} }
// Purge the dfs stack, in case we aborted because cycle_found() // Purge the dfs_ stack, in case we aborted because cycle_found()
// said so. // returned false.
while (!dfs.empty()) while (!dfs_.empty())
{ {
delete dfs.back().succ; delete dfs_.back().succ;
dfs.pop_back(); dfs_.pop_back();
} }
hash_type::iterator i = tags_.begin();
hash_type::iterator i = tags.begin(); while (i != tags_.end())
while (i != tags.end())
{ {
hash_type::iterator old = i; hash_type::iterator old = i;
++i; ++i;
old->first->destroy(); old->first->destroy();
} }
tags.clear(); tags_.clear();
dfs.clear(); dfs_.clear();
} }
bool bool
enumerate_cycles::cycle_found(const state* start) 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) while (i->ts->first != start)
++i; ++i;
do do
...@@ -189,7 +188,7 @@ namespace spot ...@@ -189,7 +188,7 @@ namespace spot
std::cout << aut_->format_state(i->ts->first) << " "; std::cout << aut_->format_state(i->ts->first) << " ";
++i; ++i;
} }
while (i != dfs.end()); while (i != dfs_.end());
std::cout << "\n"; std::cout << "\n";
return true; return true;
} }
......
...@@ -24,15 +24,13 @@ ...@@ -24,15 +24,13 @@
#include "scc.hh" #include "scc.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
#include <deque> #include <deque>
#include <utility>
namespace spot namespace spot
{ {
/// \brief Enumerate elementary cycles in a SCC.
/// \brief Enumerate cycles from a SCC.
///
/// This implements the algorithm on page 170 of:
/// ///
/// This class implements a non-recursive version of the algorithm
/// on page 170 of:
/// \verbatim /// \verbatim
/// @Article{loizou.82.is, /// @Article{loizou.82.is,
/// author = {George Loizou and Peter Thanisch}, /// author = {George Loizou and Peter Thanisch},
...@@ -46,25 +44,45 @@ namespace spot ...@@ -46,25 +44,45 @@ namespace spot
/// month = aug /// month = aug
/// } /// }
/// \endverbatim /// \endverbatim
/// (the additional preprocessings described later in that paper are
/// 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.
///
/// 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.
/// ///
/// (the additional preprocessing described in that paper is not /// We represent a cycle by a sequence of succ_iterator objects
/// implemented). /// 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 /// The class constructor takes an automaton and an scc_map that
/// should already have been built for for automaton. Calling /// should already have been built for that automaton. Calling
/// run(n) will enumerate all elementary cycles in SCC #n. Each /// run(n) will enumerate all elementary cycles in SCC #n. Each
/// time an SCC is found, the method cycle_found() is called with /// time an SCC is found, the method cycle_found(s) is called with
/// the initial state of the cycle (the cycle is constituted from /// the initial state s of the cycle: the cycle is constituted from
/// all the states that are on the dfs stack after this starting /// all the states that are on the dfs_ stack after s (including s).
/// state). When if cycle_found() returns false, the run() method ///
/// will terminate. If it returns true, the run() method will /// You should inherit from this class and redefine the
/// search the next elementary cycle. /// 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 class enumerate_cycles
{ {
protected: protected:
typedef Sgi::hash_set<const state*, typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type; state_ptr_hash, state_ptr_equal> set_type;
// Extra information required for the algorithm for each state.
struct state_info struct state_info
{ {
// Whether the state has already left the stack at least once. // Whether the state has already left the stack at least once.
...@@ -77,38 +95,31 @@ namespace spot ...@@ -77,38 +95,31 @@ namespace spot
bool mark; bool mark;
// Deleted successors (in the paper, states deleted from A(x)) // Deleted successors (in the paper, states deleted from A(x))
set_type del; set_type del;
// Predecessors of the current states, that could not yet // Predecessors of the current states, that could not yet
// contribute to a cycle. // contribute to a cycle.
set_type b; set_type b;
}; };
// Store the state_info for all visited states.
typedef Sgi::hash_map<const state*, state_info, typedef Sgi::hash_map<const state*, state_info,
state_ptr_hash, state_ptr_equal> hash_type; state_ptr_hash, state_ptr_equal> 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; typedef hash_type::iterator tagged_state;
public: // The automaton we are working on.
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:
const tgba* aut_; const tgba* aut_;
// The SCC map built for aut_.
const scc_map& sm_; 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 struct dfs_entry
{ {
tagged_state ts; tagged_state ts;
...@@ -116,9 +127,43 @@ namespace spot ...@@ -116,9 +127,43 @@ namespace spot
bool f; bool f;
}; };
typedef std::deque<dfs_entry> dfs_stack; typedef std::deque<dfs_entry> dfs_stack;
dfs_stack dfs; dfs_stack dfs_;
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);
hash_type tags; 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);
}; };
} }
......
...@@ -27,6 +27,7 @@ namespace spot ...@@ -27,6 +27,7 @@ namespace spot
{ {
namespace namespace
{ {
// Look for a non-accepting cycle.
class weak_checker: public enumerate_cycles class weak_checker: public enumerate_cycles
{ {
public: public:
...@@ -40,16 +41,16 @@ namespace spot ...@@ -40,16 +41,16 @@ namespace spot
virtual bool virtual bool
cycle_found(const state* start) cycle_found(const state* start)
{ {
dfs_stack::const_iterator i = dfs.begin(); dfs_stack::const_reverse_iterator i = dfs_.rbegin();
bdd acc = bddfalse; bdd acc = bddfalse;
while (i->ts->first != start) for (;;)
++i;
do
{ {
acc |= i->succ->current_acceptance_conditions(); acc |= i->succ->current_acceptance_conditions();
if (i->ts->first == start)
break;
++i; ++i;
assert(i != dfs_.rend());
} }
while (i != dfs.end());
if (acc != aut_->all_acceptance_conditions()) if (acc != aut_->all_acceptance_conditions())
{ {
// We have found an non-accepting cycle, so the SCC is not // We have found an non-accepting cycle, so the SCC is not
......
...@@ -30,14 +30,14 @@ namespace spot ...@@ -30,14 +30,14 @@ namespace spot
/// \brief Whether the SCC number \a scc in \a aut is weak. /// \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 /// An SCC is weak if either its cycles are all accepting, or they
/// non-accepting. /// are all non-accepting.
/// ///
/// The scc_map \a map should have been built already. The absence /// The scc_map \a map should have been built already. The absence
/// of accepting cycle is easy to check (the scc_map can tell /// of accepting cycle is easy to check (the scc_map can tell
/// whether the SCC is non-accepting already). For the accepting /// whether the SCC is non-accepting already). For the accepting
/// SCC, this function works by enumerating all cycles in the given /// SCCs, this function enumerates all cycles in the given SCC (it
/// SCC (it stops if it find a non-accepting cycle). /// stops if it find a non-accepting cycle).
bool is_weak_scc(const tgba* aut, scc_map& map, unsigned scc); bool is_weak_scc(const tgba* aut, scc_map& map, unsigned scc);
/// @} /// @}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment