Commit 29bc087d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

reachiter: fix the DFS, and add a version with on_stack()

* src/tgbaalgos/reachiter.hh, src/tgbaalgos/reachiter.cc: Fix the
tgba_reachable_iterator_depth_first implementation by not making
inheriting from tgba_reachable_iterator.  Add a
tgba_reachable_iterator_depth_first_stack
* src/tgbatest/sim.test, src/tgbatest/dstar.test: Adjust.
parent 57f712fc
// 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,54 +115,186 @@ namespace spot
{
}
// tgba_reachable_iterator_depth_first
// tgba_reachable_iterator_breadth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_depth_first::
tgba_reachable_iterator_depth_first(const tgba* a)
tgba_reachable_iterator_breadth_first::
tgba_reachable_iterator_breadth_first(const tgba* a)
: tgba_reachable_iterator(a)
{
}
void
tgba_reachable_iterator_depth_first::add_state(const state* s)
tgba_reachable_iterator_breadth_first::add_state(const state* s)
{
todo.push(s);
todo.push_back(s);
}
const state*
tgba_reachable_iterator_depth_first::next_state()
tgba_reachable_iterator_breadth_first::next_state()
{
if (todo.empty())
return 0;
const state* s = todo.top();
todo.pop();
const state* s = todo.front();
todo.pop_front();
return s;
}
// tgba_reachable_iterator_breadth_first
// tgba_reachable_iterator_depth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_breadth_first::
tgba_reachable_iterator_breadth_first(const tgba* a)
: tgba_reachable_iterator(a)
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_breadth_first::add_state(const state* s)
tgba_reachable_iterator_depth_first::push(const state* s, int sn)
{
todo.push_back(s);
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();
}
const state*
tgba_reachable_iterator_breadth_first::next_state()
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<seen_map::iterator, bool> 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()
{
if (todo.empty())
return 0;
const state* s = todo.front();
todo.pop_front();
return s;
}
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();
}
}
......@@ -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.
......@@ -98,37 +98,107 @@ namespace spot
/// \ingroup tgba_generic
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states depth first.
class SPOT_API tgba_reachable_iterator_depth_first :
/// states breadth first.
class SPOT_API tgba_reachable_iterator_breadth_first :
public tgba_reachable_iterator
{
public:
tgba_reachable_iterator_depth_first(const tgba* a);
tgba_reachable_iterator_breadth_first(const tgba* a);
virtual void add_state(const state* s);
virtual const state* next_state();
protected:
std::stack<const state*> todo; ///< A stack of states yet to explore.
std::deque<const state*> todo; ///< A queue of states yet to explore.
};
/// \ingroup tgba_generic
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states breadth first.
class SPOT_API tgba_reachable_iterator_breadth_first :
public tgba_reachable_iterator
/// \brief Iterate over all states of an automaton using a DFS.
class SPOT_API tgba_reachable_iterator_depth_first
{
public:
tgba_reachable_iterator_breadth_first(const tgba* a);
tgba_reachable_iterator_depth_first(const tgba* a);
virtual ~tgba_reachable_iterator_depth_first();
virtual void add_state(const state* s);
virtual const state* next_state();
/// \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:
std::deque<const state*> todo; ///< A queue of states yet to explore.
const tgba* aut_; ///< The spot::tgba to explore.
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> seen_map;
seen_map seen; ///< States already seen.
struct stack_item
{
const state* src;
int src_n;
tgba_succ_iterator* it;
};
std::deque<stack_item> 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<int> stack_;
};
}
......
......@@ -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]}"]
......
......@@ -35,8 +35,8 @@ run 0 ../ltl2tgba -X -RDCS -b in.tgba > out.tgba
cat >expected.tgba <<EOF
acc = "1";
"1", "2", "b",;
"2", "2", "a", "1";
"4", "3", "b",;
"3", "3", "a", "1";
EOF
diff out.tgba expected.tgba
......
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