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

Implement Loizou & Thanisch's algorithm for enumerating cycles.

Browse source 
* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbatest/cycles.test: New files.
* src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add a -KC option for testing.
This commit is contained in:
Alexandre Duret-Lutz 2012-09-20 16:09:53 +02:00
parent 379e0d5eb4
commit 374a489e3f
6 changed files with 410 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tgbaalgos/Makefile.am
View file

@ -32,6 +32,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
bfssteps.hh \
cutscc.hh \
cycles.hh \
degen.hh \
dotty.hh \
dottydec.hh \
@ -72,6 +73,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
bfssteps.cc \
cutscc.cc \
cycles.cc \
degen.cc \
dotty.cc \
dottydec.cc \

198
src/tgbaalgos/cycles.cc Normal file
View file

@ -0,0 +1,198 @@
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// 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 <iostream>
#include "cycles.hh"
namespace spot
{
enumerate_cycles::enumerate_cycles(const tgba* aut,
const scc_map& map)
: aut_(aut), sm_(map)
{
}
void
enumerate_cycles::nocycle(tagged_state x, tagged_state y)
{
// insert x in B(y)
y->second.b.insert(x->first);
// insert y in A(x)
x->second.del.insert(y->first);
}
void
enumerate_cycles::unmark(tagged_state y)
{
std::deque<tagged_state> q;
q.push_back(y);
while (!q.empty())
{
y = q.back();
q.pop_back();
y->second.mark = false;
for (set_type::iterator i = y->second.b.begin();
i != y->second.b.end(); ++i)
{
tagged_state x = tags.find(*i);
assert(x != tags.end());
// insert y in A(x)
x->second.del.erase(y->first);
// unmark x recursively if marked
if (x->second.mark)
q.push_back(x);
}
// empty B(y)
y->second.b.clear();
}
}
enumerate_cycles::tagged_state
enumerate_cycles::tag_state(const state* s)
{
std::pair<tagged_state, bool> p =
tags.insert(std::make_pair(s, state_info()));
if (p.second)
s->destroy();
return p.first;
}
void
enumerate_cycles::push_state(tagged_state ts)
{
ts->second.mark = true;
dfs_entry e;
e.ts = ts;
e.succ = 0;
e.f = false;
dfs.push_back(e);
}
void
enumerate_cycles::run(unsigned scc)
{
bool keep_going = true;
push_state(tag_state(sm_.one_state_of(scc)->clone()));
while (keep_going && !dfs.empty())
{
dfs_entry& cur = dfs.back();
if (cur.succ == 0)
{
cur.succ = aut_->succ_iter(cur.ts->first);
cur.succ->first();
}
else
cur.succ->next();
if (!cur.succ->done())
{
// Explore one successor.
// Ignore those that are not on the SCC, or destination
// that have been "virtually" deleted from A(v).
state* s = cur.succ->current_state();
if ((sm_.scc_of_state(s) != scc)
|| (cur.ts->second.del.find(s) != cur.ts->second.del.end()))
{
s->destroy();
continue;
}
tagged_state w = tag_state(s);
if (!w->second.mark)
{
push_state(w);
}
else if (!w->second.reach)
{
keep_going = cycle_found(w->first);
cur.f = true;
}
else
{
nocycle(cur.ts, w);
}
}
else
{
// No more successors.
bool f = cur.f;
tagged_state v = cur.ts;
delete cur.succ;
dfs.pop_back();
if (f)
unmark(v);
v->second.reach = true;
// Update the predecessor in the stack if there is one.
if (!dfs.empty())
{
if (f)
dfs.back().f = true;
else
nocycle(dfs.back().ts, v);
}
}
}
// Purge the dfs stack, in case we aborted because cycle_found()
// said so.
while (!dfs.empty())
{
delete dfs.back().succ;
dfs.pop_back();
}
hash_type::iterator i = tags.begin();
while (i != tags.end())
{
hash_type::iterator old = i;
++i;
old->first->destroy();
}
tags.clear();
dfs.clear();
}
bool
enumerate_cycles::cycle_found(const state* start)
{
dfs_stack::const_iterator i = dfs.begin();
while (i->ts->first != start)
++i;
do
{
std::cout << aut_->format_state(i->ts->first) << " ";
++i;
}
while (i != dfs.end());
std::cout << "\n";
return true;
}
}

126
src/tgbaalgos/cycles.hh Normal file
View file

