From 15329c5618aafecfc31b0a0791718b1ea866ae98 Mon Sep 17 00:00:00 2001 From: Denis Poitrenaud Date: Thu, 25 Nov 2004 14:40:17 +0000 Subject: [PATCH] * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix comments and debug traces * src/tgbatest/randtgba.cc: Adjust names of algorithms. --- ChangeLog | 9 ++ src/tgbaalgos/magic.cc | 79 ++++++----------- src/tgbaalgos/magic.hh | 5 +- src/tgbaalgos/se05.cc | 160 +++++++++++----------------------- src/tgbaalgos/se05.hh | 27 ++---- src/tgbaalgos/tau03.cc | 101 +++++++--------------- src/tgbaalgos/tau03opt.cc | 177 ++++++++++++++++++++------------------ src/tgbaalgos/tau03opt.hh | 48 +++++++---- src/tgbatest/randtgba.cc | 10 +-- 9 files changed, 252 insertions(+), 364 deletions(-) diff --git a/ChangeLog b/ChangeLog index cc2002e8e..b77560050 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-11-25 Denis Poitrenaud + + * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, + src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, + src/tgbaalgos/tau03opt.cc: Fix comments and debug traces + + * src/tgbatest/randtgba.cc: Adjust names of algorithms. + 2004-11-25 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Add option -D. diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 2c06de500..0390dd99f 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -21,8 +21,11 @@ //#define TRACE -#ifdef TRACE #include +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr #endif #include @@ -178,17 +181,12 @@ 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 + trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -197,9 +195,7 @@ namespace spot typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { -# ifdef TRACE - std::cout << " It is white, go down" << std::endl; -# endif + trace << " It is white, go down" << std::endl; inc_states(); h.add_new_state(s_prime, BLUE); push(st_blue, s_prime, label, acc); @@ -212,10 +208,8 @@ namespace spot // 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 + trace << " It is blue and the arc is " + << "accepting, start a red dfs" << std::endl; target = f.s; c.set_color(RED); push(st_red, s_prime, label, acc); @@ -224,9 +218,7 @@ namespace spot } else { -# ifdef TRACE - std::cout << " It is blue or red, pop it" << std::endl; -# endif + trace << " It is blue or red, pop it" << std::endl; h.pop_notify(s_prime); } } @@ -235,10 +227,7 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -# ifdef TRACE - std::cout << " All the successors have been visited" - << std::endl; -# endif + trace << " All the successors have been visited" << std::endl; stack_item f_dest(f); pop(st_blue); typename heap::color_ref c = h.get_color_ref(f_dest.s); @@ -250,12 +239,10 @@ namespace spot // 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 + trace << " It is blue and the arc from " + << a_->format_state(st_blue.front().s) + << " to it is accepting, start a red dfs" + << std::endl; target = st_blue.front().s; c.set_color(RED); push(st_red, f_dest.s, f_dest.label, f_dest.acc); @@ -264,10 +251,7 @@ namespace spot } else { -# ifdef TRACE - std::cout << " Pop it" - << std::endl; -# endif + trace << " Pop it" << std::endl; h.pop_notify(f_dest.s); } } @@ -284,17 +268,12 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -# ifdef TRACE - std::cout << "DFS_RED treats: " - << a_->format_state(f.s) << std::endl; -# endif + trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -310,16 +289,12 @@ namespace spot // 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 + trace << " It is white, pop it" << std::endl; delete s_prime; } else if (c.get_color() == BLUE) { -# ifdef TRACE - std::cout << " It is blue, go down" << std::endl; -# endif + trace << " It is blue, go down" << std::endl; c.set_color(RED); push(st_red, s_prime, label, acc); if (target->compare(s_prime) == 0) @@ -327,18 +302,14 @@ namespace spot } else { -# ifdef TRACE - std::cout << " It is red, pop it" << std::endl; -# endif + trace << " It is red, pop it" << std::endl; h.pop_notify(s_prime); } } else // Backtrack { -# ifdef TRACE - std::cout << " All the successors have been visited, pop it" - << std::endl; -# endif + trace << " All the successors have been visited, pop it" + << std::endl; h.pop_notify(f.s); pop(st_red); } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 7b52ba907..ba801e390 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -55,8 +55,7 @@ namespace spot /// 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 + /// else if (the edge (s,t) is accepting) then /// target = s; /// call dfs_red(t); /// end if; @@ -70,7 +69,7 @@ namespace spot /// report cycle /// end if; /// for all t in post(s) do - /// if t.color != red then + /// if t.color == blue then /// call dfs_red(t); /// end if; /// end for; diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index a5d9fe464..8624b66c0 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -21,8 +21,11 @@ //#define TRACE -#ifdef TRACE #include +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr #endif #include @@ -53,7 +56,7 @@ namespace spot /// condition (i.e. it is a TBA). se05_search(const tgba *a, size_t size) : emptiness_check(a), - current_weight(0), + ec_statistics(), h(size), all_cond(a->all_acceptance_conditions()) { @@ -92,7 +95,7 @@ namespace spot assert(st_blue.empty()); const state* s0 = a_->get_init_state(); inc_states(); - h.add_new_state(s0, CYAN, current_weight); + h.add_new_state(s0, CYAN); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) return new result(*this); @@ -160,10 +163,6 @@ namespace spot 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; @@ -182,17 +181,12 @@ 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 + trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -201,25 +195,16 @@ namespace spot typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { -# ifdef TRACE - std::cout << " It is white, go down" << std::endl; -# endif - if (acc == all_cond) - ++current_weight; + trace << " It is white, go down" << std::endl; inc_states(); - h.add_new_state(s_prime, CYAN, current_weight); + h.add_new_state(s_prime, CYAN); push(st_blue, s_prime, label, acc); } 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! ----------^ + (f.s->compare(s_prime) != 0 && f.acc == all_cond))) { -# ifdef TRACE - std::cout << " It is cyan and acceptance condition " - << "is reached, report cycle" << std::endl; -# endif + trace << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; c.set_color(RED); push(st_red, s_prime, label, acc); return true; @@ -230,10 +215,8 @@ namespace spot // 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 + trace << " It is cyan or blue and the arc is " + << "accepting, start a red dfs" << std::endl; c.set_color(RED); push(st_red, s_prime, label, acc); if (dfs_red()) @@ -241,10 +224,7 @@ namespace spot } else { -# ifdef TRACE - std::cout << " It is cyan, blue or red, pop it" - << std::endl; -# endif + trace << " It is cyan, blue or red, pop it" << std::endl; h.pop_notify(s_prime); } } @@ -252,14 +232,9 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -# ifdef TRACE - std::cout << " All the successors have been visited" - << std::endl; -# endif + trace << " All the successors have been visited" << std::endl; stack_item f_dest(f); 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 (!st_blue.empty() && @@ -269,12 +244,10 @@ namespace spot // 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 + trace << " The arc from " + << a_->format_state(st_blue.front().s) + << " to the current state is accepting, start a " + << "red dfs" << std::endl; c.set_color(RED); push(st_red, f_dest.s, f_dest.label, f_dest.acc); if (dfs_red()) @@ -282,9 +255,7 @@ namespace spot } else { -# ifdef TRACE - std::cout << " Pop it" << std::endl; -# endif + trace << " Pop it" << std::endl; c.set_color(BLUE); h.pop_notify(f_dest.s); } @@ -300,17 +271,12 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -# ifdef TRACE - std::cout << "DFS_RED treats: " - << a_->format_state(f.s) << std::endl; -# endif + trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -325,45 +291,33 @@ namespace spot // 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 + trace << " It is white (due to collision), pop it" + << std::endl; delete s_prime; } else if (c.get_color() == RED) { -# ifdef TRACE - std::cout << " It is red, pop it" - << std::endl; -# endif + trace << " It is red, pop it" << std::endl; h.pop_notify(s_prime); } else if (c.get_color() == CYAN) { -# ifdef TRACE - std::cout << " It is cyan, report a cycle" - << std::endl; -# endif + trace << " It is cyan, report a cycle" << std::endl; 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 + trace << " It is blue, go down" << std::endl; 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 + trace << " All the successors have been visited, pop it" + << std::endl; h.pop_notify(f.s); pop(st_red); } @@ -429,7 +383,7 @@ namespace spot class explicit_se05_search_heap { - typedef Sgi::hash_map hcyan_type; typedef Sgi::hash_map hash_type; @@ -437,12 +391,12 @@ namespace spot 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(hash_type* h, hcyan_type* hc, const state* s) + : is_cyan(true), 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) + : is_cyan(false), ph(0), phc(0), ps(0), pc(c) { } color get_color() const @@ -451,11 +405,6 @@ namespace spot return CYAN; return *pc; } - int get_weight() const - { - assert(is_cyan); - return weight; - } void set_color(color c) { assert(!is_white()); @@ -478,7 +427,6 @@ namespace spot } 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 @@ -494,7 +442,7 @@ namespace spot hcyan_type::const_iterator sc = hc.begin(); while (sc != hc.end()) { - const state* ptr = sc->first; + const state* ptr = *sc; ++sc; delete ptr; } @@ -522,20 +470,19 @@ namespace spot } return color_ref(&(it->second)); // blue or red state } - if (s!=ic->first) + if (s!=*ic) { delete s; - s = ic->first; + s = *ic; } - return color_ref(&h, &hc, ic->first, ic->second); // cyan state + return color_ref(&h, &hc, *ic); // cyan state } - void add_new_state(const state* s, color c, int w=-1) + void add_new_state(const state* s, color c) { assert(hc.find(s)==hc.end() && h.find(s)==h.end()); - assert(c!=CYAN || w>=0); if (c == CYAN) - hc.insert(std::make_pair(s, w)); + hc.insert(s); else h.insert(std::make_pair(s, c)); } @@ -553,19 +500,19 @@ namespace spot class bsh_se05_search_heap { private: - typedef Sgi::hash_map hcyan_type; public: class color_ref { public: - color_ref(hcyan_type* h, const state* st, int w, + color_ref(hcyan_type* h, const state* st, unsigned char *base, unsigned char offset) - : is_cyan(true), weight(w), phc(h), ps(st), b(base), o(offset*2) + : is_cyan(true), phc(h), ps(st), b(base), o(offset*2) { } color_ref(unsigned char *base, unsigned char offset) - : is_cyan(false), weight(0), phc(0), ps(0), b(base), o(offset*2) + : is_cyan(false), phc(0), ps(0), b(base), o(offset*2) { } color get_color() const @@ -574,11 +521,6 @@ namespace spot return CYAN; return color(((*b) >> o) & 3U); } - int get_weight() const - { - assert(is_cyan); - return weight; - } void set_color(color c) { if (is_cyan && c!=CYAN) @@ -595,7 +537,6 @@ namespace spot } private: bool is_cyan; - int weight; hcyan_type* phc; const state* ps; unsigned char *b; @@ -618,16 +559,15 @@ namespace spot size_t ha = s->hash(); hcyan_type::iterator ic = hc.find(s); if (ic!=hc.end()) - return color_ref(&hc, ic->first, ic->second, &h[ha%size], ha%4); + return color_ref(&hc, *ic, &h[ha%size], ha%4); return color_ref(&h[ha%size], ha%4); } - void add_new_state(const state* s, color c, int w=-1) + void add_new_state(const state* s, color c) { - assert(c!=CYAN || w>=0); assert(get_color_ref(s).is_white()); if (c==CYAN) - hc.insert(std::make_pair(s, w)); + hc.insert(s); else { color_ref cr(get_color_ref(s)); diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index 9d07c2ce3..18e47524a 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -47,29 +47,21 @@ namespace spot /// \verbatim /// procedure check () /// 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 + /// (it exists a predecessor p of s in st_blue and s != t and + /// the arc between p and s is accepting)) then /// report cycle; - /// end if; - /// if the edge (s,t) is accepting then + /// else if the edge (s,t) is accepting then /// call dfs_red(t); /// end if; /// end for; @@ -83,15 +75,14 @@ namespace spot /// end if; /// s.color = red; /// for all t in post(s) do - /// if t.color != red then + /// if t.color == blue then /// call dfs_red(t); /// end if; /// end for; /// end; /// \endverbatim /// - /// It is an adaptation to TBA (and a slight extension) of the one - /// presented in + /// It is an adaptation to TBA of the one presented in /// \verbatim /// @techreport{SE04, /// author = {Stefan Schwoon and Javier Esparza}, @@ -106,12 +97,6 @@ namespace spot /// } /// \endverbatim /// - /// The extention consists in the introduction of a weight associated - /// to each state in the blue stack (the cyan states). The weight of a - /// cyan state corresponds to the number of accepting arcs traversed to reach - /// it from the initial state. Weights are used to detect accepting cycle in - /// the blue dfs. - /// /// \sa spot::explicit_magic_search /// emptiness_check* explicit_se05_search(const tgba *a); @@ -122,7 +107,7 @@ namespace spot /// it is a TBA). /// /// During the visit of \a a, the returned checker does not store explicitely - /// the traversed states but uses the bit-state hashing technicpresented in: + /// the traversed states but uses the bit-state hashing technic presented in: /// /// \verbatim /// @book{Holzmann91, diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 3998163a0..0c39c363c 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -25,9 +25,11 @@ //#define TRACE -#ifdef TRACE #include -#include "tgba/bddprint.hh" +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr #endif #include @@ -155,17 +157,12 @@ 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 + trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -174,18 +171,14 @@ namespace spot typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { -# ifdef TRACE - std::cout << " It is white, go down" << std::endl; -# endif + trace << " It is white, go down" << std::endl; inc_states(); h.add_new_state(s_prime, BLUE); push(st_blue, s_prime, label, acc); } else { -# ifdef TRACE - std::cout << " It is blue, pop it" << std::endl; -# endif + trace << " It is blue, pop it" << std::endl; h.pop_notify(s_prime); } } @@ -193,11 +186,9 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -# ifdef TRACE - std::cout << " All the successors have been visited" - << ", rescan this successors" - << std::endl; -# endif + trace << " All the successors have been visited" + << ", rescan this successors" + << std::endl; typename heap::color_ref c = h.get_color_ref(f.s); assert(!c.is_white()); tgba_succ_iterator* i = a_->succ_iter(f.s); @@ -205,11 +196,9 @@ namespace spot { 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 + trace << "DFS_BLUE rescanning the arc from " + << a_->format_state(f.s) << " to " + << a_->format_state(s_prime) << std::endl; bdd label = i->current_condition(); bdd acc = i->current_acceptance_conditions(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); @@ -217,19 +206,8 @@ namespace spot bdd acu = 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()); - 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 + trace << " a propagation is needed, go down" + << std::endl; c_prime.cumulate_acc(acu); push(st_red, s_prime, label, acc); dfs_red(acu); @@ -238,18 +216,14 @@ 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 + trace << "DFS_BLUE propagation is successful, report a" + << " cycle" << std::endl; return true; } else { -#ifdef TRACE - std::cout << "DFS_BLUE propagation is unsuccessful, pop it"; - << std::endl; -# endif + trace << "DFS_BLUE propagation is unsuccessful, pop it" + << std::endl; h.pop_notify(f.s); pop(st_blue); } @@ -265,17 +239,12 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -#ifdef TRACE - std::cout << "DFS_RED treats: " - << a_->format_state(f.s) << std::endl; -# endif + trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -#ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -284,35 +253,27 @@ namespace spot typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { -# ifdef TRACE - std::cout << " It is white, pop it" << std::endl; -# endif + trace << " It is white, pop it" << std::endl; 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 + trace << " It is blue and propagation " + << "is needed, go down" << std::endl; 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 + trace << " It is blue and no propagation " + << "is needed, pop it" << std::endl; h.pop_notify(s_prime); } } else // Backtrack { -# ifdef TRACE - std::cout << " All the successors have been visited, pop it" - << std::endl; -# endif + trace << " All the successors have been visited, pop it" + << std::endl; h.pop_notify(f.s); pop(st_red); } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 8de532401..545b13624 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -33,15 +33,14 @@ /// 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 -#ifdef TRACE #include -#include "tgba/bddprint.hh" +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr #endif #include @@ -105,7 +104,10 @@ namespace spot h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new emptiness_check_result(a_); + if (a_->number_of_acceptance_conditions() <=1) + return new result(*this); + else + return new emptiness_check_result(a_); return 0; } @@ -173,17 +175,12 @@ 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 + trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -192,9 +189,7 @@ namespace spot typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { -# ifdef TRACE - std::cout << " It is white, go down" << std::endl; -# endif + trace << " It is white, go down" << std::endl; current_weight += acc; inc_states(); h.add_new_state(s_prime, CYAN, current_weight); @@ -208,31 +203,20 @@ namespace spot ((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 + trace << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; c_prime.cumulate_acc(c.get_acc() | acc); push(st_red, s_prime, label, acc); return true; } else { -# ifdef TRACE - std::cout << " It is cyan or blue and"; -# endif + trace << " It is cyan or blue and"; 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 + trace << " a propagation is needed, " + << "start a red dfs" << std::endl; c_prime.cumulate_acc(acu); push(st_red, s_prime, label, acc); if (dfs_red(acu)) @@ -240,10 +224,8 @@ namespace spot } else { -# ifdef TRACE - std::cout << " no propagation is needed, pop it." - << std::endl; -# endif + trace << " no propagation is needed, pop it." + << std::endl; h.pop_notify(s_prime); } } @@ -253,10 +235,7 @@ namespace spot // Backtrack the edge // (predecessor of f.s in st_blue, , f.s) { -# ifdef TRACE - std::cout << " All the successors have been visited" - << std::endl; -# endif + trace << " All the successors have been visited" << std::endl; stack_item f_dest(f); pop(st_blue); current_weight -= f_dest.acc; @@ -271,14 +250,10 @@ namespace spot bdd acu = f_dest.acc | c.get_acc(); if ((c_prime.get_acc() & acu) != acu) { -# 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; -# endif + trace << " The arc from " + << a_->format_state(st_blue.front().s) + << " to the current state implies to " + << " start a red dfs" << std::endl; c_prime.cumulate_acc(acu); push(st_red, f_dest.s, f_dest.label, f_dest.acc); if (dfs_red(acu)) @@ -286,17 +261,13 @@ namespace spot } else { -# ifdef TRACE - std::cout << " Pop it" << std::endl; -# endif + trace << " Pop it" << std::endl; h.pop_notify(f_dest.s); } } else { -# ifdef TRACE - std::cout << " Pop it" << std::endl; -# endif + trace << " Pop it" << std::endl; h.pop_notify(f_dest.s); } } @@ -311,17 +282,12 @@ namespace spot while (!st_red.empty()) { stack_item& f = st_red.front(); -# ifdef TRACE - std::cout << "DFS_RED treats: " - << a_->format_state(f.s) << std::endl; -# endif + trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl; if (!f.it->done()) { const state *s_prime = f.it->current_state(); -# ifdef TRACE - std::cout << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; -# endif + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); // Go down the edge (f.s, , s_prime) @@ -330,48 +296,38 @@ namespace spot typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { -# ifdef TRACE - std::cout << " It is white, pop it" << std::endl; -# endif + trace << " It is white, pop it" << std::endl; 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 + trace << " It is cyan and acceptance condition " + << "is reached, report cycle" << std::endl; 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 + trace << " It is cyan or blue and propagation " + << "is needed, go down" + << std::endl; 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 + trace << " It is cyan or blue and no propagation " + << "is needed , pop it" << std::endl; h.pop_notify(s_prime); } } else // Backtrack { -# ifdef TRACE - std::cout << " All the successors have been visited, pop it" - << std::endl; -# endif + trace << " All the successors have been visited, pop it" + << std::endl; h.pop_notify(f.s); pop(st_red); } @@ -379,6 +335,61 @@ namespace spot return false; } + class result: public emptiness_check_result + { + public: + result(tau03_opt_search& ms) + : emptiness_check_result(ms.a_), + 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: + tau03_opt_search& ms_; + }; + }; class explicit_tau03_opt_search_heap diff --git a/src/tgbaalgos/tau03opt.hh b/src/tgbaalgos/tau03opt.hh index 798934c61..213772eb6 100644 --- a/src/tgbaalgos/tau03opt.hh +++ b/src/tgbaalgos/tau03opt.hh @@ -40,6 +40,7 @@ namespace spot /// \verbatim /// procedure check () /// begin + /// weight = 0; // the null vector /// call dfs_blue(s0); /// end; /// @@ -47,41 +48,52 @@ namespace spot /// begin /// s.color = cyan; /// s.acc = emptyset; + /// s.weight = weight; /// for all t in post(s) do /// let (s, l, a, t) be the edge from s to t; /// if t.color == white then + /// for all b in a do + /// weight[b] = weight[b] + 1; + /// end for; /// call dfs_blue(t); - /// else if t.color == cyan && s.acc U a U t.acc == all_acc then - /// report a cycle; - /// end if; - /// end for; - /// for all t in post(s) do - /// let (s, l, a, t) be the edge from s to t; - /// if s.acc U a not included in t.acc then - /// call dfs_red(t, a U s.acc); + /// for all b in a do + /// weight[b] = weight[b] - 1; + /// end for; + /// else + /// let (s, l, a, t) be the edge from s to t; + /// Acc = s.acc U a; + /// if t.color == cyan && + /// (Acc U support(weight -s.weight) U t.acc) == all_acc then + /// report a cycle; + /// else if Acc not included in t.acc then + /// call dfs_red(t, Acc); + /// end if; /// end if; /// end for; /// s.color = blue; /// end; /// - /// procedure dfs_red(s, A) + /// procedure dfs_red(s, Acc) /// begin - /// s.acc = s.acc U A; /// for all t in post(s) do /// let (s, l, a, t) be the edge from s to t; - /// if t.color != white then - /// if t.color == cyan && A U t.acc == all_acc then - /// report a cycle; - /// else if A not included in t.acc then - /// call dfs_red(t, A); - /// end if; + /// if t.color == cyan && + /// (Acc U support(weight -t.weight) U t.acc) == all_acc then + /// report a cycle; + /// else if t.color != white and Acc not included in t.acc then + /// call dfs_red(t, Acc); /// end if; /// end for; /// end; /// \endverbatim /// - /// This algorithm is an optimisation of the one implemented in - /// spot::explicit_tau03_search. + /// This algorithm is a generalisation to TGBA of the one implemented in + /// spot::explicit_se05_search. It is based on the acceptance set labelling + /// of states used in spot::explicit_tau03_search. Moreover, it introduce + /// a slight optimisation based on vectors of integers counting for each + /// acceptance condition how many time the condition has been visited in + /// the path stored in the blue stack. Such a vector is associated to each + /// state of this stack. /// emptiness_check* explicit_tau03_opt_search(const tgba *a); diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index cd8e219af..53bb88d50 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -340,11 +340,11 @@ main(int argc, char** argv) spot::tgba* d = opt_n_acc > 1 ? degen : a; ec_obj.push_back(spot::explicit_magic_search(d)); - ec_name.push_back("explicit_magic_search"); + ec_name.push_back("explicit_magic"); ec_safe.push_back(true); ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096)); - ec_name.push_back("bit_state_hashing_magic_search"); + ec_name.push_back("bit_state_hashing_magic"); ec_safe.push_back(false); ec_obj.push_back(spot::explicit_se05_search(d)); @@ -352,7 +352,7 @@ main(int argc, char** argv) ec_safe.push_back(true); ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096)); - ec_name.push_back("bit_state_hashing_se05_search"); + ec_name.push_back("bit_state_hashing_se05"); ec_safe.push_back(false); ec_obj.push_back(spot::explicit_gv04_check(d)); @@ -365,12 +365,12 @@ main(int argc, char** argv) spot::tgba* d = opt_n_acc == 0 ? degen : a; ec_obj.push_back(spot::explicit_tau03_search(d)); - ec_name.push_back("explicit_tau03_search"); + ec_name.push_back("explicit_tau03"); ec_safe.push_back(true); } ec_obj.push_back(spot::explicit_tau03_opt_search(a)); - ec_name.push_back("explicit_tau03_opt_search"); + ec_name.push_back("explicit_tau03_opt"); ec_safe.push_back(true); int n_ec = ec_obj.size();