Commit 18b22a52 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

* src/tgbaalgos/bfssteps.hh (bfs_steps_with_path_conditions): New

class.
* src/tgbaalgos/bfssteps.cc: Remove includes that are now superfluous.
parent c1fd4d11
2004-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/bfssteps.hh (bfs_steps_with_path_conditions): New
class.
* src/tgbaalgos/bfssteps.cc: Remove includes that are now superfluous.
* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
couvreur99_check_result::accepting_cycle): Rewrite the BFSs using
the bfs_steps class.
......
......@@ -19,10 +19,7 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <map>
#include <deque>
#include "bfssteps.hh"
#include "tgba/tgba.hh"
namespace spot
{
......
......@@ -22,10 +22,20 @@
#ifndef SPOT_TGBAALGOS_BFSSTEPS_HH
# define SPOT_TGBAALGOS_BFSSTEPS_HH
#include <map>
#include <deque>
#include <utility>
#include "emptiness.hh"
#include "tgba/tgba.hh"
namespace spot
{
/// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps.
/// \ingroup tgba_misc
///
/// This class should be used to compute the shortest path
/// between a state of a spot::tgba and the first transition or
/// state that matches some conditions.
class bfs_steps
{
public:
......@@ -38,6 +48,94 @@ namespace spot
const tgba* a_;
};
template<typename T>
class bfs_steps_with_path_conditions
{
public:
bfs_steps_with_path_conditions(const tgba* a)
: a_(a)
{
}
virtual
~bfs_steps_with_path_conditions()
{
}
virtual const state* filter(const state* s) = 0;
virtual bool match(tgba_run::step& step, const state* dest,
const T& src_cond, T& dest_cond) = 0;
const state*
search(const state* start, tgba_run::steps& l)
{
// Records backlinks to parent state during the BFS.
// (This also stores the propositions of this link.)
std::map<const state*, tgba_run::step,
state_ptr_less_than> father;
// BFS queue.
std::deque<std::pair<const state*, T> > todo;
// Initial state.
todo.push_back(start);
while (!todo.empty())
{
const state* src = todo.front().first;
T cond = todo.front().second;
todo.pop_front();
tgba_succ_iterator* i = a_->succ_iter(src);
for (i->first(); !i->done(); i->next())
{
const state* dest = filter(i->current_state());
if (!dest)
continue;
bdd cond = i->current_condition();
bdd acc = i->current_acceptance_conditions();
tgba_run::step s = { src, cond, acc };
std::pair<const state*, T> next;
next.first = src;
if (match(s, dest, cond, next.second))
{
// Found it!
tgba_run::steps p;
for (;;)
{
tgba_run::step tmp = s;
tmp.s = tmp.s->clone();
p.push_front(tmp);
if (s.s == start)
break;
s = father[s.s];
}
l.splice(l.end(), p);
delete i;
return dest;
}
// Common case: record backlinks and continue BFS
// for unvisited states.
if (father.find(dest) == father.end())
{
todo.push_back(next);
father[dest] = s;
}
}
delete i;
}
return 0;
}
protected:
const tgba* a_;
};
}
#endif // SPOT_TGBAALGOS_BFSSTEPS_HH
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