@ -0,0 +1,126 @@
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// 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_CYCLES_HH
# define SPOT_TGBAALGOS_CYCLES_HH
#include "scc.hh"
#include "misc/hash.hh"
#include <deque>
#include <utility>
namespace spot
{
/// \brief Enumerate cycles from a SCC.
///
/// This implements the algorithm on page 170 of:
///
/// \verbatim
/// @Article{loizou.82.is,
/// author = {George Loizou and Peter Thanisch},
/// title = {Enumerating the Cycles of a Digraph: A New
/// Preprocessing Strategy},
/// journal = {Information Sciences},
/// year = {1982},
/// volume = {27},
/// number = {3},
/// pages = {163--182},
/// month = aug
/// }
/// \endverbatim
///
/// (the additional preprocessing described in that paper is not
/// implemented).
///
/// The class constructor takes an automaton, and an scc_map that
/// should already have been built for for automaton. Calling
/// run(n) will enumerate all elementary cycles in SCC #n. Each
/// time an SCC is found, the method cycle_found() is called with
/// the initial state of the cycle (the cycle is constituted from
/// all the states that are on the dfs stack after this starting
/// state). When if cycle_found() returns false, the run() method
/// will terminate. If it returns true, the run() method will
/// search the next elementary cycle.
class enumerate_cycles
{
protected:
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
struct state_info
{
// Whether the state has already left the stack at least once.
bool reach;
// set to true when the state current state w is stacked, and
// reset either when the state is unstacked after having
// contributed to a cycle, or when some state z that (1) w could
// reach (even indirectly) without discovering a cycle, and (2)
// that a contributed to a contributed to a cycle.
bool mark;
// Deleted successors (in the paper, states deleted from A(x))
set_type del;
// Predecessors of the current states, that could not yet
// contribute to a cycle.
set_type b;
};
typedef Sgi::hash_map<const state*, state_info,
state_ptr_hash, state_ptr_equal> hash_type;
typedef hash_type::iterator tagged_state;
public:
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 scc_map& sm_;
struct dfs_entry
{
tagged_state ts;
tgba_succ_iterator* succ;
bool f;
};
typedef std::deque<dfs_entry> dfs_stack;
dfs_stack dfs;
hash_type tags;
};
}
#endif // SPOT_TGBAALGOS_CYCLES_HH

3
src/tgbatest/Makefile.am
View file

@ -108,7 +108,8 @@ TESTS = \
spotlbtt.test \
spotlbtt2.test \
complementation.test \
randpsl.test
randpsl.test \
cycles.test
EXTRA_DIST = $(TESTS)

62
src/tgbatest/cycles.test Executable file
View file

@ -0,0 +1,62 @@
#!/bin/sh
# Copyright (C) 2012 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# 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.
# While running some benchmark, Tomáš Babiak found that Spot took too
# much time (i.e. >1h) to translate those six formulae. It turns out
# that the WDBA minimization was performed after the degeneralization
# algorithm, while this is not necessary (WDBA will produce a BA, so
# we may as well skip degeneralization). Translating these formulae
# in the test-suite ensure that they don't take too much time (the
# buildfarm will timeout if it does).
. ./defs
set -e
# Fig.1 from Johnson's SIAM J. Comput. 1975 paper.
(
echo 'acc = ;'
k=3
v=`expr $k + 2`
w=`expr 2 \* $k + 2`
x=`expr 3 \* $k + 3`
for i in $(seq 2 `expr $k + 1`); do
echo "s1,s$i,,;"
echo "s$i,s$v,,;"
done
for i in $(seq `expr $k + 2` `expr 2 \* $k`); do
echo "s$i,s`expr $i + 1`,,;"
echo "s$i,s$w,,;"
done
echo "s`expr 2 \* $k + 1`,s$w,,;"
echo "s`expr 2 \* $k + 1`,s1,,;"
for i in $(seq `expr 2 \* $k + 3` `expr 3 \* $k + 2`); do
echo "s$w,s$i,,;"
echo "s$i,s$x,,;"
done
echo "s`expr 2 \* $k + 3`,s$v,,;"
echo "s$x,s$w,,;"
) > johnson-fig1.tgba
run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out
test `wc -l < out` -eq 10

20
src/tgbatest/ltl2tgba.cc
View file

@ -64,6 +64,7 @@
#include "tgbaalgos/emptiness_stats.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/isdet.hh"
#include "tgbaalgos/cycles.hh"
#include "kripkeparse/public.hh"
#include "tgbaalgos/simulation.hh"
@ -281,6 +282,7 @@ syntax(char* prog)
<< " -K dump the graph of SCCs in dot format" << std::endl
<< " -KV verbosely dump the graph of SCCs in dot format"
<< std::endl
<< " -KC list cycles in automaton" << std::endl
<< " -N output the never clain for Spin (implies -DS)"
<< std::endl
<< " -NN output the never clain for Spin, with commented states"
@ -522,6 +524,10 @@ main(int argc, char** argv)
{
output = 11;
}
else if (!strcmp(argv[formula_index], "-KC"))
{
output = 15;
}
else if (!strcmp(argv[formula_index], "-l"))
{
translation = TransLaCIM;
@ -1409,6 +1415,20 @@ main(int argc, char** argv)
std::cout << std::endl;
break;
case 15:
{
spot::scc_map m(a);
m.build_map();
spot::enumerate_cycles c(a, m);
unsigned max = m.scc_count();
for (unsigned n = 0; n < max; ++n)
{
std::cout << "Cycles in SCC #" << n << std::endl;
c.run(n);
}
break;
}
default:
assert(!"unknown output option");
}