diff --git a/ChangeLog b/ChangeLog index 69b76ce04..cb436d299 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2004-10-13 Alexandre Duret-Lutz + The computation of the counter example fails the valgrind tests + and is wrong into two ways: the search stack is generally not a + path, and does not run until the end of the STL container. + Remove it. + * src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh + (tarjan_on_fly): Do not inherit from the emptiness_search class, + because the check method will no longer return a counter example. + (tarjan_on_fly::check): Return only a boolean. + (tarjan_on_fly::build_counter): Delete. + * src/tgbatest/ltl2tgba.cc: Adjust. + * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state, tgba_explicit_succ_iterator::current_condition, tgba_explicit_succ_iterator::current_accepting_conditions): Assert @@ -109,7 +120,7 @@ src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc, src/tgbaalgos/colordfs.hh, - src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check. + src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce @@ -117,7 +128,7 @@ * src/tgbatest/ltl2tgba.cc, src/tgbatest/emptchk.test, - src/tgbaalgos/Makefile.am: Add files for emptyness-check. + src/tgbaalgos/Makefile.am: Add files for emptiness-check. 2004-08-23 Thomas Martinez @@ -3174,7 +3185,7 @@ Switch from "promises" to "accepting sets". Fix the definitions of these accepting sets so that they are really useful. Provide - an all_accepting_conditions() method for use in the emptyness + an all_accepting_conditions() method for use in the emptiness check, and a neg_accepting_conditions() for products. Predeclare TGBA accepting conditions in the i/o. diff --git a/src/tgbaalgos/tarjan_on_fly.cc b/src/tgbaalgos/tarjan_on_fly.cc index a6271930f..5e0f82625 100644 --- a/src/tgbaalgos/tarjan_on_fly.cc +++ b/src/tgbaalgos/tarjan_on_fly.cc @@ -51,7 +51,7 @@ namespace spot } } - ce::counter_example* + bool tarjan_on_fly::check() { tgba_succ_iterator* iter = 0; @@ -96,12 +96,7 @@ namespace spot pop(); } - if (violation) - return build_counter(); - - //std::cout << "NO COUNTER EXAMPLE FOUND" << std::endl; - - return 0; + return violation; } void @@ -148,12 +143,6 @@ namespace spot void tarjan_on_fly::pop() { - /* - const state *s = stack[dftop].s; - hash_type::iterator hi = h.find(s); - hi->second = -1; - */ - int p = stack[dftop].pre; if (p >= 0) @@ -183,14 +172,6 @@ namespace spot { int n = 0; - /* - hash_type::const_iterator hi = h.find(s); - if (hi != h.end()) - n = hi->second; - else - n = -1; - */ - stack_type::const_iterator i; for (i = stack.begin(); i != stack.end(); ++i, ++n) if (s->compare(i->s) == 0) @@ -202,38 +183,10 @@ namespace spot return n; } - ce::counter_example* - tarjan_on_fly::build_counter() - { - ce = new ce::counter_example(a); - - stack_type::iterator i; - for (i = stack.begin(); i != stack.end(); ++i) - { - if (x && x->compare(i->s) == 0) - break; - - ce->prefix.push_back(ce::state_ce(i->s->clone(), - i->lasttr->current_condition())); - } - - for (; i != stack.end(); ++i) - { - ce->cycle.push_back(ce::state_ce(i->s->clone(), - i->lasttr->current_condition())); - } - - return ce; - } - std::ostream& tarjan_on_fly::print_stat(std::ostream& os) const { - int ce_size = 0; - if (ce) - ce_size = ce->size(); - os << "Size of Counter Example : " << ce_size << std::endl - << "States explored : " << h.size() << std::endl; + os << "States explored : " << h.size() << std::endl; return os; } diff --git a/src/tgbaalgos/tarjan_on_fly.hh b/src/tgbaalgos/tarjan_on_fly.hh index de8f284f1..8cef1642b 100644 --- a/src/tgbaalgos/tarjan_on_fly.hh +++ b/src/tgbaalgos/tarjan_on_fly.hh @@ -27,13 +27,11 @@ #include #include #include "tgba/tgbatba.hh" -//#include "tgba/bddprint.hh" -#include "tgbaalgos/minimalce.hh" namespace spot { - class tarjan_on_fly: public emptiness_search + class tarjan_on_fly { public: @@ -41,8 +39,8 @@ namespace spot tarjan_on_fly(const tgba_tba_proxy *a); virtual ~tarjan_on_fly(); - /// \brief Find a counter example. - virtual ce::counter_example* check(); + /// \brief Return true if there exits an accepting path. + bool check(); /// \brief Print Stat. std::ostream& print_stat(std::ostream& os) const; @@ -56,8 +54,6 @@ namespace spot int lowlink; int pre; int acc; - - //int pos; }; //typedef std::pair state_iter_pair; @@ -65,8 +61,6 @@ namespace spot state_ptr_hash, state_ptr_equal> hash_type; hash_type h; ///< Map of visited states. - - //typedef std::pair pair_type; typedef std::vector stack_type; stack_type stack; ///< Stack of visited states on the path. @@ -77,16 +71,11 @@ namespace spot bool violation; const state* x; - ce::counter_example* ce; void push(const state* s); void pop(); void lowlinkupdate(int f, int t); int in_stack(const state* s) const; - - ce::counter_example* build_counter(); - //clock_t tps_; - }; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a02d13394..10659e89b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -721,14 +721,6 @@ main(int argc, char** argv) spot::counter_example ce(ec->result()); ce.print_result(std::cout); ce.print_stats(std::cout); - - //spot::ce::counter_example* res2 = ce.get_counter_example(); - //spot::tgba* aut = res2->ce2tgba(); - //spot::dotty_reachable(std::cout, aut); - //res2->print(std::cout); - //delete res2; - //delete aut; - } else { @@ -744,15 +736,7 @@ main(int argc, char** argv) spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a); bool res = ec->check(); ec->print_stats(std::cout); - if (expect_counter_example) - { - if (!res) - exit_code = 1; - } - else - { - exit_code = res; - } + exit_code = expect_counter_example ? !res : res; delete ec; } break; @@ -786,9 +770,14 @@ main(int argc, char** argv) break; case TarjanOnFly: - std::cout << "Tarjan On Fly" << std::endl; - es = new spot::tarjan_on_fly(degeneralized); - break; + { + std::cout << "Tarjan On Fly" << std::endl; + spot::tarjan_on_fly* tof = new spot::tarjan_on_fly(degeneralized); + bool res = tof->check(); + exit_code = expect_counter_example ? !res : res; + delete tof; + break; + } case MinimalSearch: { @@ -804,7 +793,7 @@ main(int argc, char** argv) break; case MinimalSearchIterative: - std::cout << "Iterative Minimal Search" << std::endl; + std::cout << "Iterative Minimal Search" << std::endl; es = new spot::minimalce_search(degeneralized, true); break;