diff --git a/ChangeLog b/ChangeLog index 54836a96b..dd53ae7da 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-12-13 Denis Poitrenaud + + * src/tgbaalgos/ndfs_result.hh: New file factorizing the computation of + accepting runs for ndfs emptiness check algoritms. + * src/tgbaalgos/Makefile.am: Add it. + * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Remove the old + result classes and use the new one. + 2004-12-10 Alexandre Duret-Lutz * src/tgbaalgos/gtec/status.hh diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 70ddafccf..dea69bf89 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -38,6 +38,7 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ + ndfs_result.hh \ neverclaim.hh \ powerset.hh \ projrun.hh \ diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 0390dd99f..6201b4571 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -35,6 +35,7 @@ #include "emptiness.hh" #include "emptiness_stats.hh" #include "magic.hh" +#include "ndfs_result.hh" namespace spot { @@ -95,17 +96,17 @@ namespace spot h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new result(*this); + return new ndfs_result, heap>(*this); } else { h.pop_notify(st_red.front().s); pop(st_red); if (!st_red.empty() && dfs_red()) - return new result(*this); + return new ndfs_result, heap>(*this); else if (dfs_blue()) - return new result(*this); + return new ndfs_result, heap>(*this); } return 0; } @@ -124,26 +125,22 @@ namespace spot return os; } + const heap& get_heap() const + { + return h; + } + + const stack_type& get_st_blue() const + { + return st_blue; + } + + const stack_type& get_st_red() const + { + return st_red; + } private: - struct stack_item - { - stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) - : s(n), it(i), label(l), acc(a) {}; - /// The visited state. - const state* s; - /// Design the next successor of \a s which has to be visited. - tgba_succ_iterator* it; - /// The label of the transition traversed to reach \a s - /// (false for the first one). - bdd label; - /// The acceptance set of the transition traversed to reach \a s - /// (false for the first one). - bdd acc; - }; - - typedef std::list stack_type; - void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { @@ -317,54 +314,6 @@ namespace spot return false; } - class result: public emptiness_check_result - { - public: - result(magic_search& ms) - : emptiness_check_result(ms.automaton()), ms_(ms) - { - } - virtual tgba_run* accepting_run() - { - assert(!ms_.st_blue.empty()); - assert(!ms_.st_red.empty()); - - tgba_run* run = new tgba_run; - - typename stack_type::const_reverse_iterator i, j, end; - tgba_run::steps* l; - - l = &run->prefix; - - i = ms_.st_blue.rbegin(); - end = ms_.st_blue.rend(); --end; - j = i; ++j; - for (; i != end; ++i, ++j) - { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - } - - l = &run->cycle; - - j = ms_.st_red.rbegin(); - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - - i = j; ++j; - end = ms_.st_red.rend(); --end; - for (; i != end; ++i, ++j) - { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - } - - return run; - } - private: - magic_search& ms_; - }; - }; class explicit_magic_search_heap @@ -432,6 +381,19 @@ namespace spot { } + bool has_been_visited(const state*& s) const + { + hash_type::const_iterator it = h.find(s); + if (it==h.end()) + return false; + if (s!=it->first) + { + delete s; + s = it->first; + } + return true; + } + private: typedef Sgi::hash_maphash(); + return color((h[ha%size] >> (ha%4)) & 3U) != WHITE; + } + private: size_t size; unsigned char* h; diff --git a/src/tgbaalgos/ndfs_result.hh b/src/tgbaalgos/ndfs_result.hh new file mode 100644 index 000000000..d286016bb --- /dev/null +++ b/src/tgbaalgos/ndfs_result.hh @@ -0,0 +1,338 @@ +// 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_NDFS_RESULT_HH +# define SPOT_TGBAALGOS_NDFS_RESULT_HH + +#include +#include +#include "tgba/tgba.hh" +#include "emptiness.hh" +#include "emptiness_stats.hh" +#include "bfssteps.hh" + +/// FIXME: +/// * Add the necessary calls to pop_notify. + +namespace spot +{ + struct stack_item + { + stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) + : s(n), it(i), label(l), acc(a) {}; + /// The visited state. + const state* s; + /// Design the next successor of \a s which has to be visited. + tgba_succ_iterator* it; + /// The label of the transition traversed to reach \a s + /// (false for the first one). + bdd label; + /// The acceptance set of the transition traversed to reach \a s + /// (false for the first one). + bdd acc; + }; + + typedef std::list stack_type; + + template < typename ndfs_search, typename heap > + class ndfs_result : public emptiness_check_result + { + public: + ndfs_result(const ndfs_search& ms) + : emptiness_check_result(ms.automaton()), ms_(ms), h_(ms_.get_heap()) + { + } + + virtual ~ndfs_result() + { + while (!st1.empty()) + { + delete st1.front().it; + st1.pop_front(); + } + } + + virtual tgba_run* accepting_run() + { + const stack_type& stb = ms_.get_st_blue(); + const stack_type& str = ms_.get_st_red(); + + assert(!stb.empty()); + + tgba_run* run = new tgba_run; + + const state* target = str.empty()?stb.front().s:str.front().s; + bdd covered_acc = bddfalse; + typename stack_type::const_reverse_iterator i, j; + + i = j = stb.rbegin(); ++j; + for (; i->s->compare(target) != 0; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + run->prefix.push_back(s); + } + + if (!str.empty()) + { + typename stack_type::const_reverse_iterator end = stb.rend(); + for (; j != end; ++i, ++j) + { + covered_acc |= j->acc; + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + run->cycle.push_back(s); + } + + j = str.rbegin(); + covered_acc |= j->acc; + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + run->cycle.push_back(s); + + i = j; ++j; + end = str.rend(); + for (; j != end; ++i, ++j) + { + covered_acc |= j->acc; + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + run->cycle.push_back(s); + } + } + + if (a_->all_acceptance_conditions() != covered_acc) + { + // try if any to minimize the first loop in run->cycle ?? + // what transitions have to be preserved (it depend on + // the detection (in the blue or red dfs) ?? + tgba_succ_iterator* i = a_->succ_iter(target); + i->first(); + st1.push_front(stack_item(target, i, bddfalse, bddfalse)); + bool b = dfs(target, run->cycle, covered_acc); + assert(b); + (void)b; + while (!st1.empty()) + { + delete st1.front().it; + st1.pop_front(); + } + } + + return run; + } + + private: + const ndfs_search& ms_; + const heap& h_; + stack_type st1; + + typedef Sgi::hash_set state_set; + + class shortest_path: public bfs_steps + { + public: + shortest_path(const tgba* a, const state* t, + const state_set& d, const heap& h) + : bfs_steps(a), target(t), dead(d), h(h) + { + } + + ~shortest_path() + { + } + + const state* + search(const state* start, tgba_run::steps& l) + { + const state* s = filter(start); + if (s) + return this->bfs_steps::search(s, l); + else + return 0; + } + + const state* + filter(const state* s) + { + if (!h.has_been_visited(s)) + { + delete s; + return 0; + } + if (dead.find(s) != dead.end()) + return 0; + seen.insert(s); + return s; + } + + const state_set& + get_seen() const + { + return seen; + } + + bool + match(tgba_run::step&, const state* dest) + { + return target->compare(dest) == 0; + } + + private: + state_set seen; + const state* target; + const state_set& dead; + const heap& h; + }; + + void complete_cycle(tgba_run::steps& cycle, bdd& covered_acc, + const tgba_run::step& start, tgba_run::steps& path, + const state_set& dead) + { + tgba_run::steps new_cycle; + + // find the minimal path between st1.back().s and st1.front().s + if (st1.back().s->compare(st1.front().s)!=0) + { + shortest_path s(a_, st1.front().s, dead, h_); + const state* res = s.search(st1.back().s, new_cycle); + assert(res && res->compare(st1.front().s) == 0); + (void)res; + for (tgba_run::steps::const_iterator it = new_cycle.begin(); + it != new_cycle.end(); ++it) + covered_acc |= it->acc; + } + + // traverse the accepting transition + covered_acc |= start.acc; + tgba_run::step s = { st1.front().s->clone(), start.label, start.acc }; + new_cycle.push_back(s); + + // follow the minimal path returning to st1.back().s + for (tgba_run::steps::const_iterator it = path.begin(); + it != path.end(); ++it) + covered_acc |= it->acc; + new_cycle.splice(new_cycle.end(), path); + + // concat this new loop to the existing ones + cycle.splice(cycle.end(), new_cycle); + } + + bool dfs(const state* target, tgba_run::steps& cycle, bdd& covered_acc) + { + state_set seen, dead; + + seen.insert(target); + while (!st1.empty()) + { + stack_item& f = st1.front(); + trace << "DFS1 treats: " << a_->format_state(f.s) << std::endl; + if (!f.it->done()) + { + const state *s_prime = f.it->current_state(); + trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + if (h_.has_been_visited(s_prime)) + { + if (dead.find(s_prime) != dead.end()) + { + trace << " it is dead, pop it" << std::endl; + } + else if (seen.find(s_prime) == seen.end()) + { + trace << " it is not seen, go down" << std::endl; + seen.insert(s_prime); + tgba_succ_iterator* i = a_->succ_iter(s_prime); + i->first(); + st1.push_front(stack_item(s_prime, i, label, acc)); + } + else if ((acc & covered_acc) != acc) + { + trace << " a propagation is needed, start a search" + << std::endl; + tgba_run::step s = {s_prime, label, acc}; + if (search(s, target, dead, cycle, covered_acc)) + return true; + } + else + { + trace << " already seen, pop it" << std::endl; + } + } + else + delete s_prime; + } + else + { + trace << " all the successors have been visited" + << std::endl; + stack_item f_dest(f); + delete st1.front().it; + st1.pop_front(); + if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) + { + trace << " a propagation is needed, start a search" + << std::endl; + tgba_run::step s = {f_dest.s, + f_dest.label, + f_dest.acc}; + if (search(s, target, dead, cycle, covered_acc)) + return true; + } + else + { + trace << " no propagation needed, pop it" << std::endl; + } + } + } + return false; + } + + bool search(const tgba_run::step& start, const state* target, + state_set& dead, tgba_run::steps& cycle, bdd& covered_acc) + { + tgba_run::steps path; + if (start.s->compare(target)==0) + { + trace << " complete the cycle" << std::endl; + complete_cycle(cycle, covered_acc, start, path, dead); + return covered_acc == a_->all_acceptance_conditions(); + } + + shortest_path s(a_, target, dead, h_); + const state* res = s.search(start.s, path); + if (res) + { + assert(res->compare(target) == 0); + trace << " complete the cycle" << std::endl; + complete_cycle(cycle, covered_acc, start, path, dead); + return covered_acc == a_->all_acceptance_conditions(); + } + state_set::const_iterator it; + for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it) + dead.insert(*it); + return false; + } + }; + +} + +#endif // SPOT_TGBAALGOS_NDFS_RESULT_HH diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 8624b66c0..d41d630f8 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -35,6 +35,7 @@ #include "emptiness.hh" #include "emptiness_stats.hh" #include "se05.hh" +#include "ndfs_result.hh" /// FIXME: make compiling depedent the taking into account of weights. @@ -98,17 +99,17 @@ namespace spot h.add_new_state(s0, CYAN); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new result(*this); + return new ndfs_result, heap>(*this); } else { h.pop_notify(st_red.front().s); pop(st_red); if (!st_red.empty() && dfs_red()) - return new result(*this); + return new ndfs_result, heap>(*this); else if (dfs_blue()) - return new result(*this); + return new ndfs_result, heap>(*this); } return 0; } @@ -127,26 +128,22 @@ namespace spot return os; } + const heap& get_heap() const + { + return h; + } + + const stack_type& get_st_blue() const + { + return st_blue; + } + + const stack_type& get_st_red() const + { + return st_red; + } private: - struct stack_item - { - stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) - : s(n), it(i), label(l), acc(a) {}; - /// The visited state. - const state* s; - /// Design the next successor of \a s which has to be visited. - tgba_succ_iterator* it; - /// The label of the transition traversed to reach \a s - /// (false for the first one). - bdd label; - /// The acceptance set of the transition traversed to reach \a s - /// (false for the first one). - bdd acc; - }; - - typedef std::list stack_type; - void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { @@ -325,60 +322,6 @@ namespace spot return false; } - class result: public emptiness_check_result - { - public: - result(se05_search& ms) - : emptiness_check_result(ms.automaton()), ms_(ms) - { - } - virtual tgba_run* accepting_run() - { - assert(!ms_.st_blue.empty()); - assert(!ms_.st_red.empty()); - - tgba_run* run = new tgba_run; - - typename stack_type::const_reverse_iterator i, j, end; - tgba_run::steps* l; - - const state* target = ms_.st_red.front().s; - - l = &run->prefix; - - i = ms_.st_blue.rbegin(); - end = ms_.st_blue.rend(); --end; - j = i; ++j; - for (; i != end; ++i, ++j) - { - if (l == &run->prefix && i->s->compare(target) == 0) - l = &run->cycle; - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - } - - if (l == &run->prefix && i->s->compare(target) == 0) - l = &run->cycle; - assert(l == &run->cycle); - - j = ms_.st_red.rbegin(); - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - - i = j; ++j; - end = ms_.st_red.rend(); --end; - for (; i != end; ++i, ++j) - { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - l->push_back(s); - } - - return run; - } - private: - se05_search& ms_; - }; - }; class explicit_se05_search_heap @@ -491,6 +434,29 @@ namespace spot { } + bool has_been_visited(const state*& s) const + { + hcyan_type::const_iterator ic = hc.find(s); + if (ic==hc.end()) + { + hash_type::const_iterator it = h.find(s); + if (it==h.end()) + return false; // white state + if (s!=it->first) + { + delete s; + s = it->first; + } + return true; // blue or red state + } + if (s!=*ic) + { + delete s; + s = *ic; + } + return true; // cyan state + } + private: hash_type h; // associate to each blue and red state its color @@ -580,6 +546,15 @@ namespace spot delete s; } + bool has_been_visited(const state*& s) const + { + hcyan_type::const_iterator ic = hc.find(s); + if (ic!=hc.end()) + return true; + size_t ha = s->hash(); + return color((h[ha%size] >> (ha%4)) & 3U) != WHITE; + } + private: size_t size; unsigned char* h; diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 0c39c363c..825be5d8c 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -20,7 +20,6 @@ // 02111-1307, USA. /// FIXME: Add -/// - the computation of a counter example if detected. /// - a bit-state hashing version. //#define TRACE @@ -39,6 +38,7 @@ #include "emptiness.hh" #include "emptiness_stats.hh" #include "tau03.hh" +#include "ndfs_result.hh" namespace spot { @@ -92,7 +92,7 @@ namespace spot h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new emptiness_check_result(a_); + return new ndfs_result, heap>(*this); return 0; } @@ -104,25 +104,22 @@ namespace spot return os; } + const heap& get_heap() const + { + return h; + } + + const stack_type& get_st_blue() const + { + return st_blue; + } + + const stack_type& get_st_red() const + { + return st_red; + } + private: - struct stack_item - { - stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) - : s(n), it(i), label(l), acc(a) {}; - /// The visited state. - const state* s; - /// Design the next successor of \a s which has to be visited. - tgba_succ_iterator* it; - /// The label of the transition traversed to reach \a s - /// (false for the first one). - bdd label; - /// The acceptance set of the transition traversed to reach \a s - /// (false for the first one). - bdd acc; - }; - - typedef std::list stack_type; - void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { @@ -358,6 +355,18 @@ namespace spot { } + bool has_been_visited(const state*& s) const + { + hash_type::const_iterator it = h.find(s); + if (it == h.end()) + return false; + else if (s != it->first) + { + delete s; + s = it->first; + } + return true; + } private: typedef Sgi::hash_map, diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 09338e20d..2ed477a4f 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -20,8 +20,6 @@ // 02111-1307, USA. /// FIXME: -/// * Add the necessary calls to pop_notify in the subclass result. -/// /// * Test 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 @@ -43,14 +41,13 @@ #endif #include -#include #include "misc/hash.hh" #include "tgba/tgba.hh" #include "emptiness.hh" #include "emptiness_stats.hh" #include "tau03opt.hh" #include "weight.hh" -#include "bfssteps.hh" +#include "ndfs_result.hh" namespace spot { @@ -104,7 +101,7 @@ namespace spot h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new result(*this); + return new ndfs_result, heap>(*this); return 0; } @@ -116,25 +113,22 @@ namespace spot return os; } + const heap& get_heap() const + { + return h; + } + + const stack_type& get_st_blue() const + { + return st_blue; + } + + const stack_type& get_st_red() const + { + return st_red; + } + private: - struct stack_item - { - stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a) - : s(n), it(i), label(l), acc(a) {}; - /// The visited state. - const state* s; - /// Design the next successor of \a s which has to be visited. - tgba_succ_iterator* it; - /// The label of the transition traversed to reach \a s - /// (false for the first one). - bdd label; - /// The acceptance set of the transition traversed to reach \a s - /// (false for the first one). - bdd acc; - }; - - typedef std::list stack_type; - void push(stack_type& st, const state* s, const bdd& label, const bdd& acc) { @@ -332,287 +326,6 @@ namespace spot return false; } - class result: public emptiness_check_result - { - private: - typedef Sgi::hash_set state_set; - - class shortest_path: public bfs_steps - { - public: - shortest_path(const tgba* a, const state* t, - const state_set& d, heap& h) - : bfs_steps(a), target(t), dead(d), h(h) - { - } - - ~shortest_path() - { - } - - const state* - search(const state* start, tgba_run::steps& l) - { - const state* s = filter(start); - if (s) - return this->bfs_steps::search(s, l); - else - return 0; - } - - const state* - filter(const state* s) - { - typename heap::color_ref c = h.get_color_ref(s); - if (c.is_white()) - { - delete s; - return 0; - } - else if (dead.find(s) != dead.end()) - return 0; - seen.insert(s); - return s; - } - - const state_set& - get_seen() const - { - return seen; - } - - bool - match(tgba_run::step&, const state* dest) - { - return target->compare(dest) == 0; - } - - private: - state_set seen; - const state* target; - const state_set& dead; - heap& h; - }; - - stack_type st1; - - tau03_opt_search& ms_; - - void complete_cycle(tgba_run::steps& cycle, bdd& covered_acc, - const tgba_run::step& start, tgba_run::steps& path, - const state_set& dead) - { - tgba_run::steps new_cycle; - - // find the minimal path between st1.back().s and st1.front().s - if (st1.back().s->compare(st1.front().s)!=0) - { - shortest_path s(ms_.a_, st1.front().s, dead, ms_.h); - const state* res = s.search(st1.back().s, new_cycle); - assert(res && res->compare(st1.front().s) == 0); - (void)res; - for (tgba_run::steps::const_iterator it = new_cycle.begin(); - it != new_cycle.end(); ++it) - covered_acc |= it->acc; - } - - // traverse the accepting transition - covered_acc |= start.acc; - tgba_run::step s = { st1.front().s->clone(), start.label, start.acc }; - new_cycle.push_back(s); - - // follow the minimal path returning to st1.back().s - for (tgba_run::steps::const_iterator it = path.begin(); - it != path.end(); ++it) - covered_acc |= it->acc; - new_cycle.splice(new_cycle.end(), path); - - // concat this new loop to the existing ones - cycle.splice(cycle.end(), new_cycle); - } - - bool dfs_result(const state* target, tgba_run::steps& cycle, - bdd& covered_acc) - { - state_set seen, dead; - - seen.insert(target); - while (!st1.empty()) - { - stack_item& f = st1.front(); - trace << "DFS1 treats: " << a_->format_state(f.s) << std::endl; - if (!f.it->done()) - { - const state *s_prime = f.it->current_state(); - trace << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; - bdd label = f.it->current_condition(); - bdd acc = f.it->current_acceptance_conditions(); - f.it->next(); - typename heap::color_ref c_prime = - ms_.h.get_color_ref(s_prime); - if (!c_prime.is_white()) - { - if (dead.find(s_prime) != dead.end()) - { - trace << " it is dead, pop it" << std::endl; - } - else if (seen.find(s_prime) == seen.end()) - { - trace << " it is not seen, go down" << std::endl; - seen.insert(s_prime); - tgba_succ_iterator* i = a_->succ_iter(s_prime); - i->first(); - st1.push_front(stack_item(s_prime, i, label, acc)); - } - else if ((acc & covered_acc) != acc) - { - trace << " a propagation is needed, start a search" - << std::endl; - tgba_run::step s = {s_prime, label, acc}; - if (search(s, target, dead, cycle, covered_acc)) - return true; - } - else - { - trace << " already seen, pop it" << std::endl; - } - } - else - delete s_prime; - } - else - { - trace << " all the successors have been visited" - << std::endl; - stack_item f_dest(f); - delete st1.front().it; - st1.pop_front(); - if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) - { - trace << " a propagation is needed, start a search" - << std::endl; - tgba_run::step s = {f_dest.s, - f_dest.label, - f_dest.acc}; - if (search(s, target, dead, cycle, covered_acc)) - return true; - } - else - { - trace << " no propagation needed, pop it" << std::endl; - } - } - } - return false; - } - - bool search(const tgba_run::step& start, const state* target, - state_set& dead, tgba_run::steps& cycle, bdd& covered_acc) - { - tgba_run::steps path; - if (start.s->compare(target)==0) - { - trace << " complete the cycle" << std::endl; - complete_cycle(cycle, covered_acc, start, path, dead); - return covered_acc == ms_.all_acc; - } - - shortest_path s(ms_.a_, target, dead, ms_.h); - const state* res = s.search(start.s, path); - if (res) - { - assert(res->compare(target) == 0); - trace << " complete the cycle" << std::endl; - complete_cycle(cycle, covered_acc, start, path, dead); - return covered_acc == ms_.all_acc; - } - state_set::const_iterator it; - for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it) - dead.insert(*it); - return false; - } - - public: - result(tau03_opt_search& ms) - : emptiness_check_result(ms.a_), - ms_(ms) - { - } - - virtual ~result() - { - while (!st1.empty()) - { - delete st1.front().it; - st1.pop_front(); - } - } - - virtual tgba_run* accepting_run() - { - assert(!ms_.st_blue.empty()); - assert(!ms_.st_red.empty()); - - tgba_run* run = new tgba_run; - - const state* target = ms_.st_red.front().s; - bdd covered_acc = bddfalse; - typename stack_type::const_reverse_iterator i, j, end; - - i = j = ms_.st_blue.rbegin(); ++j; - for (; i->s->compare(target) != 0; ++i, ++j) - { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - run->prefix.push_back(s); - } - - end = ms_.st_blue.rend(); - for (; j != end; ++i, ++j) - { - covered_acc |= j->acc; - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - run->cycle.push_back(s); - } - - j = ms_.st_red.rbegin(); - covered_acc |= j->acc; - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - run->cycle.push_back(s); - - i = j; ++j; - end = ms_.st_red.rend(); - for (; j != end; ++i, ++j) - { - covered_acc |= j->acc; - tgba_run::step s = { i->s->clone(), j->label, j->acc }; - run->cycle.push_back(s); - } - - if (ms_.all_acc != covered_acc) - { - // try to minimize the first loop in run->cycle ?? - // what transitions have to be preserved (it depend on - // the detection (in the blue or red dfs) ?? - tgba_succ_iterator* i = a_->succ_iter(target); - i->first(); - st1.push_front(stack_item(target, i, bddfalse, bddfalse)); - bool b = dfs_result(target, run->cycle, covered_acc); - assert(b); - (void)b; - while (!st1.empty()) - { - delete st1.front().it; - st1.pop_front(); - } - } - - return run; - } - - }; - }; class explicit_tau03_opt_search_heap @@ -757,6 +470,31 @@ namespace spot { } + bool has_been_visited(const state*& s) const + { + hcyan_type::const_iterator ic = hc.find(s); + if (ic == hc.end()) + { + hash_type::const_iterator it = h.find(s); + if (it == h.end()) + // white state + return false; + if (s != it->first) + { + delete s; + s = it->first; + } + // blue or red state + return true; + } + else if (s != ic->first) + { + delete s; + s = ic->first; + } + return true; + } + private: // associate to each blue and red state its color and its acceptance set