alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files.

Browse source 
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use
the new bfs_steps class.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-24 14:38:21 +00:00
parent df1bf80d1f
commit 2b74398a62
5 changed files with 218 additions and 160 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2004-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use
the new bfs_steps class.
2004-11-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gv04.cc (gv04::result): New struct to compute

2
src/tgbaalgos/Makefile.am
View file

@ -27,6 +27,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
bfssteps.hh \
dotty.hh \
dottydec.hh \
dupexp.hh \
@ -54,6 +55,7 @@ tgbaalgos_HEADERS = \
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
bfssteps.cc \
dotty.cc \
dottydec.cc \
dupexp.cc \

100
src/tgbaalgos/bfssteps.cc Normal file
View file

@ -0,0 +1,100 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// 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
{
bfs_steps::bfs_steps(const tgba* a)
: a_(a)
{
}
bfs_steps::~bfs_steps()
{
}
const state*
bfs_steps::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<const state*> todo;
// Initial state.
todo.push_back(start);
while (!todo.empty())
{
const state* src = todo.front();
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 };
if (match(s, dest))
{
// 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(dest);
father[dest] = s;
}
}
delete i;
}
return 0;
}
}

43
src/tgbaalgos/bfssteps.hh Normal file
View file

@ -0,0 +1,43 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_BFSSTEPS_HH
# define SPOT_TGBAALGOS_BFSSTEPS_HH
#include "emptiness.hh"
namespace spot
{
class bfs_steps
{
public:
bfs_steps(const tgba* a);
virtual ~bfs_steps();
const state* search(const state* start, tgba_run::steps& l);
virtual const state* filter(const state* s) = 0;
virtual bool match(tgba_run::step& step, const state* dest) = 0;
protected:
const tgba* a_;
};
}
#endif // SPOT_TGBAALGOS_BFSSTEPS_HH

225
src/tgbaalgos/gv04.cc
View file

