diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 0a9e7c6df..6fb676dbb 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -115,31 +115,6 @@ namespace spot { } - // tgba_reachable_iterator_depth_first - ////////////////////////////////////////////////////////////////////// - - tgba_reachable_iterator_depth_first:: - tgba_reachable_iterator_depth_first(const tgba* a) - : tgba_reachable_iterator(a) - { - } - - void - tgba_reachable_iterator_depth_first::add_state(const state* s) - { - todo.push(s); - } - - const state* - tgba_reachable_iterator_depth_first::next_state() - { - if (todo.empty()) - return 0; - const state* s = todo.top(); - todo.pop(); - return s; - } - // tgba_reachable_iterator_breadth_first ////////////////////////////////////////////////////////////////////// @@ -165,4 +140,161 @@ namespace spot return s; } + // tgba_reachable_iterator_depth_first + ////////////////////////////////////////////////////////////////////// + + tgba_reachable_iterator_depth_first:: + tgba_reachable_iterator_depth_first(const tgba* a) + : aut_(a) + { + } + + tgba_reachable_iterator_depth_first::~tgba_reachable_iterator_depth_first() + { + seen_map::const_iterator s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + ptr->destroy(); + } + } + + void + tgba_reachable_iterator_depth_first::push(const state* s, int sn) + { + tgba_succ_iterator* si = aut_->succ_iter(s); + process_state(s, sn, si); + stack_item item = { s, sn, si }; + todo.push_back(item); + si->first(); + } + + void + tgba_reachable_iterator_depth_first::pop() + { + delete todo.back().it; + todo.pop_back(); + if (!todo.empty()) + todo.back().it->next(); + } + + void + tgba_reachable_iterator_depth_first::run() + { + int n = 1; + start(); + state* i = aut_->get_init_state(); + if (want_state(i)) + push(i, n); + seen[i] = n++; + const state* dst; + while (!todo.empty()) + { + tgba_succ_iterator* si = todo.back().it; + if (si->done()) + { + pop(); + continue; + } + + dst = si->current_state(); + std::pair res = + seen.insert(std::make_pair(dst, n)); + if (!res.second) + { + // The state has already been seen. + dst->destroy(); + // 0-numbered states are not wanted. + if (res.first->second == 0) + { + si->next(); + continue; + } + dst = res.first->first; + } + else if (!want_state(dst)) + { + // Mark this state as non-wanted in case we see it again. + res.first->second = 0; + si->next(); + continue; + } + else + { + ++n; + } + + int dst_n = res.first->second; + process_link(todo.back().src, todo.back().src_n, dst, dst_n, si); + + if (res.second) + push(dst, dst_n); + else + si->next(); + } + end(); + } + + bool + tgba_reachable_iterator_depth_first::want_state(const state*) const + { + return true; + } + + void + tgba_reachable_iterator_depth_first::start() + { + } + + void + tgba_reachable_iterator_depth_first::end() + { + } + + void + tgba_reachable_iterator_depth_first::process_state(const state*, int, + tgba_succ_iterator*) + { + } + + void + tgba_reachable_iterator_depth_first::process_link(const state*, int, + const state*, int, + const tgba_succ_iterator*) + { + } + + // tgba_reachable_iterator_depth_first_stack + ////////////////////////////////////////////////////////////////////// + + + tgba_reachable_iterator_depth_first_stack:: + tgba_reachable_iterator_depth_first_stack(const tgba* a) + : tgba_reachable_iterator_depth_first(a) + { + } + + void + tgba_reachable_iterator_depth_first_stack::push(const state* s, int sn) + { + stack_.insert(sn); + this->tgba_reachable_iterator_depth_first::push(s, sn); + } + + void + tgba_reachable_iterator_depth_first_stack::pop() + { + stack_.erase(todo.back().src_n); + this->tgba_reachable_iterator_depth_first::pop(); + } + + bool + tgba_reachable_iterator_depth_first_stack::on_stack(int sn) const + { + return stack_.find(sn) != stack_.end(); + } + + } diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 599e3e59f..bda9ed419 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -40,15 +40,15 @@ namespace spot /// \brief Iterate over all reachable states of a spot::tgba. /// - /// This is a template method that will call add_state(), next_state(), - /// start(), end(), process_state(), and process_link(), while it - /// iterates over states. - void run(); + /// This is a template method that will call add_state(), + /// next_state(), want_state(), start(), end(), process_state(), + /// and process_link(), while it iterates over states. + virtual void run(); /// \name Todo list management. /// - /// spot::tgba_reachable_iterator_depth_first and - /// spot::tgba_reachable_iterator_breadth_first offer two precanned + /// See e.g. + /// spot::tgba_reachable_iterator_breadth_first for precanned /// implementations for these functions. /// \{ /// \brief Called by run() to register newly discovered states. @@ -96,22 +96,6 @@ namespace spot seen_map seen; ///< States already seen. }; - /// \ingroup tgba_generic - /// \brief An implementation of spot::tgba_reachable_iterator that browses - /// states depth first. - class SPOT_API tgba_reachable_iterator_depth_first : - public tgba_reachable_iterator - { - public: - tgba_reachable_iterator_depth_first(const tgba* a); - - virtual void add_state(const state* s); - virtual const state* next_state(); - - protected: - std::stack todo; ///< A stack of states yet to explore. - }; - /// \ingroup tgba_generic /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states breadth first. @@ -128,7 +112,93 @@ namespace spot std::deque todo; ///< A queue of states yet to explore. }; + /// \ingroup tgba_generic + /// \brief Iterate over all states of an automaton using a DFS. + class SPOT_API tgba_reachable_iterator_depth_first + { + public: + tgba_reachable_iterator_depth_first(const tgba* a); + virtual ~tgba_reachable_iterator_depth_first(); + /// \brief Iterate over all reachable states of a spot::tgba. + /// + /// This is a template method that will call start(), end(), + /// want_state(), process_state(), and process_link(), while it + /// iterates over states. + virtual void run(); + + /// Called by add_state or next_states implementations to filter + /// states. Default implementation always return true. + virtual bool want_state(const state* s) const; + + /// Called by run() before starting its iteration. + virtual void start(); + /// Called by run() once all states have been explored. + virtual void end(); + + /// Called by run() to process a state. + /// + /// \param s The current state. + /// \param n A unique number assigned to \a s. + /// \param si The spot::tgba_succ_iterator for \a s. + virtual void process_state(const state* s, int n, tgba_succ_iterator* si); + /// Called by run() to process a transition. + /// + /// \param in_s The source state + /// \param in The source state number. + /// \param out_s The destination state + /// \param out The destination state number. + /// \param si The spot::tgba_succ_iterator positionned on the current + /// transition. + /// + /// The in_s and out_s states are owned by the + /// spot::tgba_reachable_iterator instance and destroyed when the + /// instance is destroyed. + virtual void process_link(const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si); + + protected: + const tgba* aut_; ///< The spot::tgba to explore. + + typedef Sgi::hash_map seen_map; + seen_map seen; ///< States already seen. + struct stack_item + { + const state* src; + int src_n; + tgba_succ_iterator* it; + }; + std::deque todo; ///< the DFS stack + + /// Push a new state in todo. + virtual void push(const state* s, int sn); + /// Pop the DFS stack. + virtual void pop(); + }; + + /// \ingroup tgba_generic + /// \brief Iterate over all states of an automaton using a DFS. + /// + /// This variant also maintains a set of states that are on the DFS + /// stack. It can be checked using the on_stack() method. + class tgba_reachable_iterator_depth_first_stack + : public tgba_reachable_iterator_depth_first + { + public: + tgba_reachable_iterator_depth_first_stack(const tgba* a); + /// \brief Whether state sn is on the DFS stack. + /// + /// Note the destination state of a transition is only pushed to + /// the stack after process_link() has been called. + bool on_stack(int sn) const; + protected: + virtual void push(const state* s, int sn); + virtual void pop(); + + Sgi::hash_set stack_; + }; } diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index ffec48eb7..a904e0032 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -85,7 +85,7 @@ digraph G { 1 [label="1"] 1 -> 1 [label="a & !b\n"] 1 -> 2 [label="b\n"] - 2 [label="3", peripheries=2] + 2 [label="2", peripheries=2] 2 -> 2 [label="1\n{Acc[1]}"] } EOF @@ -219,12 +219,12 @@ digraph G { 2 [label="2"] 2 -> 2 [label="!b\n"] 2 -> 4 [label="b\n"] - 3 [label="3", peripheries=2] + 3 [label="4", peripheries=2] 3 -> 2 [label="!a & !b\n{Acc[1]}"] 3 -> 3 [label="a & !b\n{Acc[1]}"] 3 -> 4 [label="b & !a\n{Acc[1]}"] 3 -> 5 [label="a & b\n{Acc[1]}"] - 4 [label="4", peripheries=2] + 4 [label="3", peripheries=2] 4 -> 4 [label="1\n{Acc[1]}"] 5 [label="5", peripheries=2] 5 -> 4 [label="!a\n{Acc[1]}"] diff --git a/src/tgbatest/sim.test b/src/tgbatest/sim.test index 209aec1c1..bb00a8add 100755 --- a/src/tgbatest/sim.test +++ b/src/tgbatest/sim.test @@ -35,8 +35,8 @@ run 0 ../ltl2tgba -X -RDCS -b in.tgba > out.tgba cat >expected.tgba <