From f52082bcfb9283b00d095f54c486db845fc10678 Mon Sep 17 00:00:00 2001 From: Denis Poitrenaud Date: Tue, 9 Nov 2004 17:22:58 +0000 Subject: [PATCH] * src/tgbaalgos/magic.cc: rewrite to externalize the heap and prepare it to a bit state hashing version. * src/tgbaalgos/magic.hh: adapt to the new interface of magic_search and se05_search. * src/tgbaalgos/se05.cc: new file. * src/tgbaalgos/Makefile.am: Add it. * src/tgbatest/ltl2tgba.cc: Add new emptiness check. * src/tgbatest/emptchk.test: more tests. * src/tgbatest/dfs.test: new file. * src/tgbatest/Makefile.am: Add it. --- ChangeLog | 13 + src/tgbaalgos/Makefile.am | 1 + src/tgbaalgos/magic.cc | 514 +++++++++++++++++++++++++++----------- src/tgbaalgos/magic.hh | 227 ++++++++++------- src/tgbaalgos/se05.cc | 483 +++++++++++++++++++++++++++++++++++ src/tgbatest/Makefile.am | 7 +- src/tgbatest/dfs.test | 170 +++++++++++++ src/tgbatest/emptchk.test | 41 +-- src/tgbatest/ltl2tgba.cc | 24 +- 9 files changed, 1226 insertions(+), 254 deletions(-) create mode 100644 src/tgbaalgos/se05.cc create mode 100755 src/tgbatest/dfs.test diff --git a/ChangeLog b/ChangeLog index 6af1b26f9..240c8b56e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2004-11-09 Poitrenaud Denis + + * src/tgbaalgos/magic.cc: rewrite to externalize the heap and + prepare it to a bit state hashing version. + * src/tgbaalgos/magic.hh: adapt to the new interface of + magic_search and se05_search. + * src/tgbaalgos/se05.cc: new file. + * src/tgbaalgos/Makefile.am: Add it. + * src/tgbatest/ltl2tgba.cc: Add new emptiness check. + * src/tgbatest/emptchk.test: more tests. + * src/tgbatest/dfs.test: new file. + * src/tgbatest/Makefile.am: Add it. + 2004-11-09 Alexandre Duret-Lutz * src/tgbaalgos/emptiness.cc (print_tgba_run): Output the diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index d3282e906..b8aff5328 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -62,6 +62,7 @@ libtgbaalgos_la_SOURCES = \ replayrun.cc \ rundotdec.cc \ save.cc \ + se05.cc \ stats.cc \ reductgba_sim.cc \ reductgba_sim_del.cc diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 3a6048f02..1cc4ec055 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -19,163 +19,397 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include +#include "misc/hash.hh" +#include #include #include #include "magic.hh" -#include "tgba/bddprint.hh" namespace spot { - magic_search::result::result(magic_search& ms) - : ms_(ms) + namespace { - } + enum color {WHITE, BLUE, RED}; - tgba_run* - magic_search::result::accepting_run() - { - tgba_run* run = new tgba_run; - - stack_type::const_reverse_iterator i, e = ms_.stack.rend(); - tstack_type::const_reverse_iterator ti; - tgba_run::steps* l = &run->prefix; - - for (i = ms_.stack.rbegin(), ti = ms_.tstack.rbegin(); i != e; ++i, ++ti) + /// \brief Emptiness checker on spot::tgba automata having at most one + /// accepting condition (i.e. a TBA). + template + class magic_search : public emptiness_check + { + public: + /// \brief Initialize the Magic Search algorithm on the automaton \a a + /// + /// \pre The automaton \a a must have at most one accepting + /// condition (i.e. it is a TBA). + magic_search(const tgba *a) + : a(a), all_cond(a->all_acceptance_conditions()) { - if (i->first.s->compare(ms_.x) == 0) - l = &run->cycle; - - tgba_run::step s = { i->first.s->clone(), ti->first, ti->second }; - l->push_back(s); + assert(a->number_of_acceptance_conditions() <= 1); } - return run; - } - - - magic_search::magic_search(const tgba_tba_proxy* a) - : a(a), x(0) - { - } - - magic_search::~magic_search() - { - hash_type::const_iterator s = h.begin(); - while (s != h.end()) + virtual ~magic_search() { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - delete ptr; - } - delete x; - // Release all iterators on the stack. - while (!stack.empty()) - { - delete stack.front().second; - stack.pop_front(); - } - } - - void - magic_search::push(const state* s, bool m) - { - tgba_succ_iterator* i = a->succ_iter(s); - i->first(); - - hash_type::iterator hi = h.find(s); - if (hi == h.end()) - { - magic d = { !m, m }; - h[s] = d; - } - else - { - hi->second.seen_without |= !m; - hi->second.seen_with |= m; - if (hi->first != s) - delete s; - s = hi->first; + // Release all iterators on the stacks. + while (!st_blue.empty()) + { + h.pop_notify(st_blue.front().s); + delete st_blue.front().it; + st_blue.pop_front(); + } + while (!st_red.empty()) + { + h.pop_notify(st_red.front().s); + delete st_red.front().it; + st_red.pop_front(); + } } - magic_state ms = { s, m }; - stack.push_front(state_iter_pair(ms, i)); - } - - bool - magic_search::has(const state* s, bool m) const - { - hash_type::const_iterator i = h.find(s); - if (i == h.end()) - return false; - if (!m && i->second.seen_without) - return true; - if (m && i->second.seen_with) - return true; - return false; - } - - emptiness_check_result* - magic_search::check() - { - if (stack.empty()) - // It's a new search. - push(a->get_init_state(), false); - else - // Remove the transition to the cycle root. - tstack.pop_front(); - - assert(stack.size() == 1 + tstack.size()); - - while (!stack.empty()) + /// \brief Perform a Magic Search. + /// + /// \return non null pointer iff the algorithm has found a + /// new accepting path. + /// + /// check() can be called several times (until it returns a null + /// pointer) to enumerate all the visited accepting paths. The method + /// visits only a finite set of accepting paths. + virtual emptiness_check_result* check() { - recurse: - magic_search::state_iter_pair& p = stack.front(); - tgba_succ_iterator* i = p.second; - const bool magic = p.first.m; - - while (!i->done()) - { - const state* s_prime = i->current_state(); - bdd c = i->current_condition(); - bdd acc = i->current_acceptance_conditions(); - i->next(); - if (magic && 0 == s_prime->compare(x)) - { - delete s_prime; - tstack.push_front (tstack_item(c, acc)); - assert(stack.size() == tstack.size()); - return new result(*this); - } - if (!has(s_prime, magic)) - { - push(s_prime, magic); - tstack.push_front (tstack_item(c, acc)); - goto recurse; - } - delete s_prime; - } - - const state* s = p.first.s; - delete i; - stack.pop_front(); - - if (!magic && a->state_is_accepting(s)) - { - if (!has(s, true)) - { - delete x; - x = s->clone(); - push(s, true); - continue; - } - } - if (!stack.empty()) - tstack.pop_front(); + nbn = nbt = 0; + sts = mdp = st_blue.size() + st_red.size(); + if (st_red.empty()) + { + assert(st_blue.empty()); + const state* s0 = a->get_init_state(); + ++nbn; + h.add_new_state(s0, BLUE); + push(st_blue, s0, bddfalse, bddfalse); + if (dfs_blue()) + return new result(*this); + } + else + { + h.pop_notify(st_red.front().s); + delete st_red.front().it; + st_red.pop_front(); + if (!st_red.empty() && dfs_red()) + return new result(*this); + else + if (dfs_blue()) + return new result(*this); + } + return 0; } - assert(tstack.empty()); - return 0; + virtual std::ostream& print_stats(std::ostream &os) const + { + os << nbn << " distinct nodes visited" << std::endl; + os << nbt << " transitions explored" << std::endl; + os << mdp << " nodes for the maximal stack depth" << std::endl; + if (!st_red.empty()) + { + assert(!st_blue.empty()); + os << st_blue.size() + st_red.size() - 1 + << " nodes for the counter example" << std::endl; + } + return os; + } + + private: + /// \brief counters for statistics (number of distinct nodes, of + /// transitions and maximal stacks size. + int nbn, nbt, mdp, sts; + + struct stack_item + { + stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) + : s(n), it(i), label(l), acc(a) {}; + /// The visited state. + const state* s; + /// Design the next successor of \a s which has to be visited. + tgba_succ_iterator* it; + /// The label of the transition followed to reach \a s + /// (false for the first one). + bdd label; + /// The acc set of the transition followed to reach \a s + /// (false for the first one). + bdd acc; + }; + + typedef std::list stack_type; + + void push(stack_type& st, const state* s, + const bdd& label, const bdd& acc) + { + ++sts; + if (sts>mdp) + mdp = sts; + tgba_succ_iterator* i = a->succ_iter(s); + i->first(); + st.push_front(stack_item(s, i, label, acc)); + } + + /// \brief Stack of the blue dfs. + stack_type st_blue; + + /// \brief Stack of the red dfs. + stack_type st_red; + + /// \brief Map where each visited state is colored + /// by the last dfs visiting it. + heap h; + + /// State targeted by the red dfs. + const state* target; + + /// The automata to check. + const tgba* a; + + /// The automata to check. + bdd all_cond; + + bool dfs_blue() + { + while (!st_blue.empty()) + { + stack_item& f = st_blue.front(); + if (!f.it->done()) + { + ++nbt; + const state *s_prime = f.it->current_state(); + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + typename heap::color_ref c = h.get_color_ref(s_prime); + if (c.is_null()) + // Go down the edge (f.s, , s_prime) + { + ++nbn; + h.add_new_state(s_prime, BLUE); + push(st_blue, s_prime, label, acc); + } + else // Backtrack the edge (f.s, , s_prime) + { + if (c.get() == BLUE && acc == all_cond) + // the test 'c.get() == BLUE' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. + { + target = f.s; + c.set(RED); + push(st_red, s_prime, label, acc); + if (dfs_red()) + return true; + } + } + } + else + // Backtrack the edge + // (predecessor of f.s in st_blue, , f.s) + { + --sts; + stack_item f_dest(f); + delete f.it; + st_blue.pop_front(); + typename heap::color_ref c = h.get_color_ref(f_dest.s); + assert(!c.is_null()); + if (c.get() == BLUE && f_dest.acc == all_cond + && !st_blue.empty()) + // the test 'c.get() == BLUE' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. + { + target = st_blue.front().s; + c.set(RED); + push(st_red, f_dest.s, f_dest.label, f_dest.acc); + if (dfs_red()) + return true; + } + else + h.pop_notify(f_dest.s); + } + } + return false; + } + + bool dfs_red() + { + assert(!st_red.empty()); + if (target->compare(st_red.front().s) == 0) + return true; + + while (!st_red.empty()) + { + stack_item& f = st_red.front(); + if (!f.it->done()) // Go down + { + ++nbt; + const state *s_prime = f.it->current_state(); + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + typename heap::color_ref c = h.get_color_ref(s_prime); + if (c.is_null()) + // Notice that this case is taken into account only to + // support successive calls to the check method. Without + // this functionnality, one can check assert(c.is_null()). + // Go down the edge (f.s, , s_prime) + { + ++nbn; + h.add_new_state(s_prime, RED); + push(st_red, s_prime, label, acc); + } + else // Go down the edge (f.s, , s_prime) + { + if (c.get() != RED) + { + c.set(RED); + push(st_red, s_prime, label, acc); + if (target->compare(s_prime) == 0) + return true; + } + } + } + else // Backtrack + { + --sts; + h.pop_notify(f.s); + delete f.it; + st_red.pop_front(); + } + } + return false; + } + + class result: public emptiness_check_result + { + public: + result(magic_search& ms) + : ms_(ms) + { + } + virtual tgba_run* accepting_run() + { + assert(!ms_.st_blue.empty()); + assert(!ms_.st_red.empty()); + + tgba_run* run = new tgba_run; + + typename stack_type::const_reverse_iterator i, j, end; + tgba_run::steps* l; + + l = &run->prefix; + + i = ms_.st_blue.rbegin(); + end = ms_.st_blue.rend(); --end; + j = i; ++j; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + l = &run->cycle; + + j = ms_.st_red.rbegin(); + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + + i = j; ++j; + end = ms_.st_red.rend(); --end; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + return run; + } + private: + magic_search& ms_; + }; + + }; + + class explicit_magic_search_heap + { + public: + class color_ref + { + public: + color_ref(color* c) :p(c) + { + } + int get() const + { + return *p; + } + void set(color c) + { + assert(!is_null()); + *p=c; + } + bool is_null() const + { + return p==0; + } + private: + color *p; + }; + + explicit_magic_search_heap() + { + } + + ~explicit_magic_search_heap() + { + 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; + } + } + + color_ref get_color_ref(const state*& s) + { + hash_type::iterator it = h.find(s); + if (it==h.end()) + return color_ref(0); + if (s!=it->first) + { + delete s; + s = it->first; + } + return color_ref(&(it->second)); + } + + void add_new_state(const state* s, color c) + { + assert(h.find(s)==h.end()); + h.insert(std::make_pair(s, c)); + } + + void pop_notify(const state*) + { + } + + private: + + typedef Sgi::hash_map hash_type; + hash_type h; + }; + + } // anonymous + + emptiness_check* explicit_magic_search(const tgba *a) + { + return new magic_search(a); } } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 91f134c78..975b292d2 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -22,107 +22,148 @@ #ifndef SPOT_TGBAALGOS_MAGIC_HH # define SPOT_TGBAALGOS_MAGIC_HH -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" +#include "tgba/tgba.hh" #include "emptiness.hh" namespace spot { - /// \brief Emptiness check on spot::tgba_tba_proxy automata using - /// the Magic Search algorithm. + /// \brief Returns an emptiness check on the spot::tgba automaton \a a. + /// + /// \pre The automaton \a a must have at most one accepting condition (i.e. + /// it is a TBA). + /// + /// The method \a check() of the returned checker can be called several times + /// (until it returns a null pointer) to enumerate all the visited accepting + /// paths. The method visits only a finite set of accepting paths. + /// + /// The implemented algorithm is the following. /// - /// This algorithm comes from /// \verbatim - /// @InProceedings{ godefroid.93.pstv, - /// author = {Patrice Godefroid and Gerard .J. Holzmann}, - /// title = {On the verification of temporal properties}, - /// booktitle = {Proceedings of the 13th IFIP TC6/WG6.1 International - /// Symposium on Protocol Specification, Testing, and - /// Verification (PSTV'93)}, - /// month = {May}, - /// editor = {Andr{\'e} A. S. Danthine and Guy Leduc - /// and Pierre Wolper}, - /// address = {Liege, Belgium}, - /// pages = {109--124}, - /// publisher = {North-Holland}, - /// year = {1993}, - /// series = {IFIP Transactions}, - /// volume = {C-16}, - /// isbn = {0-444-81648-8} - /// } + /// procedure nested_dfs () + /// begin + /// call dfs_blue(s0); + /// end; + /// + /// procedure dfs_blue (s) + /// begin + /// s.color = blue; + /// for all t in post(s) do + /// if t.color == white then + /// call dfs_blue(t); + /// end if; + /// if (the edge (s,t) is accepting) then + /// target = s; + /// call dfs_red(t); + /// end if; + /// end for; + /// end; + /// + /// procedure dfs_red(s) + /// begin + /// s.color = red; + /// if s == target then + /// report cycle + /// end if; + /// for all t in post(s) do + /// if t.color != red then + /// call dfs_red(t); + /// end if; + /// end for; + /// end; /// \endverbatim - struct magic_search : public emptiness_check - { - /// Initialize the Magic Search algorithm on the automaton \a a. - magic_search(const tgba_tba_proxy *a); - virtual ~magic_search(); + /// + /// It is an adaptation to TBA of the Magic Search algorithm + /// which deals with accepting states and is presented in + /// + /// \verbatim + /// Article{ courcoubertis.92.fmsd, + /// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre + /// Wolper and Mihalis Yannakakis}, + /// title = {Memory-Efficient Algorithm for the Verification of + /// Temporal Properties}, + /// journal = {Formal Methods in System Design}, + /// pages = {275--288}, + /// year = {1992}, + /// volume = {1} + /// } + /// \endverbatim + emptiness_check* explicit_magic_search(const tgba *a); - /// \brief Perform a Magic Search. - /// - /// \return true iff the algorithm has found a new accepting - /// path. - /// - /// check() can be called several times until it return false, - /// to enumerate all accepting paths. - virtual emptiness_check_result* check(); - - private: - - // The names "stack", "h", and "x", are those used in the paper. - - /// \brief Records whether a state has be seen with the magic bit - /// on or off. - struct magic - { - bool seen_without : 1; - bool seen_with : 1; - }; - - /// \brief A state for the spot::magic_search algorithm. - struct magic_state - { - const state* s; - bool m; ///< The state of the magic demon. - }; - - typedef std::pair state_iter_pair; - typedef std::list stack_type; - stack_type stack; ///< Stack of visited states on the path. - - typedef std::pair tstack_item; - typedef std::list tstack_type; - /// \brief Stack of transitions. - /// - /// This is an addition to the data from the paper. - tstack_type tstack; - - typedef Sgi::hash_map hash_type; - hash_type h; ///< Map of visited states. - - /// Append a new state to the current path. - void push(const state* s, bool m); - /// Check whether we already visited \a s with the Magic bit set to \a m. - bool has(const state* s, bool m) const; - - const tgba_tba_proxy* a; ///< The automata to check. - /// The state for which we are currently seeking an SCC. - const state* x; - -#ifndef SWIG - class result: public emptiness_check_result - { - public: - result(magic_search& ms); - virtual tgba_run* accepting_run(); - private: - magic_search& ms_; - }; -#endif // SWIG - }; + /// \brief Returns an emptiness check on the spot::tgba automaton \a a. + /// + /// \pre The automaton \a a must have at most one accepting condition (i.e. + /// it is a TBA). + /// + /// The method \a check() of the returned checker can be called several times + /// (until it returns a null pointer) to enumerate all the visited accepting + /// paths. The method visits only a finite set of accepting paths. + /// + /// The implemented algorithm is the following: + /// + /// procedure nested_dfs () + /// begin + /// weight = 0; + /// call dfs_blue(s0); + /// end; + /// + /// procedure dfs_blue (s) + /// begin + /// s.color = cyan; + /// s.weight = weight; + /// for all t in post(s) do + /// if t.color == white then + /// if the edge (s,t) is accepting then + /// weight = weight + 1; + /// end if; + /// call dfs_blue(t); + /// if the edge (s,t) is accepting then + /// weight = weight - 1; + /// end if; + /// else if t.color == cyan and + /// (the edge (s,t) is accepting or + /// weight > t.weight) then + /// report cycle; + /// end if; + /// if the edge (s,t) is accepting then + /// call dfs_red(t); + /// end if; + /// end for; + /// s.color = blue; + /// end; + /// + /// procedure dfs_red(s) + /// begin + /// if s.color == cyan then + /// report cycle; + /// end if; + /// s.color = red; + /// for all t in post(s) do + /// if t.color != red then + /// call dfs_red(t); + /// end if; + /// end for; + /// end; + /// + /// It is an adaptation to TBA and an extension of the one + /// presented in + /// \verbatim + /// InProceedings{ schwoon.05.tacas, + /// author = {Stephan Schwoon and Javier Esparza}, + /// title = {A Note on On-The-Fly Verification Algorithms}, + /// booktitle = {TACAS'05}, + /// pages = {}, + /// year = {2005}, + /// volume = {}, + /// series = {LNCS}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + /// + /// the extention consists in the introduction of a weight associated + /// to each state in the blue stack. The weight represents the number of + /// accepting arcs traversed to reach it from the initial state. + /// + emptiness_check* explicit_se05_search(const tgba *a); } diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc new file mode 100644 index 000000000..2a0898f02 --- /dev/null +++ b/src/tgbaalgos/se05.cc @@ -0,0 +1,483 @@ +// Copyright (C) 2003, 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 +#include "misc/hash.hh" +#include +#include +#include +#include "magic.hh" + +namespace spot +{ + namespace + { + enum color {WHITE, CYAN, BLUE, RED}; + + /// \brief Emptiness checker on spot::tgba automata having at most one + /// accepting condition (i.e. a TBA). + template + class se05_search : public emptiness_check + { + public: + /// \brief Initialize the Magic Search algorithm on the automaton \a a + /// + /// \pre The automaton \a a must have at most one accepting + /// condition (i.e. it is a TBA). + se05_search(const tgba *a) + : current_weight(0), a(a), all_cond(a->all_acceptance_conditions()) + { + assert(a->number_of_acceptance_conditions() <= 1); + } + + virtual ~se05_search() + { + // Release all iterators on the stacks. + while (!st_blue.empty()) + { + h.pop_notify(st_blue.front().s); + delete st_blue.front().it; + st_blue.pop_front(); + } + while (!st_red.empty()) + { + h.pop_notify(st_red.front().s); + delete st_red.front().it; + st_red.pop_front(); + } + } + + /// \brief Perform a Magic Search. + /// + /// \return non null pointer iff the algorithm has found a + /// new accepting path. + /// + /// check() can be called several times (until it returns a null + /// pointer) to enumerate all the visited accepting paths. The method + /// visits only a finite set of accepting paths. + virtual emptiness_check_result* check() + { + nbn = nbt = 0; + sts = mdp = st_blue.size() + st_red.size(); + if (st_red.empty()) + { + assert(st_blue.empty()); + const state* s0 = a->get_init_state(); + ++nbn; + h.add_new_state(s0, CYAN); + push(st_blue, s0, bddfalse, bddfalse); + if (dfs_blue()) + return new result(*this); + } + else + { + h.pop_notify(st_red.front().s); + delete st_red.front().it; + st_red.pop_front(); + if (!st_red.empty() && dfs_red()) + return new result(*this); + else + if (dfs_blue()) + return new result(*this); + } + return 0; + } + + virtual std::ostream& print_stats(std::ostream &os) const + { + os << nbn << " distinct nodes visited" << std::endl; + os << nbt << " transitions explored" << std::endl; + os << mdp << " nodes for the maximal stack depth" << std::endl; + if (!st_red.empty()) + { + assert(!st_blue.empty()); + os << st_blue.size() + st_red.size() - 1 + << " nodes for the counter example" << std::endl; + } + return os; + } + + private: + /// \brief counters for statistics (number of distinct nodes, of + /// transitions and maximal stacks size. + int nbn, nbt, mdp, sts; + + struct stack_item + { + stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) + : s(n), it(i), label(l), acc(a) {}; + /// The visited state. + const state* s; + /// Design the next successor of \a s which has to be visited. + tgba_succ_iterator* it; + /// The label of the transition followed to reach \a s + /// (false for the first one). + bdd label; + /// The acc set of the transition followed to reach \a s + /// (false for the first one). + bdd acc; + }; + + typedef std::list stack_type; + + void push(stack_type& st, const state* s, + const bdd& label, const bdd& acc) + { + ++sts; + if (sts>mdp) + mdp = sts; + tgba_succ_iterator* i = a->succ_iter(s); + i->first(); + st.push_front(stack_item(s, i, label, acc)); + } + + /// \brief Stack of the blue dfs. + stack_type st_blue; + + /// \brief number of visited accepting arcs + /// in the blue stack. + int current_weight; + + /// \brief Stack of the red dfs. + stack_type st_red; + + /// \brief Map where each visited state is colored + /// by the last dfs visiting it. + heap h; + + /// The automata to check. + const tgba* a; + + /// The automata to check. + bdd all_cond; + + bool dfs_blue() + { + while (!st_blue.empty()) + { + stack_item& f = st_blue.front(); + if (!f.it->done()) + { + ++nbt; + const state *s_prime = f.it->current_state(); + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + typename heap::color_ref c = h.get_color_ref(s_prime); + if (c.is_null()) + // Go down the edge (f.s, , s_prime) + { + if (acc == all_cond) + ++current_weight; + ++nbn; + h.add_new_state(s_prime, CYAN, current_weight); + push(st_blue, s_prime, label, acc); + } + else // Backtrack the edge (f.s, , s_prime) + { + if (c.get() == CYAN && + (acc == all_cond || current_weight > c.get_weight())) + { + c.set(RED); + push(st_red, s_prime, label, acc); + return true; + } + else if (c.get() == BLUE && acc == all_cond) + { + // the test 'c.get() == BLUE' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. + c.set(RED); + push(st_red, s_prime, label, acc); + if (dfs_red()) + return true; + } + } + } + else + // Backtrack the edge + // (predecessor of f.s in st_blue, , f.s) + { + --sts; + stack_item f_dest(f); + delete f.it; + st_blue.pop_front(); + if (f_dest.acc == all_cond) + --current_weight; + typename heap::color_ref c = h.get_color_ref(f_dest.s); + assert(!c.is_null()); + if (c.get() == BLUE && f_dest.acc == all_cond + && !st_blue.empty()) + // the test 'c.get() == BLUE' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. + { + c.set(RED); + push(st_red, f_dest.s, f_dest.label, f_dest.acc); + if (dfs_red()) + return true; + } + else + { + c.set(BLUE); + h.pop_notify(f_dest.s); + } + } + } + return false; + } + + bool dfs_red() + { + assert(!st_red.empty()); + + while (!st_red.empty()) + { + stack_item& f = st_red.front(); + if (!f.it->done()) + { + ++nbt; + const state *s_prime = f.it->current_state(); + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + typename heap::color_ref c = h.get_color_ref(s_prime); + if (c.is_null()) + // Notice that this case is taken into account only to + // support successive calls to the check method. Without + // this functionnality => assert(c.is_null()) + // Go down the edge (f.s, , s_prime) + { + ++nbn; + h.add_new_state(s_prime, RED); + push(st_red, s_prime, label, acc); + } + else // Go down the edge (f.s, , s_prime) + { + if (c.get() == CYAN) + { + c.set(RED); + push(st_red, s_prime, label, acc); + return true; + } + if (c.get() == BLUE) + { + c.set(RED); + push(st_red, s_prime, label, acc); + } + } + } + else // Backtrack + { + --sts; + h.pop_notify(f.s); + delete f.it; + st_red.pop_front(); + } + } + return false; + } + + class result: public emptiness_check_result + { + public: + result(se05_search& ms) + : ms_(ms) + { + } + virtual tgba_run* accepting_run() + { + assert(!ms_.st_blue.empty()); + assert(!ms_.st_red.empty()); + + tgba_run* run = new tgba_run; + + typename stack_type::const_reverse_iterator i, j, end; + tgba_run::steps* l; + + const state* target = ms_.st_red.front().s; + + l = &run->prefix; + + i = ms_.st_blue.rbegin(); + end = ms_.st_blue.rend(); --end; + j = i; ++j; + for (; i != end; ++i, ++j) + { + if (l == &run->prefix && i->s->compare(target) == 0) + l = &run->cycle; + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + if (l == &run->prefix && i->s->compare(target) == 0) + l = &run->cycle; + assert(l == &run->cycle); + + j = ms_.st_red.rbegin(); + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + + i = j; ++j; + end = ms_.st_red.rend(); --end; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + return run; + } + private: + se05_search& ms_; + }; + + }; + + class explicit_se05_search_heap + { + typedef Sgi::hash_map hcyan_type; + typedef Sgi::hash_map hash_type; + public: + class color_ref + { + public: + color_ref(hash_type* h, hcyan_type* hc, const state* s, int w) + : is_cyan(true), weight(w), ph(h), phc(hc), ps(s), pc(0) + { + } + color_ref(color* c) + : is_cyan(false), weight(0), ph(0), phc(0), ps(0), pc(c) + { + } + int get() const + { + if (is_cyan) + return CYAN; // the color cyan is fixed to 0 + return *pc; + } + int get_weight() const + { + assert(is_cyan); + return weight; + } + void set(color c) + { + assert(!is_null()); + if (is_cyan) + { + phc->erase(ps); + ph->insert(std::make_pair(ps, c)); + } + else + { + *pc=c; + } + } + bool is_null() const + { + return !is_cyan && pc==0; + } + private: + bool is_cyan; + int weight; // weight of a cyan node + hash_type* ph; //point to the main hash table + hcyan_type* phc; // point to the hash table hcyan + const state* ps; // point to the state in hcyan + color *pc; // point to the color of a state stored in main hash table + }; + + explicit_se05_search_heap() + { + } + + ~explicit_se05_search_heap() + { + hcyan_type::const_iterator sc = hc.begin(); + while (sc != hc.end()) + { + const state* ptr = sc->first; + ++sc; + delete ptr; + } + hash_type::const_iterator s = h.begin(); + while (s != h.end()) + { + const state* ptr = s->first; + ++s; + delete ptr; + } + } + + color_ref get_color_ref(const state*& s) + { + hcyan_type::iterator ic = hc.find(s); + if (ic==hc.end()) + { + hash_type::iterator it = h.find(s); + if (it==h.end()) + return color_ref(0); // unknown state + if (s!=it->first) + { + delete s; + s = it->first; + } + return color_ref(&(it->second)); // blue or red state + } + if (s!=ic->first) + { + delete s; + s = ic->first; + } + return color_ref(&h, &hc, ic->first, ic->second); // cyan state + } + + void add_new_state(const state* s, color c, int w=0) + { + assert(hc.find(s)==hc.end() && h.find(s)==h.end()); + if (c == CYAN) + hc.insert(std::make_pair(s, w)); + else + h.insert(std::make_pair(s, c)); + } + + void pop_notify(const state*) + { + } + + private: + + hash_type h; + hcyan_type hc; + }; + + } // anonymous + + emptiness_check* explicit_se05_search(const tgba *a) + { + return new se05_search(a); + } + +} diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 0ffc81bb4..994f26283 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -80,9 +80,14 @@ TESTS = \ reduccmp.test \ reductgba.test \ emptchk.test \ + magic.test \ + se05.test \ emptchke.test \ + dfs.test \ spotlbtt.test EXTRA_DIST = $(TESTS) ltl2baw.pl -CLEANFILES = input input1 input2 input3 stdout expected config output1 output2 +CLEANFILES = input input1 input2 input3 stdout expected config output1 output2 \ +red blue_counter blue_last + diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test new file mode 100755 index 000000000..98e557c15 --- /dev/null +++ b/src/tgbatest/dfs.test @@ -0,0 +1,170 @@ +#!/bin/sh +# Copyright (C) 2003, 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. + + +. ./defs + +set -e + +cat >blue_counter <<'EOF' +acc = a; +s1, s2,, a; +s2, s3,,; +s3, s1,,; +s3, s4,,; +s4, s4,,; +s4, s5,,; +s4, s6,,; +s4, s7,,; +s4, s8,,; +s4, s9,,; +s5, s4,,; +s5, s5,,; +s5, s6,,; +s5, s7,,; +s5, s8,,; +s5, s9,,; +s6, s4,,; +s6, s5,,; +s6, s6,,; +s6, s7,,; +s6, s8,,; +s6, s9,,; +s7, s4,,; +s7, s5,,; +s7, s6,,; +s7, s7,,; +s7, s8,,; +s7, s9,,; +s8, s4,,; +s8, s5,,; +s8, s6,,; +s8, s7,,; +s8, s8,,; +s8, s9,,; +s9, s4,,; +s9, s5,,; +s9, s6,,; +s9, s7,,; +s9, s8,,; +s9, s9,,; +EOF + +run 0 ./ltl2tgba -emagic_search -X blue_counter +run 0 ./ltl2tgba -ese05_search -X blue_counter + +cat >blue_last <<'EOF' +acc = a; +s1, s2,,; +s2, s3,,; +s3, s1,, a; +s3, s4,,; +s4, s4,,; +s4, s5,,; +s4, s6,,; +s4, s7,,; +s4, s8,,; +s4, s9,,; +s5, s4,,; +s5, s5,,; +s5, s6,,; +s5, s7,,; +s5, s8,,; +s5, s9,,; +s6, s4,,; +s6, s5,,; +s6, s6,,; +s6, s7,,; +s6, s8,,; +s6, s9,,; +s7, s4,,; +s7, s5,,; +s7, s6,,; +s7, s7,,; +s7, s8,,; +s7, s9,,; +s8, s4,,; +s8, s5,,; +s8, s6,,; +s8, s7,,; +s8, s8,,; +s8, s9,,; +s9, s4,,; +s9, s5,,; +s9, s6,,; +s9, s7,,; +s9, s8,,; +s9, s9,,; +EOF + +run 0 ./ltl2tgba -emagic_search -X blue_last +run 0 ./ltl2tgba -ese05_search -X blue_last + +cat >red <<'EOF' +acc = a; +s1, s2,,; +s1, s3,, a; +s2, s3,,; +s3, s1,,; +s3, s4,,; +s4, s4,,; +s4, s5,,; +s4, s6,,; +s4, s7,,; +s4, s8,,; +s4, s9,,; +s5, s4,,; +s5, s5,,; +s5, s6,,; +s5, s7,,; +s5, s8,,; +s5, s9,,; +s6, s4,,; +s6, s5,,; +s6, s6,,; +s6, s7,,; +s6, s8,,; +s6, s9,,; +s7, s4,,; +s7, s5,,; +s7, s6,,; +s7, s7,,; +s7, s8,,; +s7, s9,,; +s8, s4,,; +s8, s5,,; +s8, s6,,; +s8, s7,,; +s8, s8,,; +s8, s9,,; +s9, s4,,; +s9, s5,,; +s9, s6,,; +s9, s7,,; +s9, s8,,; +s9, s9,,; +EOF + +run 0 ./ltl2tgba -emagic_search -X red +run 0 ./ltl2tgba -ese05_search -X red + +rm -f red blue_counter blue_last \ No newline at end of file diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 4f4e78f1d..b77d55497 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -43,6 +43,11 @@ expect_ce() expect_ce_do -ecouvreur99_shy -f -D "$1" expect_ce_do -emagic_search "$1" expect_ce_do -emagic_search -f "$1" + run 0 ./ltl2tgba -ese05_search "$1" + run 0 ./ltl2tgba -ese05_search -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 } expect_no() @@ -57,22 +62,24 @@ expect_no() run 0 ./ltl2tgba -Ecouvreur99_shy -f -D "$1" run 0 ./ltl2tgba -Emagic_search "$1" run 0 ./ltl2tgba -Emagic_search -f "$1" + run 0 ./ltl2tgba -Ese05_search "$1" + run 0 ./ltl2tgba -Ese05_search -f "$1" + test `./ltl2tgba -emagic_search_repeated "!($1)" | + grep Prefix: | wc -l` -ge $2 + test `./ltl2tgba -ese05_search_repeated "!($1)" | + grep Prefix: | wc -l` -ge $2 } -expect_ce 'a' -expect_ce 'a U b' -expect_ce 'X a' -expect_ce 'a & b & c' -expect_ce 'a | b | (c U (d & (g U (h ^ i))))' -expect_ce 'Xa & (b U !a) & (b U !a)' -expect_ce 'Fa & Xb & GFc & Gd' -expect_ce 'Fa & Xa & GFc & Gc' -expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -expect_ce '!((FF a) <=> (F x))' -expect_no '!((FF a) <=> (F a))' -expect_no 'Xa && (!a U b) && !b && X!b' -expect_no '(a U !b) && Gb' - -# Expect at least four accepting runs -test `./ltl2tgba -emagic_search_repeated 'FFx <=> Fx' | - grep Prefix: | wc -l` -ge 4 +expect_ce 'a' 1 +expect_ce 'a U b' 2 +expect_ce 'X a' 1 +expect_ce 'a & b & c' 1 +expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 2 +expect_ce 'Xa & (b U !a) & (b U !a)' 1 +expect_ce 'Fa & Xb & GFc & Gd' 1 +expect_ce 'Fa & Xa & GFc & Gc' 2 +expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1 +expect_ce '!((FF a) <=> (F x))' 3 +expect_no '!((FF a) <=> (F a))' 4 +expect_no 'Xa && (!a U b) && !b && X!b' 5 +expect_no '(a U !b) && Gb' 4 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6ab85dac0..cb41c38d5 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -119,7 +119,9 @@ syntax(char* prog) << " couvreur99 (the default)" << std::endl << " couvreur99_shy" << std::endl << " magic_search" << std::endl - << " magic_search_repeated" << std::endl; + << " magic_search_repeated" << std::endl + << " se05_search" << std::endl + << " se05_search_repeated" << std::endl; exit(2); } @@ -137,7 +139,7 @@ main(int argc, char** argv) int output = 0; int formula_index = 0; std::string echeck_algo; - enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None; + enum { None, Couvreur, Couvreur2, MagicSearch, Se04Search } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; bool expect_counter_example = false; @@ -347,6 +349,17 @@ main(int argc, char** argv) degeneralize_opt = true; magic_many = true; } + else if (echeck_algo == "se05_search") + { + echeck = Se04Search; + degeneralize_opt = true; + } + else if (echeck_algo == "se05_search_repeated") + { + echeck = Se04Search; + degeneralize_opt = true; + magic_many = true; + } else { std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl; @@ -569,7 +582,12 @@ main(int argc, char** argv) case MagicSearch: ec_a = degeneralized; - ec = new spot::magic_search(degeneralized); + ec = spot::explicit_magic_search(degeneralized); + break; + + case Se04Search: + ec_a = degeneralized; + ec = spot::explicit_se05_search(degeneralized); break; }