@ -30,13 +30,12 @@
#include <cassert>
#include <utility>
#include <map>
#include <deque>
#include "tgba/tgba.hh"
#include "misc/hash.hh"
#include "emptiness.hh"
#include "emptiness_stats.hh"
#include "gv04.hh"
#include "bfssteps.hh"
namespace spot
{
@ -242,6 +241,8 @@ namespace spot
struct result: public emptiness_check_result
{
gv04& data;
result(gv04& data)
: data(data)
{
@ -253,7 +254,7 @@ namespace spot
tgba_run* res = new tgba_run;
// Transitively update the lowlinks, so we can use them in
// the BDS bellow.
// the BFS bellow.
for (int i = 0; i <= data.top; ++i)
{
int l = data.stack[i].lowlink;
@ -293,179 +294,83 @@ namespace spot
father = data.stack[father].pre;
}
// Construct the cycle in two phases. A first BFS find the
// Construct the cycle in two phases. A first BFS finds the
// shortest path from scc_root to an accepting transition.
// A second BFS then search a path back to scc_root. If
// there is no acceptance conditions we just use the second
// BFS to find a cycle around scc_root.
struct first_bfs: bfs_steps
{
const gv04& data;
int scc_root;
first_bfs(const gv04& data, int scc_root)
: bfs_steps(data.a), data(data), scc_root(scc_root)
{
}
virtual const state*
filter(const state* s)
{
// Do not escape the SCC
hash_type::const_iterator j = data.h.find(s);
if (// This state was never visited so far.
j == data.h.end()
// Or it was discarded
|| j->second >= data.stack.size()
// Or it was discarded (but its stack slot reused)
|| data.stack[j->second].s->compare(s)
// Or it is still on the stack but not in the SCC
|| data.stack[j->second].lowlink < scc_root)
{
delete s;
return 0;
}
delete s;
return j->first;
}
virtual bool
match(tgba_run::step& step, const state*)
{
return step.acc != bddfalse;
}
};
struct second_bfs: first_bfs
{
const state* target;
second_bfs(const gv04& data, int scc_root, const state* target)
: first_bfs(data, scc_root), target(target)
{
}
virtual bool
match(tgba_run::step&, const state* s)
{
return s == target;
}
};
const state* bfs_start = data.stack[scc_root].s;
const state* bfs_end = bfs_start;
if (data.accepting != bddfalse)
{
trace << "1st BFS" << std::endl;
// 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<const state*> todo;
// Initial state.
todo.push_back(bfs_start);
while (!todo.empty())
{
const state* src = todo.front();
todo.pop_front();
tgba_succ_iterator* i = data.a->succ_iter(src);
for (i->first(); !i->done(); i->next())
{
const state* dest = i->current_state();
trace << " state " << data.a->format_state(dest);
// Do not escape the SCC
hash_type::const_iterator j = data.h.find(dest);
if (// This state was never visited so far.
j == data.h.end()
// Or it was discarded
|| j->second >= data.stack.size()
// Or it was discarded (but its stack slot reused)
|| data.stack[j->second].s->compare(dest)
// Or it is still on the stack but not in the SCC
|| data.stack[j->second].lowlink < scc_root)
{
trace << " ignored" << std::endl;
delete dest;
continue;
first_bfs b1(data, scc_root);
bfs_start = b1.search(bfs_start, res->cycle);
assert(bfs_start);
}
trace << " explored" << std::endl;
delete dest;
dest = j->first;
bdd cond = i->current_condition();
bdd acc = i->current_acceptance_conditions();
tgba_run::step s = { src, cond, acc };
if (acc != bddfalse)
{
// Found it!
tgba_run::steps p;
while (s.s != bfs_start)
{
p.push_front(s);
s = father[s.s];
}
p.push_front(s);
res->cycle.splice(res->cycle.end(), p);
// Exit this BFS, and start the next one at dest.
todo.clear();
bfs_start = dest;
break;
}
// Common case: record backlinks and continue BFS
// for unvisited states.
if (father.find(dest) == father.end())
{
todo.push_back(dest);
father[dest] = s;
}
}
delete i;
}
}
// Second BFS.
if (bfs_start != bfs_end || res->cycle.empty())
{
trace << "2nd BFS" << std::endl;
// 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<const state*> todo;
// Initial state.
todo.push_back(bfs_start);
while (!todo.empty())
{
const state* src = todo.front();
todo.pop_front();
tgba_succ_iterator* i = data.a->succ_iter(src);
for (i->first(); !i->done(); i->next())
{
const state* dest = i->current_state();
trace << " state " << data.a->format_state(dest);
// Do not escape the SCC
hash_type::const_iterator j = data.h.find(dest);
if (// This state was never visited so far.
j == data.h.end()
// Or it was discarded
|| j->second >= data.stack.size()
// Or it was discarded (but its stack slot reused)
|| data.stack[j->second].s->compare(dest)
// Or it is still on the stack but not in the SCC
|| data.stack[j->second].lowlink < scc_root)
{
trace << " ignored" << std::endl;
delete dest;
continue;
second_bfs b2(data, scc_root, bfs_end);
bfs_start = b2.search(bfs_start, res->cycle);
assert(bfs_start == bfs_end);
}
trace << " explored" << std::endl;
delete dest;
dest = j->first;
bdd cond = i->current_condition();
bdd acc = i->current_acceptance_conditions();
tgba_run::step s = { src, cond, acc };
if (dest == bfs_end)
{
// Found it!
tgba_run::steps p;
while (s.s != bfs_start)
{
p.push_front(s);
s = father[s.s];
}
p.push_front(s);
res->cycle.splice(res->cycle.end(), p);
// Exit this BFS.
todo.clear();
break;
}
// Common case: record backlinks and continue BFS
// for unvisited states.
if (father.find(dest) == father.end())
{
todo.push_back(dest);
father[dest] = s;
}
}
delete i;
}
}
// Clone every state in the cycle before returning it. (We
// didn't do that before in the algorithm, because it's
// easier to follow if every state manipulated in the BFS is
// the instance in the hash table.)
for (tgba_run::steps::iterator i = res->cycle.begin();
i != res->cycle.end(); ++i)
i->s = i->s->clone();
assert(res->cycle.begin() != res->cycle.end());
return res;
}
gv04& data;
};