diff --git a/ChangeLog b/ChangeLog index cc187cc9b..62da5534a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2004-11-22 Alexandre Duret-Lutz + + * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly + based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and + src/tgbaalgos/tarjan_on_fly.hh former implementation. + * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, + tgbaalgos_HEADERS): Add them. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the + new algorithm. + * src/tgbatest/emptchk.test: Test it. + 2004-11-22 Poitrenaud Denis * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 948157f86..cdd02e98f 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -32,6 +32,7 @@ tgbaalgos_HEADERS = \ dupexp.hh \ emptiness.hh \ emptiness_stats.hh \ + gv04.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ @@ -57,6 +58,7 @@ libtgbaalgos_la_SOURCES = \ dottydec.cc \ dupexp.cc \ emptiness.cc \ + gv04.cc \ lbtt.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc new file mode 100644 index 000000000..ce2cd5c04 --- /dev/null +++ b/src/tgbaalgos/gv04.cc @@ -0,0 +1,245 @@ +// 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. + +//#define TRACE + +#include +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr +#endif + +#include +#include +#include "tgba/tgba.hh" +#include "misc/hash.hh" +#include "emptiness.hh" +#include "gv04.hh" + +namespace spot +{ + namespace + { + struct stack_entry + { + const state* s; // State stored in stack entry. + tgba_succ_iterator* nexttr; // Next transition to explore. + // (The paper uses lasttr for the + // last transition, but nexttr is + // easier for our iterators.) + int lowlink; // Lowlink value if this entry. + int pre; // DFS predecessor. + int acc; // Accepting state link. + }; + + struct gv04: public emptiness_check + { + // The automata to check. + const tgba* a; + + // The unique accepting condition of the automaton \a a, + // or bddfalse if there is no. + bdd accepting; + + // Map of visited states. + typedef Sgi::hash_map hash_type; + hash_type h; + + // Stack of visited states on the path. + typedef std::vector stack_type; + stack_type stack; + size_t max_stack_size; + + int top; // Top of SCC stack. + int dftop; // Top of DFS stack. + bool violation; // Whether an accepting run was found. + + gv04(const tgba *a) + : a(a), accepting(a->all_acceptance_conditions()) + { + assert(a->number_of_acceptance_conditions() <= 1); + } + + ~gv04() + { + for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i) + delete i->nexttr; + hash_type::const_iterator s = h.begin(); + while (s != h.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + delete ptr; + } + } + + virtual emptiness_check_result* + check() + { + max_stack_size = 0; + top = dftop = -1; + violation = false; + push(a->get_init_state(), false); + + while (!violation && dftop >= 0) + { + tgba_succ_iterator* iter = stack[dftop].nexttr; + + trace << "Main iteration (top = " << top + << ", dftop = " << dftop + << ", s = " << a->format_state(stack[dftop].s) + << ")" << std::endl; + + if (iter->done()) + { + trace << " No more successors" << std::endl; + pop(); + } + else + { + const state* s_prime = iter->current_state(); + bool acc = iter->current_acceptance_conditions() == accepting; + iter->next(); + + trace << " Next successor: s_prime = " + << a->format_state(s_prime) + << (acc ? " (with accepting link)" : ""); + + hash_type::const_iterator i = h.find(s_prime); + + if (i == h.end()) + { + trace << " is a new state." << std::endl; + push(s_prime, acc); + } + else + { + if (i->second < stack.size() + && stack[i->second].s->compare(s_prime) == 0) + { + // s_prime has a clone on stack + trace << " is on stack." << std::endl; + // This is an addition to GV04 to support TBA. + violation |= acc; + lowlinkupdate(dftop, i->second); + } + else + { + trace << " has been seen, but is no longer on stack." + << std::endl; + } + + delete s_prime; + } + } + } + if (violation) + return new emptiness_check_result; + return 0; + } + + void + push(const state* s, bool accepting) + { + trace << " push(s = " << a->format_state(s) + << ", accepting = " << accepting << ")" << std::endl; + + h[s] = ++top; + + tgba_succ_iterator* iter = a->succ_iter(s); + iter->first(); + stack_entry ss = { s, iter, top, dftop, 0 }; + + if (accepting) + ss.acc = dftop; // This differs from GV04 to support TBA. + else if (dftop >= 0) + ss.acc = stack[dftop].acc; + else + ss.acc = -1; + + trace << " s.lowlink = " << top << std::endl; + + stack.push_back(ss); + dftop = top; + + max_stack_size = std::max(max_stack_size, stack.size()); + } + + void + pop() + { + trace << " pop()" << std::endl; + + int p = stack[dftop].pre; + if (p >= 0) + lowlinkupdate(p, dftop); + if (stack[dftop].lowlink == dftop) + { + assert(static_cast(top + 1) == stack.size()); + for (int i = top; i >= dftop; --i) + { + delete stack[i].nexttr; + stack.pop_back(); + } + top = dftop - 1; + } + dftop = p; + } + + void + lowlinkupdate(int f, int t) + { + trace << " lowlinkupdate(f = " << f << ", t = " << t + << ")" << std::endl + << " t.lowlink = " << stack[t].lowlink << std::endl + << " f.lowlink = " << stack[f].lowlink << std::endl; + int stack_t_lowlink = stack[t].lowlink; + if (stack_t_lowlink <= stack[f].lowlink) + { + if (stack_t_lowlink <= stack[f].acc) + violation = true; + stack[f].lowlink = stack_t_lowlink; + trace << " f.lowlink updated to " + << stack[f].lowlink << std::endl; + } + } + + virtual std::ostream& + print_stats(std::ostream& os) const + { + os << h.size() << " unique states visited" << std::endl; + os << max_stack_size << " items max on stack" << std::endl; + return os; + } + + }; + + } // anonymous + + emptiness_check* + explicit_gv04_check(const tgba* a) + { + return new gv04(a); + } +} diff --git a/src/tgbaalgos/gv04.hh b/src/tgbaalgos/gv04.hh new file mode 100644 index 000000000..4a17cf95c --- /dev/null +++ b/src/tgbaalgos/gv04.hh @@ -0,0 +1,57 @@ +// 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_GV04_HH +# define SPOT_TGBAALGOS_GV04_HH + +namespace spot +{ + class tgba; + class emptiness_check; + + /// \brief Emptiness check based on Geldenhuys and Valmari's + /// TACAS'04 paper. + /// \ingroup emptiness_check_algorithms + /// \pre The automaton \a a must have at most one accepting condition. + /// + /// The original algorithm, coming from the following paper, has only + /// been slightly modified to work on transition-based automata. + /// \verbatim + /// @InProceedings{geldenhuys.04.tacas, + /// author = {Jaco Geldenhuys and Antti Valmari}, + /// title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification + /// More Efficient}, + /// booktitle = {Proceedings of the 10th International Conference on Tools + /// and Algorithms for the Construction and Analysis of Systems + /// (TACAS'04)}, + /// editor = {Kurt Jensen and Andreas Podelski}, + /// pages = {205--219}, + /// year = {2004}, + /// publisher = {Springer-Verlag}, + /// series = {Lecture Notes in Computer Science}, + /// volume = {2988}, + /// isbn = {3-540-21299-X} + /// } + /// \endverbatim + emptiness_check* explicit_gv04_check(const tgba* a); +} + +#endif // SPOT_TGBAALGOS_GV04_HH diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 998271309..f2ab1e2a3 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -50,6 +50,7 @@ expect_ce() run 0 ./ltl2tgba -ebsh_se05_search "$1" run 0 ./ltl2tgba -ebsh_se05_search -f "$1" run 0 ./ltl2tgba -etau03_opt_search -f "$1" + run 0 ./ltl2tgba -egv04 -f "$1" # Expect multiple accepting runs test `./ltl2tgba -emagic_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 test `./ltl2tgba -ese05_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 @@ -74,6 +75,7 @@ expect_no() run 0 ./ltl2tgba -Ebsh_se05_search "$1" run 0 ./ltl2tgba -Ebsh_se05_search -f "$1" run 0 ./ltl2tgba -Etau03_opt_search -f "$1" + run 0 ./ltl2tgba -Egv04 -f "$1" test `./ltl2tgba -emagic_search_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 test `./ltl2tgba -ese05_search_repeated "!($1)" | diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5cb535132..76c89c8fb 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -35,6 +35,7 @@ #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" +#include "tgbaalgos/gv04.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/se05.hh" #include "tgbaalgos/tau03.hh" @@ -150,7 +151,7 @@ main(int argc, char** argv) int formula_index = 0; std::string echeck_algo; enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search, - Tau03Search, Tau03OptSearch } echeck = None; + Tau03Search, Tau03OptSearch, Gv04 } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool search_many = false; bool bit_state_hashing = false; @@ -421,6 +422,11 @@ main(int argc, char** argv) { echeck = Tau03OptSearch; } + else if (echeck_algo == "gv04") + { + echeck = Gv04; + degeneralize_maybe = true; + } else { std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl; @@ -679,6 +685,9 @@ main(int argc, char** argv) case Tau03OptSearch: ec = spot::explicit_tau03_opt_search(a); break; + case Gv04: + ec = spot::explicit_gv04_check(a); + break; } if (ec) diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index e278c9428..f4db221c9 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -36,6 +36,7 @@ #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/gv04.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/se05.hh" #include "tgbaalgos/tau03.hh" @@ -337,6 +338,10 @@ main(int argc, char** argv) ec_obj.push_back(spot::bit_state_hashing_se05_search(a, 4096)); ec_name.push_back("bit_state_hashing_se05_search"); ec_safe.push_back(false); + + ec_obj.push_back(spot::explicit_gv04_check(a)); + ec_name.push_back("explicit_gv04"); + ec_safe.push_back(true); } if (opt_n_acc >= 1)