From 0f15d28fe8a723b4bf4329aaa4109309568f92cb Mon Sep 17 00:00:00 2001 From: Denis Poitrenaud Date: Mon, 22 Nov 2004 12:06:03 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, src/tgbaalgos/weight.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics capability. * src/tgbatest/randtgba.cc: Print these statistics. * src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance condition. * src/tgbatest/emptchk.test: Test tau03opt search. --- ChangeLog | 15 ++ src/tgbaalgos/Makefile.am | 7 +- src/tgbaalgos/emptiness_stats.hh | 83 +++++++ src/tgbaalgos/gtec/gtec.cc | 2 + src/tgbaalgos/gtec/gtec.hh | 3 +- src/tgbaalgos/gtec/status.cc | 6 + src/tgbaalgos/gtec/status.hh | 3 + src/tgbaalgos/magic.cc | 192 ++++++++++----- src/tgbaalgos/se05.cc | 292 +++++++++++----------- src/tgbaalgos/tau03.cc | 172 ++++++------- src/tgbaalgos/tau03opt.cc | 411 +++++++++++++++++++------------ src/tgbaalgos/weight.cc | 125 ++++++++++ src/tgbaalgos/weight.hh | 64 +++++ src/tgbatest/emptchk.test | 2 + src/tgbatest/ltl2tgba.cc | 11 +- src/tgbatest/randtgba.cc | 143 +++++++++-- 16 files changed, 1053 insertions(+), 478 deletions(-) create mode 100644 src/tgbaalgos/emptiness_stats.hh create mode 100644 src/tgbaalgos/weight.cc create mode 100644 src/tgbaalgos/weight.hh diff --git a/ChangeLog b/ChangeLog index d744ce6b0..cc187cc9b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2004-11-22 Poitrenaud Denis + + * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, + src/tgbaalgos/weight.hh: New files. + * src/tgbaalgos/Makefile.am: Add them. + * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, + src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc, + src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics + capability. + * src/tgbatest/randtgba.cc: Print these statistics. + * src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance + condition. + * src/tgbatest/emptchk.test: Test tau03opt search. + 2004-11-19 Alexandre Duret-Lutz * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index bcf8bfdb5..948157f86 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -31,6 +31,7 @@ tgbaalgos_HEADERS = \ dottydec.hh \ dupexp.hh \ emptiness.hh \ + emptiness_stats.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ @@ -47,7 +48,8 @@ tgbaalgos_HEADERS = \ stats.hh \ tau03.hh \ tau03opt.hh \ - reductgba_sim.hh + reductgba_sim.hh \ + weight.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ @@ -72,6 +74,7 @@ libtgbaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ reductgba_sim.cc \ - reductgba_sim_del.cc + reductgba_sim_del.cc \ + weight.cc libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh new file mode 100644 index 000000000..67f8344eb --- /dev/null +++ b/src/tgbaalgos/emptiness_stats.hh @@ -0,0 +1,83 @@ +// 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_EC_STATS_HH +# define SPOT_TGBAALGOS_EC_STATS_HH + +namespace spot +{ + + /// \addtogroup ec_misc + /// @{ + + class ec_statistics + { + public : + ec_statistics() + : states_(0), transitions_(0), depth_(0), max_depth_(0) + { + } + void set_states(int n) + { + states_ = n; + } + void inc_states() + { + ++states_; + } + void inc_transitions() + { + ++transitions_; + } + void inc_depth() + { + ++depth_; + if (depth_ > max_depth_) + max_depth_ = depth_; + } + void dec_depth() + { + --depth_; + } + int states() const + { + return states_; + } + int transitions() const + { + return transitions_; + } + int max_depth() const + { + return max_depth_; + } + + private : + unsigned states_; /// number of disctint visited states + unsigned transitions_; /// number of visited transitions + unsigned depth_; /// maximal depth of the stack(s) + unsigned max_depth_; /// maximal depth of the stack(s) + }; + + /// @} +} + +#endif // SPOT_TGBAALGOS_EC_STATS_HH diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index cc8e33013..01de5b7fe 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -221,6 +221,7 @@ namespace spot delete todo.top().second; todo.pop(); } + set_states(ecs_->states()); return new couvreur99_check_result(ecs_); } } @@ -344,6 +345,7 @@ namespace spot } todo.pop(); } + set_states(ecs_->states()); return new couvreur99_check_result(ecs_); } } diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index fb0541fa2..660c9f833 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -24,6 +24,7 @@ #include "status.hh" #include "tgbaalgos/emptiness.hh" +#include "tgbaalgos/emptiness_stats.hh" namespace spot { @@ -71,7 +72,7 @@ namespace spot /// tgba_succ_iterators: it must compute all successors of a state /// at once in order to decide which to explore first, and must keep /// a list of all unexplored successors in its DFS stack. - class couvreur99_check: public emptiness_check + class couvreur99_check: public emptiness_check, public ec_statistics { public: couvreur99_check(const tgba* a, diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc index 70b3c2fe7..ce741bf47 100644 --- a/src/tgbaalgos/gtec/status.cc +++ b/src/tgbaalgos/gtec/status.cc @@ -45,4 +45,10 @@ namespace spot << " strongly connected components in search stack" << std::endl; } + + int + couvreur99_check_status::states() const + { + return h->size(); + } } diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 2fe6c1fad..e52c5dc90 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -47,6 +47,9 @@ namespace spot /// Output statistics about this object. void print_stats(std::ostream& os) const; + + /// Return the number of states visited by the search + int states() const; }; } diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 90e005a88..dd07c5fde 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -19,11 +19,18 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +//#define TRACE + +#ifdef TRACE +#include +#endif + #include #include #include "misc/hash.hh" #include "tgba/tgba.hh" #include "emptiness.hh" +#include "emptiness_stats.hh" #include "magic.hh" namespace spot @@ -35,7 +42,7 @@ namespace spot /// \brief Emptiness checker on spot::tgba automata having at most one /// accepting condition (i.e. a TBA). template - class magic_search : public emptiness_check + class magic_search : public emptiness_check, public ec_statistics { public: /// \brief Initialize the Magic Search algorithm on the automaton \a a @@ -43,7 +50,10 @@ namespace spot /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). magic_search(const tgba *a, size_t size) - : h(size), a(a), all_cond(a->all_acceptance_conditions()) + : ec_statistics(), + h(size), + a(a), + all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -75,13 +85,11 @@ namespace spot /// 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; + inc_states(); h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) @@ -90,8 +98,7 @@ namespace spot else { h.pop_notify(st_red.front().s); - delete st_red.front().it; - st_red.pop_front(); + pop(st_red); if (!st_red.empty() && dfs_red()) return new result(*this); else @@ -103,9 +110,9 @@ namespace spot 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; + os << states() << " distinct nodes visited" << std::endl; + os << transitions() << " transitions explored" << std::endl; + os << max_depth() << " nodes for the maximal stack depth" << std::endl; if (!st_red.empty()) { assert(!st_blue.empty()); @@ -116,9 +123,6 @@ namespace spot } private: - /// \brief counters for statistics (number of distinct nodes, of - /// transitions and maximal stacks size. - int nbn, nbt, mdp, sts; struct stack_item { @@ -141,14 +145,19 @@ namespace spot void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { - ++sts; - if (sts>mdp) - mdp = sts; + inc_depth(); tgba_succ_iterator* i = a->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } + void pop(stack_type& st) + { + dec_depth(); + delete st.front().it; + st.pop_front(); + } + /// \brief Stack of the blue dfs. stack_type st_blue; @@ -173,64 +182,98 @@ namespace spot while (!st_blue.empty()) { stack_item& f = st_blue.front(); +# ifdef TRACE + std::cout << "DFS_BLUE treats: " + << a->format_state(f.s) << std::endl; +# endif if (!f.it->done()) { - ++nbt; const state *s_prime = f.it->current_state(); +# ifdef TRACE + std::cout << " Visit the successor: " + << a->format_state(s_prime) << std::endl; +# endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) - // Go down the edge (f.s, , s_prime) { - ++nbn; +# ifdef TRACE + std::cout << " It is white, go down" << std::endl; +# endif + inc_states(); h.add_new_state(s_prime, BLUE); push(st_blue, s_prime, label, acc); } - else // Backtrack the edge (f.s, , s_prime) + else { - if (c.get() != RED && acc == all_cond) - // the test 'c.get() != RED' is added to limit - // the number of runs reported by successive - // calls to the check method. Without this - // functionnality, the test can be ommited. + if (acc == all_cond && c.get_color() != RED) { + // the test 'c.get_color() != RED' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. +# ifdef TRACE + std::cout << " It is blue and the arc is " + << "accepting, start a red dfs" << std::endl; +# endif target = f.s; - c.set(RED); + c.set_color(RED); push(st_red, s_prime, label, acc); if (dfs_red()) return true; } else - h.pop_notify(s_prime); + { +# ifdef TRACE + std::cout << " It is blue or red, pop it" << std::endl; +# endif + h.pop_notify(s_prime); + } } } else // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { - --sts; +# ifdef TRACE + std::cout << " All the successors have been visited" + << std::endl; +# endif stack_item f_dest(f); - delete f.it; - st_blue.pop_front(); + pop(st_blue); typename heap::color_ref c = h.get_color_ref(f_dest.s); assert(!c.is_white()); - if (c.get() != RED && f_dest.acc == all_cond - && !st_blue.empty()) - // the test 'c.get() != RED' is added to limit - // the number of runs reported by successive - // calls to the check method. Without this - // functionnality, the test can be ommited. + if (!st_blue.empty() && + f_dest.acc == all_cond && c.get_color() != RED) { + // the test 'c.get_color() != RED' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. +# ifdef TRACE + std::cout << " It is blue and the arc from " + << a->format_state(st_blue.front().s) + << " to it is accepting, start a red dfs" + << std::endl; +# endif target = st_blue.front().s; - c.set(RED); + c.set_color(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); + { +# ifdef TRACE + std::cout << " Pop it" + << std::endl; +# endif + h.pop_notify(f_dest.s); + } } } return false; @@ -245,40 +288,63 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); - if (!f.it->done()) // Go down +# ifdef TRACE + std::cout << "DFS_RED treats: " + << a->format_state(f.s) << std::endl; +# endif + if (!f.it->done()) { - ++nbt; const state *s_prime = f.it->current_state(); +# ifdef TRACE + std::cout << " Visit the successor: " + << a->format_state(s_prime) << std::endl; +# endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) - // Go down the edge (f.s, , s_prime) { - ++nbn; - h.add_new_state(s_prime, RED); - push(st_red, s_prime, label, acc); + // If the red dfs find a white here, it must have crossed + // the blue stack and the target must be reached soon. + // Notice that this property holds only for explicit search. + // Collisions in bit-state hashing search can also lead + // to the visit of white state. Anyway, it is not necessary + // to visit white states either if a cycle can be missed + // with bit-state hashing search. +# ifdef TRACE + std::cout << " It is white, pop it" << std::endl; +# endif + delete s_prime; } - else // Go down the edge (f.s, , s_prime) + else if (c.get_color() == BLUE) { - if (c.get() != RED) - { - c.set(RED); - push(st_red, s_prime, label, acc); - if (target->compare(s_prime) == 0) - return true; - } - else - h.pop_notify(s_prime); +# ifdef TRACE + std::cout << " It is blue, go down" << std::endl; +# endif + c.set_color(RED); + push(st_red, s_prime, label, acc); + if (target->compare(s_prime) == 0) + return true; + } + else + { +# ifdef TRACE + std::cout << " It is red, pop it" << std::endl; +# endif + h.pop_notify(s_prime); } } else // Backtrack { - --sts; +# ifdef TRACE + std::cout << " All the successors have been visited, pop it" + << std::endl; +# endif h.pop_notify(f.s); - delete f.it; - st_red.pop_front(); + pop(st_red); } } return false; @@ -343,11 +409,11 @@ namespace spot color_ref(color* c) :p(c) { } - color get() const + color get_color() const { return *p; } - void set(color c) + void set_color(color c) { assert(!is_white()); *p=c; @@ -415,17 +481,17 @@ namespace spot color_ref(unsigned char *b, unsigned char o): base(b), offset(o*2) { } - color get() const + color get_color() const { return color(((*base) >> offset) & 3U); } - void set(color c) + void set_color(color c) { *base = (*base & ~(3U << offset)) | (c << offset); } bool is_white() const { - return get()==WHITE; + return get_color()==WHITE; } private: unsigned char *base; @@ -454,7 +520,7 @@ namespace spot { color_ref cr(get_color_ref(s)); assert(cr.is_white()); - cr.set(c); + cr.set_color(c); } void pop_notify(const state* s) diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index f47280e8e..76a6c8506 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -30,8 +30,11 @@ #include "misc/hash.hh" #include "tgba/tgba.hh" #include "emptiness.hh" +#include "emptiness_stats.hh" #include "se05.hh" +/// FIXME: make compiling depedent the taking into account of weights. + namespace spot { namespace @@ -41,7 +44,7 @@ namespace spot /// \brief Emptiness checker on spot::tgba automata having at most one /// accepting condition (i.e. a TBA). template - class se05_search : public emptiness_check + class se05_search : public emptiness_check, public ec_statistics { public: /// \brief Initialize the Magic Search algorithm on the automaton \a a @@ -49,8 +52,11 @@ namespace spot /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). se05_search(const tgba *a, size_t size) - : current_weight(0), h(size), - a(a), all_cond(a->all_acceptance_conditions()) + : ec_statistics(), + current_weight(0), + h(size), + a(a), + all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -82,13 +88,11 @@ namespace spot /// 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; + inc_states(); h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) @@ -97,8 +101,7 @@ namespace spot else { h.pop_notify(st_red.front().s); - delete st_red.front().it; - st_red.pop_front(); + pop(st_red); if (!st_red.empty() && dfs_red()) return new result(*this); else @@ -110,9 +113,9 @@ namespace spot 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; + os << states() << " distinct nodes visited" << std::endl; + os << transitions() << " transitions explored" << std::endl; + os << max_depth() << " nodes for the maximal stack depth" << std::endl; if (!st_red.empty()) { assert(!st_blue.empty()); @@ -123,9 +126,6 @@ namespace spot } private: - /// \brief counters for statistics (number of distinct nodes, of - /// transitions and maximal stacks size. - int nbn, nbt, mdp, sts; struct stack_item { @@ -148,21 +148,26 @@ namespace spot void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { - ++sts; - if (sts>mdp) - mdp = sts; + inc_depth(); 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; + void pop(stack_type& st) + { + dec_depth(); + delete st.front().it; + st.pop_front(); + } /// \brief number of visited accepting arcs /// in the blue stack. int current_weight; + /// \brief Stack of the blue dfs. + stack_type st_blue; + /// \brief Stack of the red dfs. stack_type st_red; @@ -173,7 +178,7 @@ namespace spot /// The automata to check. const tgba* a; - /// The automata to check. + /// The unique accepting condition of the automaton \a a. bdd all_cond; bool dfs_blue() @@ -181,110 +186,110 @@ namespace spot while (!st_blue.empty()) { stack_item& f = st_blue.front(); -#ifdef TRACE +# ifdef TRACE std::cout << "DFS_BLUE treats: " << a->format_state(f.s) << std::endl; -#endif +# endif 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(); -#ifdef TRACE +# ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) - // Go down the edge (f.s, , s_prime) { +# ifdef TRACE + std::cout << " It is white, go down" << std::endl; +# endif if (acc == all_cond) ++current_weight; - ++nbn; -#ifdef TRACE - std::cout << " It is white, go down" << std::endl; -#endif + inc_states(); h.add_new_state(s_prime, CYAN, current_weight); push(st_blue, s_prime, label, acc); } - else // Backtrack the edge (f.s, , s_prime) + else if (c.get_color() == CYAN && (acc == all_cond || + (f.s->compare(s_prime) != 0 && f.acc == all_cond) // option SE05 +// current_weight > c.get_weight() // option WEIGHT + /**/)) +// For Alexandre: combat style.test! ----------^ { - if (c.get() == CYAN && - (acc == all_cond || current_weight > c.get_weight())) - { -#ifdef TRACE - std::cout << " It is cyan and a cycle has been found" - << std::endl; -#endif - c.set(RED); - push(st_red, s_prime, label, acc); - return true; - } - else if (c.get() != RED && acc == all_cond) - { -#ifdef TRACE - std::cout << " It is blue and the arc is accepting" - << ", start a red dfs" << std::endl; -#endif - // the test 'c.get() != RED' 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 -#ifdef TRACE - std::cout << " It is blue or red, pop it" - << std::endl; -#endif - h.pop_notify(s_prime); +# ifdef TRACE + std::cout << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; +# endif + c.set_color(RED); + push(st_red, s_prime, label, acc); + return true; + } + else if (acc == all_cond && c.get_color() != RED) + { + // the test 'c.get_color() != RED' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. +# ifdef TRACE + std::cout << " It is cyan or blue and the arc is " + << "accepting, start a red dfs" << std::endl; +# endif + c.set_color(RED); + push(st_red, s_prime, label, acc); + if (dfs_red()) + return true; + } + else + { +# ifdef TRACE + std::cout << " It is cyan, blue or red, pop it" + << std::endl; +# endif + h.pop_notify(s_prime); } } else // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -#ifdef TRACE +# ifdef TRACE std::cout << " All the successors have been visited" << std::endl; -#endif - --sts; +# endif stack_item f_dest(f); - delete f.it; - st_blue.pop_front(); + pop(st_blue); if (f_dest.acc == all_cond) --current_weight; typename heap::color_ref c = h.get_color_ref(f_dest.s); assert(!c.is_white()); - if (c.get() != RED && f_dest.acc == all_cond - && !st_blue.empty()) - // the test 'c.get() != RED' is added to limit - // the number of runs reported by successive - // calls to the check method. Without this - // functionnality, the test can be ommited. + if (!st_blue.empty() && + f_dest.acc == all_cond && c.get_color() != RED) { -#ifdef TRACE + // the test 'c.get_color() != RED' is added to limit + // the number of runs reported by successive + // calls to the check method. Without this + // functionnality, the test can be ommited. +# ifdef TRACE std::cout << " The arc from " << a->format_state(st_blue.front().s) - << " to the current state is accepting," - << " start a red dfs" << std::endl; -#endif - c.set(RED); + << " to the current state is accepting, start a " + << "red dfs" << std::endl; +# endif + c.set_color(RED); push(st_red, f_dest.s, f_dest.label, f_dest.acc); if (dfs_red()) return true; } else { -#ifdef TRACE - std::cout << " Set it blue and pop it" << std::endl; -#endif - c.set(BLUE); +# ifdef TRACE + std::cout << " Pop it" << std::endl; +# endif + c.set_color(BLUE); h.pop_notify(f_dest.s); } } @@ -299,70 +304,72 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -#ifdef TRACE +# ifdef TRACE std::cout << "DFS_RED treats: " << a->format_state(f.s) << std::endl; -#endif +# endif 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(); -#ifdef TRACE +# ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) - // Go down the edge (f.s, , s_prime) { -#ifdef TRACE - std::cout << " It is white, go down" << std::endl; -#endif - ++nbn; - h.add_new_state(s_prime, RED); - push(st_red, s_prime, label, acc); + // For an explicit search, we can pose assert(!c.is_white()) + // because to reach a white state, the red dfs must + // have crossed a cyan one (a state in the blue stack) + // implying the report of a cycle. + // However, with a bit-state hashing search and due to + // collision, this property does not hold. +# ifdef TRACE + std::cout << " It is white (due to collision), pop it" + << std::endl; +# endif + delete s_prime; } - else // Go down the edge (f.s, , s_prime) + else if (c.get_color() == RED) { - if (c.get() == CYAN) - { -#ifdef TRACE - std::cout << " It is cyan, report a cycle" - << std::endl; -#endif - c.set(RED); - push(st_red, s_prime, label, acc); - return true; - } - if (c.get() == BLUE) - { -#ifdef TRACE - std::cout << " It is blue, go down" << std::endl; -#endif - c.set(RED); - push(st_red, s_prime, label, acc); - } - else -#ifdef TRACE - std::cout << " It is red, pop it" - << std::endl; -#endif - h.pop_notify(s_prime); +# ifdef TRACE + std::cout << " It is red, pop it" + << std::endl; +# endif + h.pop_notify(s_prime); + } + else if (c.get_color() == CYAN) + { +# ifdef TRACE + std::cout << " It is cyan, report a cycle" + << std::endl; +# endif + c.set_color(RED); + push(st_red, s_prime, label, acc); + return true; + } + else + { +# ifdef TRACE + std::cout << " It is blue, go down" << std::endl; +# endif + c.set_color(RED); + push(st_red, s_prime, label, acc); } } else // Backtrack { -#ifdef TRACE - std::cout << " All the successors have been visited" - << ", pop it" << std::endl; -#endif - --sts; +# ifdef TRACE + std::cout << " All the successors have been visited, pop it" + << std::endl; +# endif h.pop_notify(f.s); - delete f.it; - st_red.pop_front(); + pop(st_red); } } return false; @@ -442,7 +449,7 @@ namespace spot : is_cyan(false), weight(0), ph(0), phc(0), ps(0), pc(c) { } - color get() const + color get_color() const { if (is_cyan) return CYAN; @@ -453,11 +460,12 @@ namespace spot assert(is_cyan); return weight; } - void set(color c) + void set_color(color c) { assert(!is_white()); if (is_cyan) { + assert(c != CYAN); int i = phc->erase(ps); assert(i==1); (void)i; @@ -510,7 +518,7 @@ namespace spot { hash_type::iterator it = h.find(s); if (it==h.end()) - return color_ref(0); // unknown state + return color_ref(0); // white state if (s!=it->first) { delete s; @@ -564,7 +572,7 @@ namespace spot : is_cyan(false), weight(0), phc(0), ps(0), b(base), o(offset*2) { } - color get() const + color get_color() const { if (is_cyan) return CYAN; @@ -575,7 +583,7 @@ namespace spot assert(is_cyan); return weight; } - void set(color c) + void set_color(color c) { if (is_cyan && c!=CYAN) { @@ -587,15 +595,7 @@ namespace spot } bool is_white() const { - return !is_cyan && get()==WHITE; - } - const unsigned char* base() const - { - return b; - } - unsigned char offset() const - { - return o; + return get_color()==WHITE; } private: bool is_cyan; @@ -635,7 +635,7 @@ namespace spot else { color_ref cr(get_color_ref(s)); - cr.set(c); + cr.set_color(c); } } diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 52646453f..07e894bbe 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -35,6 +35,7 @@ #include "misc/hash.hh" #include "tgba/tgba.hh" #include "emptiness.hh" +#include "emptiness_stats.hh" #include "tau03.hh" namespace spot @@ -46,12 +47,15 @@ namespace spot /// \brief Emptiness checker on spot::tgba automata having at most one /// accepting condition (i.e. a TBA). template - class tau03_search : public emptiness_check + class tau03_search : public emptiness_check, public ec_statistics { public: /// \brief Initialize the search algorithm on the automaton \a a tau03_search(const tgba *a, size_t size) - : h(size), a(a), all_cond(a->all_acceptance_conditions()) + : ec_statistics(), + h(size), + a(a), + all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() > 0); } @@ -80,14 +84,10 @@ namespace spot virtual emptiness_check_result* check() { if (!st_blue.empty()) - { return 0; - } assert(st_red.empty()); - nbn = nbt = 0; - sts = mdp = 0; const state* s0 = a->get_init_state(); - ++nbn; + inc_states(); h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) @@ -97,17 +97,13 @@ namespace spot 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; + os << states() << " distinct nodes visited" << std::endl; + os << transitions() << " transitions explored" << std::endl; + os << max_depth() << " nodes for the maximal stack depth" << 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) @@ -129,14 +125,19 @@ namespace spot void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { - ++sts; - if (sts>mdp) - mdp = sts; + inc_depth(); tgba_succ_iterator* i = a->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } + void pop(stack_type& st) + { + dec_depth(); + delete st.front().it; + st.pop_front(); + } + /// \brief Stack of the blue dfs. stack_type st_blue; @@ -158,37 +159,37 @@ namespace spot while (!st_blue.empty()) { stack_item& f = st_blue.front(); -#ifdef TRACE +# ifdef TRACE std::cout << "DFS_BLUE treats: " << a->format_state(f.s) << std::endl; -#endif +# endif 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(); -#ifdef TRACE +# ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) - // Go down the edge (f.s, , s_prime) { - ++nbn; -#ifdef TRACE +# ifdef TRACE std::cout << " It is white, go down" << std::endl; -#endif +# endif + inc_states(); h.add_new_state(s_prime, BLUE); push(st_blue, s_prime, label, acc); } - else // Backtrack the edge (f.s, , s_prime) + else { -#ifdef TRACE +# ifdef TRACE std::cout << " It is blue, pop it" << std::endl; -#endif +# endif h.pop_notify(s_prime); } } @@ -196,31 +197,31 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -#ifdef TRACE +# ifdef TRACE std::cout << " All the successors have been visited" << ", rescan this successors" << std::endl; -#endif +# endif typename heap::color_ref c = h.get_color_ref(f.s); assert(!c.is_white()); tgba_succ_iterator* i = a->succ_iter(f.s); for (i->first(); !i->done(); i->next()) { - ++nbt; - const state *s_prime = i->current_state(); + inc_transitions(); + const state *s_prime = i->current_state(); +#ifdef TRACE + std::cout << "DFS_BLUE rescanning the arc from " + << a->format_state(f.s) << " to " + << a->format_state(s_prime) << std::endl; +# endif bdd label = i->current_condition(); bdd acc = i->current_acceptance_conditions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); assert(!c_prime.is_white()); bdd acu = acc | c.get_acc(); -#ifdef TRACE - std::cout << "DFS_BLUE rescanning the arc from " - << a->format_state(f.s) << " to " - << a->format_state(s_prime) << std::endl; -#endif if ((c_prime.get_acc() & acu) != acu) { -#ifdef TRACE +# ifdef TRACE std::cout << " "; bdd_print_acc(std::cout, a->get_dict(), acu); std::cout << " is not included in "; @@ -232,7 +233,7 @@ namespace spot << " propagating: "; bdd_print_acc(std::cout, a->get_dict(), acu); std::cout << std::endl; -#endif +# endif c_prime.cumulate_acc(acu); push(st_red, s_prime, label, acc); dfs_red(acu); @@ -241,12 +242,21 @@ namespace spot delete i; if (c.get_acc() == all_cond) { +#ifdef TRACE + std::cout << "DFS_BLUE propagation is successful, report a" + << " cycle" << std::endl; +# endif return true; } - delete f.it; - --sts; - h.pop_notify(f.s); - st_blue.pop_front(); + else + { +#ifdef TRACE + std::cout << "DFS_BLUE propagation is unsuccessful, pop it"; + << std::endl; +# endif + h.pop_notify(f.s); + pop(st_blue); + } } } return false; @@ -259,60 +269,56 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -#ifdef TRACE +#ifdef TRACE std::cout << "DFS_RED treats: " << a->format_state(f.s) << std::endl; -#endif - if (!f.it->done()) // Go down +# endif + 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(); -#ifdef TRACE +#ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); - if (!c_prime.is_white()) + if (c_prime.is_white()) { - if ((c_prime.get_acc() & acu) != acu) - { -#ifdef TRACE - std::cout << " It is blue and propagation " - << "is needed, go down" << std::endl; -#endif - c_prime.cumulate_acc(acu); - push(st_red, s_prime, label, acc); - } - else - { -#ifdef TRACE - std::cout << " It is blue and no propagation " - << "is needed, pop it" << std::endl; -#endif - h.pop_notify(s_prime); - } +# ifdef TRACE + std::cout << " It is white, pop it" << std::endl; +# endif + delete s_prime; + } + else if ((c_prime.get_acc() & acu) != acu) + { +# ifdef TRACE + std::cout << " It is blue and propagation " + << "is needed, go down" << std::endl; +# endif + c_prime.cumulate_acc(acu); + push(st_red, s_prime, label, acc); } else { -#ifdef TRACE - std::cout << " It is white, pop it" << std::endl; -#endif - delete s_prime; +# ifdef TRACE + std::cout << " It is blue and no propagation " + << "is needed, pop it" << std::endl; +# endif + h.pop_notify(s_prime); } } else // Backtrack { -#ifdef TRACE - std::cout << " All the successors have been visited" - << ", pop it" << std::endl; -#endif - --sts; +# ifdef TRACE + std::cout << " All the successors have been visited, pop it" + << std::endl; +# endif h.pop_notify(f.s); - delete f.it; - st_red.pop_front(); + pop(st_red); } } } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index fd9db45c6..d53190717 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -19,10 +19,23 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// FIXME: Add -/// - the optimisation based on weights (a weight by accepting conditions), -/// - the computation of a counter example if detected. -/// - a bit-state hashing version. +/// FIXME: +/// +/// * Add the computation of a counter example if detected. +/// +/// * Add some heuristics on the order of visit of the successors in the blue +/// dfs: +/// - favorize the arcs conducting to the blue stack (the states of color +/// cyan) +/// - in this category, favorize the arcs labelled +/// - for the remaining ones, favorize the arcs labelled by the greatest +/// number of new acceptance conditions (notice that this number may evolve +/// after the visit of previous successors). +/// +/// * Add a bit-state hashing version. +/// +/// * Is it possible to reduce the tgba on-the-fly during the product: only the +/// acceptance conditions are pertinent... //#define TRACE @@ -36,7 +49,9 @@ #include "misc/hash.hh" #include "tgba/tgba.hh" #include "emptiness.hh" +#include "emptiness_stats.hh" #include "tau03opt.hh" +#include "weight.hh" namespace spot { @@ -47,14 +62,17 @@ namespace spot /// \brief Emptiness checker on spot::tgba automata having at most one /// accepting condition (i.e. a TBA). template - class tau03_opt_search : public emptiness_check + class tau03_opt_search : public emptiness_check, public ec_statistics { public: /// \brief Initialize the search algorithm on the automaton \a a tau03_opt_search(const tgba *a, size_t size) - : h(size), a(a), all_acc(a->all_acceptance_conditions()) + : ec_statistics(), + current_weight(a->neg_acceptance_conditions()), + h(size), + a(a), + all_acc(a->all_acceptance_conditions()) { - assert(a->number_of_acceptance_conditions() > 0); } virtual ~tau03_opt_search() @@ -80,17 +98,12 @@ namespace spot /// accepting path. virtual emptiness_check_result* check() { - if (!st_red.empty()) - { - assert(!st_blue.empty()); + if (!st_blue.empty()) return 0; - } - assert(st_blue.empty()); - nbn = nbt = 0; - sts = mdp = 0; + assert(st_red.empty()); const state* s0 = a->get_init_state(); - ++nbn; - h.add_new_state(s0, CYAN); + inc_states(); + h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) return new emptiness_check_result; @@ -99,17 +112,13 @@ namespace spot 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; + os << states() << " distinct nodes visited" << std::endl; + os << transitions() << " transitions explored" << std::endl; + os << max_depth() << " nodes for the maximal stack depth" << 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) @@ -131,14 +140,22 @@ namespace spot void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { - ++sts; - if (sts>mdp) - mdp = sts; + inc_depth(); tgba_succ_iterator* i = a->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } + void pop(stack_type& st) + { + dec_depth(); + delete st.front().it; + st.pop_front(); + } + + /// \brief weight of the state on top of the blue stack. + weight current_weight; + /// \brief Stack of the blue dfs. stack_type st_blue; @@ -160,30 +177,31 @@ namespace spot while (!st_blue.empty()) { stack_item& f = st_blue.front(); -#ifdef TRACE +# ifdef TRACE std::cout << "DFS_BLUE treats: " << a->format_state(f.s) << std::endl; -#endif +# endif 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(); -#ifdef TRACE +# ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) - // Go down the edge (f.s, , s_prime) { - ++nbn; -#ifdef TRACE +# ifdef TRACE std::cout << " It is white, go down" << std::endl; -#endif - h.add_new_state(s_prime, CYAN); +# endif + current_weight += acc; + inc_states(); + h.add_new_state(s_prime, CYAN, current_weight); push(st_blue, s_prime, label, acc); } else @@ -191,23 +209,47 @@ namespace spot typename heap::color_ref c = h.get_color_ref(f.s); assert(!c.is_white()); if (c_prime.get_color() == CYAN && - (c.get_acc() | acc | c_prime.get_acc()) == all_acc) + ((current_weight - c_prime.get_weight()) | + c.get_acc() | acc | c_prime.get_acc()) == all_acc) { -#ifdef TRACE - std::cout << " It is cyan and acceptance condition " - << "is reached, report cycle" << std::endl; -#endif +# ifdef TRACE + std::cout << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; +# endif c_prime.cumulate_acc(c.get_acc() | acc); push(st_red, s_prime, label, acc); return true; } - else // Backtrack the edge (f.s, , s_prime) + else { -#ifdef TRACE - std::cout << " It is cyan or blue, pop it" - << std::endl; -#endif - h.pop_notify(s_prime); +# ifdef TRACE + std::cout << " It is cyan or blue and"; +# endif + bdd acu = acc | c.get_acc(); + if ((c_prime.get_acc() & acu) != acu) + { +# ifdef TRACE + bdd_print_acc(std::cout, a->get_dict(), acu); + std::cout << " is not included in "; + bdd_print_acc(std::cout, a->get_dict(), + c_prime.get_acc()); + std::cout << ", start a red dfs propagating: "; + bdd_print_acc(std::cout, a->get_dict(), acu); + std::cout << std::endl; +# endif + c_prime.cumulate_acc(acu); + push(st_red, s_prime, label, acc); + if (dfs_red(acu)) + return true; + } + else + { +# ifdef TRACE + std::cout << " no propagation is needed, pop it." + << std::endl; +# endif + h.pop_notify(s_prime); + } } } } @@ -215,58 +257,52 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -#ifdef TRACE +# ifdef TRACE std::cout << " All the successors have been visited" - << ", rescan this successors" << std::endl; -#endif - typename heap::color_ref c = h.get_color_ref(f.s); - assert(!c.is_white()); - tgba_succ_iterator* i = a->succ_iter(f.s); - for (i->first(); !i->done(); i->next()) +# endif + stack_item f_dest(f); + pop(st_blue); + current_weight -= f_dest.acc; + typename heap::color_ref c_prime = h.get_color_ref(f_dest.s); + assert(!c_prime.is_white()); + c_prime.set_color(BLUE); + if (!st_blue.empty()) { - ++nbt; - const state *s_prime = i->current_state(); - bdd label = i->current_condition(); - bdd acc = i->current_acceptance_conditions(); - typename heap::color_ref c_prime = h.get_color_ref(s_prime); - assert(!c_prime.is_white()); - bdd acu = acc | c.get_acc(); -#ifdef TRACE - std::cout << "DFS_BLUE rescanning the arc from " - << a->format_state(f.s) << " to " - << a->format_state(s_prime) << std::endl; -#endif + typename heap::color_ref c = + h.get_color_ref(st_blue.front().s); + assert(!c.is_white()); + bdd acu = f_dest.acc | c.get_acc(); if ((c_prime.get_acc() & acu) != acu) { -#ifdef TRACE - std::cout << " "; - bdd_print_acc(std::cout, a->get_dict(), acu); - std::cout << " is not included in "; - bdd_print_acc(std::cout, a->get_dict(), - c_prime.get_acc()); +# ifdef TRACE + std::cout << " The arc from " + << a->format_state(st_blue.front().s) + << " to the current state implies to " + << " start a red dfs propagating "; + bdd_print_acc(std::cout, a->get_dict(), acu); std::cout << std::endl; - std::cout << " Start a red dfs from " - << a->format_state(s_prime) - << " propagating: "; - bdd_print_acc(std::cout, a->get_dict(), acu); - std::cout << std::endl; -#endif +# endif c_prime.cumulate_acc(acu); - push(st_red, s_prime, label, acc); + push(st_red, f_dest.s, f_dest.label, f_dest.acc); if (dfs_red(acu)) - { - delete i; return true; - } - } + } + else + { +# ifdef TRACE + std::cout << " Pop it" << std::endl; +# endif + h.pop_notify(f_dest.s); + } + } + else + { +# ifdef TRACE + std::cout << " Pop it" << std::endl; +# endif + h.pop_notify(f_dest.s); } - delete i; - c.set_color(BLUE); - delete f.it; - --sts; - h.pop_notify(f.s); - st_blue.pop_front(); } } return false; @@ -279,72 +315,69 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -#ifdef TRACE +# ifdef TRACE std::cout << "DFS_RED treats: " << a->format_state(f.s) << std::endl; -#endif - if (!f.it->done()) // Go down +# endif + 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(); -#ifdef TRACE +# ifdef TRACE std::cout << " Visit the successor: " << a->format_state(s_prime) << std::endl; -#endif +# endif + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + // Go down the edge (f.s, , s_prime) f.it->next(); + inc_transitions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); - if (!c_prime.is_white()) + if (c_prime.is_white()) { - if (c_prime.get_color() == CYAN && - (c_prime.get_acc() | acu) == all_acc) - { -#ifdef TRACE - std::cout << " It is cyan and acceptance condition " - << "is reached, report cycle" << std::endl; -#endif - c_prime.cumulate_acc(acu); - push(st_red, s_prime, label, acc); - return true; - } - else if ((c_prime.get_acc() & acu) != acu) - { -#ifdef TRACE - std::cout << " It is cyan or blue and propagation " - << "is needed, go down" - << std::endl; -#endif - c_prime.cumulate_acc(acu); - push(st_red, s_prime, label, acc); - } - else - { -#ifdef TRACE - std::cout << " It is cyan or blue and no propagation " - << "is needed , pop it" << std::endl; -#endif - h.pop_notify(s_prime); - } +# ifdef TRACE + std::cout << " It is white, pop it" << std::endl; +# endif + delete s_prime; + } + else if (c_prime.get_color() == CYAN && + ((current_weight - c_prime.get_weight()) | + c_prime.get_acc() | acu) == all_acc) + { +# ifdef TRACE + std::cout << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; +# endif + c_prime.cumulate_acc(acu); + push(st_red, s_prime, label, acc); + return true; + } + else if ((c_prime.get_acc() & acu) != acu) + { +# ifdef TRACE + std::cout << " It is cyan or blue and propagation " + << "is needed, go down" + << std::endl; +# endif + c_prime.cumulate_acc(acu); + push(st_red, s_prime, label, acc); } else { -#ifdef TRACE - std::cout << " It is white, pop it" << std::endl; -#endif - delete s_prime; +# ifdef TRACE + std::cout << " It is cyan or blue and no propagation " + << "is needed , pop it" << std::endl; +# endif + h.pop_notify(s_prime); } } else // Backtrack { -#ifdef TRACE - std::cout << " All the successors have been visited" - << ", pop it" << std::endl; -#endif - --sts; +# ifdef TRACE + std::cout << " All the successors have been visited, pop it" + << std::endl; +# endif h.pop_notify(f.s); - delete f.it; - st_red.pop_front(); + pop(st_red); } } return false; @@ -354,21 +387,52 @@ namespace spot class explicit_tau03_opt_search_heap { + typedef Sgi::hash_map, + state_ptr_hash, state_ptr_equal> hcyan_type; + typedef Sgi::hash_map, + state_ptr_hash, state_ptr_equal> hash_type; public: class color_ref { public: - color_ref(color* c, bdd* a) :p(c), acc(a) + color_ref(hash_type* h, hcyan_type* hc, const state* s, + const weight* w, bdd* a) + : is_cyan(true), w(w), ph(h), phc(hc), ps(s), acc(a) + { + } + color_ref(color* c, bdd* a) + : is_cyan(false), pc(c), acc(a) { } color get_color() const { - return *p; + if (is_cyan) + return CYAN; + return *pc; + } + const weight& get_weight() const + { + assert(is_cyan); + return *w; } void set_color(color c) { assert(!is_white()); - *p = c; + if (is_cyan) + { + assert(c != CYAN); + std::pair p; + p = ph->insert(std::make_pair(ps, std::make_pair(c, *acc))); + assert(p.second); + acc = &(p.first->second.second); + int i = phc->erase(ps); + assert(i==1); + (void)i; + } + else + { + *pc=c; + } } const bdd& get_acc() const { @@ -382,11 +446,17 @@ namespace spot } bool is_white() const { - return p == 0; + return !is_cyan && pc == 0; } private: - color *p; - bdd* acc; + bool is_cyan; + const weight* w; // point to the weight of a state in hcyan + 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 + bdd* acc; // point to the acc set of a state stored in main hash table + // or hcyan }; explicit_tau03_opt_search_heap(size_t) @@ -395,10 +465,16 @@ namespace spot ~explicit_tau03_opt_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()) { - // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; delete ptr; @@ -407,32 +483,55 @@ namespace spot color_ref get_color_ref(const state*& s) { - hash_type::iterator it = h.find(s); - if (it==h.end()) - return color_ref(0, 0); - if (s!=it->first) + hcyan_type::iterator ic = hc.find(s); + if (ic==hc.end()) + { + hash_type::iterator it = h.find(s); + if (it==h.end()) + // white state + return color_ref(0, 0); + if (s!=it->first) + { + delete s; + s = it->first; + } + // blue or red state + return color_ref(&(it->second.first), &(it->second.second)); + } + if (s!=ic->first) { delete s; - s = it->first; + s = ic->first; } - return color_ref(&(it->second.first), &(it->second.second)); + // cyan state + return color_ref(&h, &hc, ic->first, + &(ic->second.first), &(ic->second.second)); } void add_new_state(const state* s, color c) { - assert(h.find(s)==h.end()); + assert(hc.find(s)==hc.end() && h.find(s)==h.end()); + assert(c != CYAN); h.insert(std::make_pair(s, std::make_pair(c, bddfalse))); } + void add_new_state(const state* s, color c, const weight& w) + { + assert(hc.find(s)==hc.end() && h.find(s)==h.end()); + assert(c == CYAN); + hc.insert(std::make_pair(s, std::make_pair(w, bddfalse))); + } + void pop_notify(const state*) { } private: - typedef Sgi::hash_map, - state_ptr_hash, state_ptr_equal> hash_type; + // associate to each blue and red state its color and its acceptance set hash_type h; + // associate to each cyan state its weight and its acceptance set + hcyan_type hc; }; } // anonymous diff --git a/src/tgbaalgos/weight.cc b/src/tgbaalgos/weight.cc new file mode 100644 index 000000000..e4827550c --- /dev/null +++ b/src/tgbaalgos/weight.cc @@ -0,0 +1,125 @@ +// 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 +#include +#include "weight.hh" + +namespace spot +{ + weight::weight_vector* weight::pm = 0; + + weight::weight(const bdd& neg_all_cond) : neg_all_acc(neg_all_cond) + { + } + + void weight::inc_weight_handler(char* varset, int size) + { + bool ok = true; + for (int v = 0; v < size; ++v) + if (varset[v] > 0) + { + assert(ok); + ok=false; + weight::weight_vector::iterator it = pm->find(v); + if (it == pm->end()) + pm->insert(std::make_pair(v, 1)); + else + ++(it->second); + } + } + + weight& weight::operator+=(const bdd& acc) + { + pm = &m; + bdd_allsat(acc, inc_weight_handler); + return *this; + } + + void weight::dec_weight_handler(char* varset, int size) + { + bool ok = true; + for (int v = 0; v < size; ++v) + if (varset[v] > 0) + { + assert(ok); + ok=false; + weight::weight_vector::iterator it = pm->find(v); + assert(it != pm->end() && it->second > 0); + if (it->second > 1) + --(it->second); + else + pm->erase(it); + } + } + + weight& weight::operator-=(const bdd& acc) + { + pm = &m; + bdd_allsat(acc, dec_weight_handler); + return *this; + } + + bdd weight::operator-(const weight& w) const + { + weight_vector::const_iterator itw1 = m.begin(), itw2 = w.m.begin(); + bdd res = bddfalse; + + while (itw1 != m.end() && itw2 != w.m.end()) + { + assert(itw1->first <= itw2->first); + if (itw1->first < itw2->first) + { + res |= bdd_exist(neg_all_acc, bdd_ithvar(itw1->first)) & + bdd_ithvar(itw1->first); + ++itw1; + } + else + { + assert(itw1->second >= itw2->second); + if (itw1->second > itw2->second) + { + res |= bdd_exist(neg_all_acc, bdd_ithvar(itw1->first)) & + bdd_ithvar(itw1->first); + } + ++itw1; + ++itw2; + } + } + assert(itw2 == w.m.end()); + while (itw1 != m.end()) + { + res |= bdd_exist(neg_all_acc, bdd_ithvar(itw1->first)) & + bdd_ithvar(itw1->first); + ++itw1; + } + return res; + } + + std::ostream& operator<<(std::ostream& os, const weight& w) + { + weight::weight_vector::const_iterator it; + for (it = w.m.begin(); it != w.m.end(); ++it) + os << "(" << it->first << "," << it->second << ")"; + return os; + } + +}; diff --git a/src/tgbaalgos/weight.hh b/src/tgbaalgos/weight.hh new file mode 100644 index 000000000..4ec52f29e --- /dev/null +++ b/src/tgbaalgos/weight.hh @@ -0,0 +1,64 @@ +// 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_WEIGHT_HH +# define SPOT_TGBAALGOS_WEIGHT_HH + +#include +#include +#include + +namespace spot +{ + /// \brief Manage for a given automaton a vector of counter indexed by + /// its acceptance condition + + class weight + { + public: + /// Construct a empty vector (all counters set to zero). + /// + /// \param neg_all_cond : negation of all the acceptance conditions of + /// the automaton (the bdd returned by tgba::neg_acceptance_conditions()). + weight(const bdd& neg_all_cond); + /// Increment by one the counters of each acceptance condition in \a acc. + weight& operator+=(const bdd& acc); + /// Decrement by one the counters of each acceptance condition in \a acc. + weight& operator-=(const bdd& acc); + /// Return the set of each acceptance condition such that its counter is + /// strictly greatest than the corresponding counter in w. + /// + /// \pre For each acceptance condition, its counter is greatest or equal to + /// the corresponding counter in w. + bdd operator-(const weight& w) const; + friend std::ostream& operator<<(std::ostream& os, const weight& w); + + private: + typedef std::map weight_vector; + weight_vector m; + bdd neg_all_acc; + static weight_vector* pm; + static void inc_weight_handler(char* varset, int size); + static void dec_weight_handler(char* varset, int size); + }; +}; + +#endif // SPOT_TGBAALGOS_WEIGHT_HH diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 8efdc65a6..998271309 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -49,6 +49,7 @@ expect_ce() run 0 ./ltl2tgba -ese05_search -f "$1" run 0 ./ltl2tgba -ebsh_se05_search "$1" run 0 ./ltl2tgba -ebsh_se05_search -f "$1" + run 0 ./ltl2tgba -etau03_opt_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 @@ -72,6 +73,7 @@ expect_no() run 0 ./ltl2tgba -Ese05_search -f "$1" run 0 ./ltl2tgba -Ebsh_se05_search "$1" run 0 ./ltl2tgba -Ebsh_se05_search -f "$1" + run 0 ./ltl2tgba -Etau03_opt_search -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 944ec32d5..5cb535132 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -677,16 +677,7 @@ main(int argc, char** argv) } case Tau03OptSearch: - if (a->number_of_acceptance_conditions() == 0) - { - std::cout << "To apply tau03_opt_search, the automaton must " - << "have at least on accepting condition. " - << "Try with another algorithm." << std::endl; - } - else - { - ec = spot::explicit_tau03_opt_search(a); - } + ec = spot::explicit_tau03_opt_search(a); break; } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 60a2413d8..e278c9428 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -34,6 +34,7 @@ #include "misc/random.hh" #include "tgbaalgos/emptiness.hh" +#include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/se05.hh" @@ -98,6 +99,51 @@ to_float(const char* s) return res; } +struct ec_stat +{ + int min_states; + int max_states; + int tot_states; + int min_transitions; + int max_transitions; + int tot_transitions; + int min_max_depth; + int max_max_depth; + int tot_max_depth; + int n; + + ec_stat() + : n(0) + { + } + + void + count(const spot::ec_statistics* ec) + { + int s = ec->states(); + int t = ec->transitions(); + int m = ec->max_depth(); + if (n++) + { + min_states = std::min(min_states, s); + max_states = std::max(max_states, s); + tot_states += s; + min_transitions = std::min(min_transitions, t); + max_transitions = std::max(max_transitions, t); + tot_transitions += t; + min_max_depth = std::min(min_max_depth, m); + max_max_depth = std::max(max_max_depth, m); + tot_max_depth += m; + } + else + { + min_states = max_states = tot_states = s; + min_transitions = max_transitions = tot_transitions = t; + min_max_depth = max_max_depth = tot_max_depth = m; + } + } +}; + struct ce_stat { int min_prefix; @@ -161,8 +207,11 @@ main(int argc, char** argv) int exit_code = 0; - typedef std::map stats_type; - stats_type stats; + typedef std::map ec_stats_type; + ec_stats_type ec_stats; + + typedef std::map ce_stats_type; + ce_stats_type ce_stats; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; @@ -271,17 +320,6 @@ main(int argc, char** argv) ec_name.push_back("couvreur99_shy"); ec_safe.push_back(true); - if (opt_n_acc >= 1) - { - ec_obj.push_back(spot::explicit_tau03_search(a)); - ec_name.push_back("explicit_tau03_search"); - ec_safe.push_back(true); - - ec_obj.push_back(spot::explicit_tau03_opt_search(a)); - ec_name.push_back("explicit_tau03_opt_search"); - ec_safe.push_back(true); - } - if (opt_n_acc <= 1) { ec_obj.push_back(spot::explicit_magic_search(a)); @@ -301,6 +339,17 @@ main(int argc, char** argv) ec_safe.push_back(false); } + if (opt_n_acc >= 1) + { + ec_obj.push_back(spot::explicit_tau03_search(a)); + ec_name.push_back("explicit_tau03_search"); + ec_safe.push_back(true); + } + + ec_obj.push_back(spot::explicit_tau03_opt_search(a)); + ec_name.push_back("explicit_tau03_opt_search"); + ec_safe.push_back(true); + int n_ec = ec_obj.size(); int n_empty = 0; int n_non_empty = 0; @@ -312,6 +361,10 @@ main(int argc, char** argv) std::cout.width(32); std::cout << algo << ": "; spot::emptiness_check_result* res = ec_obj[i]->check(); + const spot::ec_statistics* ecs = + dynamic_cast(ec_obj[i]); + if (opt_z && ecs) + ec_stats[algo].count(ecs); if (res) { std::cout << "accepting run exists"; @@ -331,7 +384,7 @@ main(int argc, char** argv) { std::cout << ", computed OK"; if (opt_z) - stats[algo].count(run); + ce_stats[algo].count(run); } if (opt_z) std::cout << " [" << run->prefix.size() @@ -387,7 +440,61 @@ main(int argc, char** argv) } while (opt_ec); - if (!stats.empty()) + if (!ec_stats.empty()) + { + std::cout << "Statistics about emptiness checkers:" << std::endl; + std::cout << std::setw(32) << "" + << " | states | transitions |" + << std::endl << std::setw(32) << "algorithm" + << " | min < mean < max | min < mean < max | n " + << std::endl + << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl << std::setprecision(3); + for (ec_stats_type::const_iterator i = ec_stats.begin(); + i != ec_stats.end(); ++i) + std::cout << std::setw(32) << i->first << " |" + << std::setw(5) << i->second.min_states + << " " + << std::setw(6) + << static_cast(i->second.tot_states) / i->second.n + << " " + << std::setw(5) << i->second.max_states + << " |" + << std::setw(5) << i->second.min_transitions + << " " + << std::setw(6) + << static_cast(i->second.tot_transitions) / i->second.n + << " " + << std::setw(5) << i->second.max_transitions + << " |" + << std::setw(5) << i->second.n + << std::endl; + std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl + << std::setw(32) << "" + << " | maximal depth |" + << std::endl << std::setw(32) << "algorithm" + << " | min < mean < max | n " + << std::endl + << std::setw(59) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (ec_stats_type::const_iterator i = ec_stats.begin(); + i != ec_stats.end(); ++i) + std::cout << std::setw(32) << i->first << " |" + << std::setw(5) + << i->second.min_max_depth + << " " + << std::setw(6) + << static_cast(i->second.tot_max_depth) / i->second.n + << " " + << std::setw(5) + << i->second.max_max_depth + << " |" + << std::setw(5) << i->second.n + << std::endl; + } + + if (!ce_stats.empty()) { std::cout << "Statistics about counter-examples:" << std::endl; std::cout << std::setw(32) << "" @@ -397,7 +504,8 @@ main(int argc, char** argv) << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl << std::setprecision(3); - for (stats_type::const_iterator i = stats.begin(); i != stats.end(); ++i) + for (ce_stats_type::const_iterator i = ce_stats.begin(); + i != ce_stats.end(); ++i) std::cout << std::setw(32) << i->first << " |" << std::setw(5) << i->second.min_prefix << " " @@ -424,7 +532,8 @@ main(int argc, char** argv) << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; - for (stats_type::const_iterator i = stats.begin(); i != stats.end(); ++i) + for (ce_stats_type::const_iterator i = ce_stats.begin(); + i != ce_stats.end(); ++i) std::cout << std::setw(32) << i->first << " |" << std::setw(5) << i->second.min_run