From 374a489e3f7c7fb3805632d1df7d95c36cdcbc03 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Sep 2012 16:09:53 +0200 Subject: [PATCH] Implement Loizou & Thanisch's algorithm for enumerating cycles. * 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. --- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/cycles.cc | 198 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/cycles.hh | 126 ++++++++++++++++++++++++ src/tgbatest/Makefile.am | 3 +- src/tgbatest/cycles.test | 62 ++++++++++++ src/tgbatest/ltl2tgba.cc | 20 ++++ 6 files changed, 410 insertions(+), 1 deletion(-) create mode 100644 src/tgbaalgos/cycles.cc create mode 100644 src/tgbaalgos/cycles.hh create mode 100755 src/tgbatest/cycles.test diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 8584b7fb9..3f8e964d8 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -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 \ diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc new file mode 100644 index 000000000..faa545236 --- /dev/null +++ b/src/tgbaalgos/cycles.cc @@ -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 +#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 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 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; + } + + +} diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh new file mode 100644 index 000000000..53d0fff42 --- /dev/null +++ b/src/tgbaalgos/cycles.hh @@ -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 +#include + +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 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 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_stack; + dfs_stack dfs; + + hash_type tags; + }; + +} + +#endif // SPOT_TGBAALGOS_CYCLES_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index f0f0252c3..70198270a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -108,7 +108,8 @@ TESTS = \ spotlbtt.test \ spotlbtt2.test \ complementation.test \ - randpsl.test + randpsl.test \ + cycles.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test new file mode 100755 index 000000000..4500c3390 --- /dev/null +++ b/src/tgbatest/cycles.test @@ -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 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1ee6964e2..3561a6369 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -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"); }