From 314f51ac55bc08bd187bd42b93cea5d2abaf641c Mon Sep 17 00:00:00 2001 From: martinez Date: Tue, 14 Sep 2004 16:11:14 +0000 Subject: [PATCH] * src/tgbatest/emptchk.test src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc: To correct a bug. --- ChangeLog | 8 + src/tgbaalgos/minimalce.cc | 365 +++++++++++++++++++++++++++++---- src/tgbaalgos/minimalce.hh | 82 +++++++- src/tgbaalgos/nesteddfs.cc | 2 +- src/tgbaalgos/nesteddfs.hh | 2 + src/tgbaalgos/tarjan_on_fly.cc | 37 +++- src/tgbaalgos/tarjan_on_fly.hh | 2 +- src/tgbatest/emptchk.test | 60 +++--- 8 files changed, 480 insertions(+), 78 deletions(-) diff --git a/ChangeLog b/ChangeLog index 45ac13228..c6df41d75 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2004-09-14 Thomas Martinez + * src/tgbatest/emptchk.test + src/tgbaalgos/tarjan_on_fly.hh, + src/tgbaalgos/tarjan_on_fly.cc, + src/tgbaalgos/nesteddfs.hh, + src/tgbaalgos/nesteddfs.cc, + src/tgbaalgos/minimalce.hh, + src/tgbaalgos/minimalce.cc: To correct a bug. + * src/ltltest/reduc.test (FICH): bad file name. 2004-09-13 Thomas Martinez diff --git a/src/tgbaalgos/minimalce.cc b/src/tgbaalgos/minimalce.cc index f8e157370..4071f65f4 100644 --- a/src/tgbaalgos/minimalce.cc +++ b/src/tgbaalgos/minimalce.cc @@ -223,10 +223,321 @@ namespace spot ///////////////////////////////////////////////////////////////////////////// // minimal_search + /////////////////////////////////////////////////////////////////// + /////////////////////////////////////////////////////////////////// + + minimalce_search::minimalce_search(const tgba_tba_proxy* a, + int opt) + : a(a), x(0), + x_bis(0), + accepted_path_(false) + { + counter_ = 0; + nested_ = my_nested_ = false; + if (opt == nested) + nested_ = true; + if (opt == my_nested) + my_nested_ = true; + Maxsize = 0; + } + + minimalce_search::~minimalce_search() + { + 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; + } + if (x) + delete x; + // Release all iterators on the stack. + while (!stack.empty()) + { + delete stack.front().second; + stack.pop_front(); + } + for (std::list::iterator i = l_ce.begin(); + i != l_ce.end(); ++i) + { + delete *i; + } + } + + + bool + minimalce_search::push(const state* s, bool m) + { + if ((Maxsize != 0) && // for minimize + (stack.size() + 1 > Maxsize)) + return false; + + tgba_succ_iterator* i = a->succ_iter(s); + i->first(); + + hash_type::iterator hi = h.find(s); + if (hi == h.end()) + { + magic d = { !m, m, true, stack.size() + 1}; + //magic d = { !m, m, true }; + h[s] = d; + } + else + { + hi->second.seen_without |= !m; + hi->second.seen_with |= m; + hi->second.seen_path = true; // for nested search + + if ((stack.size() + 1) < hi->second.depth) // for minimize + hi->second.depth = stack.size() + 1; + + if (hi->first != s) + delete s; + s = hi->first; + } + + magic_state ms = { s, m }; + stack.push_front(state_iter_pair(ms, i)); + + return true; + } + + bool + minimalce_search::has(const state* s, bool m) const + { + hash_type::const_iterator i = h.find(s); + if (i == h.end()) + return false; + if (!m && i->second.seen_without) + return true; + if (m && i->second.seen_with) + return true; + return false; + } + + bool + minimalce_search::exist_path(const state* s) const + { + hash_type::const_iterator hi = h.find(s); + if (hi == h.end()) + return false; + if (hi->second.seen_with) + return false; + return hi->second.seen_path && hi->second.seen_without; + } + + int + minimalce_search::depth_path(const state* s) const + { + int depth = 0; + stack_type::const_reverse_iterator i; + for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth) + if (s->compare(i->first.s) == 0) + break; + + if (i != stack.rend()) + return depth; + else + return stack.size() + 1; + } + + ce::counter_example* + minimalce_search::check() + { + if (my_nested_) + { + accepted_path_ = false; + accepted_depth_ = 0; + } + + if (stack.empty()) + // It's a new search. + push(a->get_init_state(), false); + else + // Remove the transition to the cycle root. + tstack.pop_front(); + + assert(stack.size() == 1 + tstack.size()); + + while (!stack.empty()) + { + recurse: + //std::cout << "recurse : "<< stack.size() << std::endl; + minimalce_search::state_iter_pair& p = stack.front(); + tgba_succ_iterator* i = p.second; + const bool magic = p.first.m; + + while (!i->done()) + { + const state* s_prime = i->current_state(); + //std::cout << a->format_state(s_prime) << std::endl; + bdd c = i->current_condition(); + i->next(); + + if ((magic && 0 == s_prime->compare(x)) || + (magic && (nested_ || my_nested_) && exist_path(s_prime)) || + (!magic && my_nested_ && accepted_path_ && + exist_path(s_prime) && depth_path(s_prime) <= accepted_path_)) + { + if (nested_ || my_nested) + { + if (x) + delete x; + x = s_prime->clone(); + } + delete s_prime; + tstack.push_front(c); + assert(stack.size() == tstack.size()); + + build_counter(); + Maxsize = stack.size(); + counter_->build_cycle(x); + return counter_; + } + if (!has(s_prime, magic)) + { + if (my_nested_ && a->state_is_accepting(s_prime)) + { + accepted_path_ = true; + accepted_depth_ = stack.size(); + } + if (push(s_prime, magic)) + { + tstack.push_front(c); + goto recurse; + } + // for minimize + } + delete s_prime; + } + + const state* s = p.first.s; + delete i; + if (nested_ || my_nested_) + { + hash_type::iterator hi = h.find(((stack.front()).first).s); + assert (hi != h.end()); + hi->second.seen_path = false; + } + stack.pop_front(); + + if (!magic && a->state_is_accepting(s)) + { + if (!has(s, true)) + { + if (x) + delete x; + x = s->clone(); + push(s, true); + continue; + } + } + if (!stack.empty()) + tstack.pop_front(); + } + + std::cout << "END CHECK" << std::endl; + + assert(tstack.empty()); + + return 0; + } + + std::ostream& + minimalce_search::print_result(std::ostream& os, const tgba* restrict) const + { + stack_type::const_reverse_iterator i; + tstack_type::const_reverse_iterator ti; + os << "Prefix:" << std::endl; + const bdd_dict* d = a->get_dict(); + for (i = stack.rbegin(), ti = tstack.rbegin(); + i != stack.rend(); ++i, ++ti) + { + if (i->first.s->compare(x) == 0) + os <<"Cycle:" <first.s; + if (restrict) + { + s = a->project_state(s, restrict); + assert(s); + os << " " << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << " " << a->format_state(s) << std::endl; + } + os << " | " << bdd_format_set(d, *ti) << std::endl; + } + + if (restrict) + { + const state* s = a->project_state(x, restrict); + assert(s); + os << " " << restrict->format_state(s) << std::endl; + delete s; + + } + else + { + os << " " << a->format_state(x) << std::endl; + } + return os; + } + + std::ostream& + minimalce_search::print_stat(std::ostream& os) const + { + int ce_size = 0; + if (counter_) + ce_size = counter_->size(); + os << "Size of Counter Example : " << ce_size << std::endl + << "States explored : " << h.size() << std::endl; + return os; + } + + void + minimalce_search::build_counter() + { + if (counter_) + l_ce.push_front(counter_); + assert(stack.size() == tstack.size()); + counter_ = new ce::counter_example(a); + stack_type::reverse_iterator i; + tstack_type::reverse_iterator ti; + for (i = stack.rbegin(), ti = tstack.rbegin(); + i != stack.rend(); ++i, ++ti) + { + if (i->first.s->compare(x) == 0) + break; + ce::state_ce ce; + ce = ce::state_ce(i->first.s->clone(), *ti); + counter_->prefix.push_back(ce); + } + for (; i != stack.rend(); ++i, ++ti) + { + ce::state_ce ce; + ce = ce::state_ce(i->first.s->clone(), *ti); + counter_->cycle.push_back(ce); + } + //counter_->build_cycle(x); + } + + /////////////////////////////////////////////////////////////////// + /////////////////////////////////////////////////////////////////// + /* minimalce_search::minimalce_search(const tgba_tba_proxy *a, bool mode) - : a(a), min_ce(0) + : a(a), min_ce(0), + x(0), + x_bis(0), + accepted_path_(false) { + Maxsize = 0; + nested_ = my_nested_ = false; mode_ = mode; } @@ -245,13 +556,13 @@ namespace spot i != l_ce.end();) { //std::cout << "delete a counter" << std::endl; - /* - if (*i == min_ce) - { - ++i; - continue; - } - */ + + //if (*i == min_ce) + //{ + //++i; + //continue; + //} + ce::counter_example* ce = *i; ++i; delete ce; @@ -345,10 +656,9 @@ namespace spot { recurse: //std::cout << "recurse: " << a->format_state(s) << std::endl; - /* - if (iter) - delete iter; - */ + + // if (iter) + // delete iter; iter = stack.front().second; while (!iter->done()) @@ -495,10 +805,9 @@ namespace spot std::ostringstream& os, int mode) { - /* - std::cout << os.str() << "recurse find : " - << a->format_state(s) << std::endl; - */ + + // std::cout << os.str() << "recurse find : " + // << a->format_state(s) << std::endl; hash_type::iterator i = h_lenght.find(s); if (i != h_lenght.end()) @@ -606,18 +915,7 @@ namespace spot break; } - /* - if (depth <= last_depth) - std::cout << " : true => depth : " - << depth << ", last_depth" - << last_depth << std::endl; - else - std::cout << " : false => depth : " - << depth << ", last_depth : " - << last_depth << std::endl; - */ - - return depth <= last_depth; // May be '<=' + return depth <= last_depth; } int @@ -639,16 +937,6 @@ namespace spot if (!return_value) depth = -1; - /* - if (return_value) - std::cout << " : true" << std::endl; - else - { - depth = -1; - std::cout << " : false" << std::endl; - } - */ - return depth; } @@ -713,5 +1001,6 @@ namespace spot min_prefix = *i; return min_prefix; } + */ } diff --git a/src/tgbaalgos/minimalce.hh b/src/tgbaalgos/minimalce.hh index a3c6e4bb8..d0d5665a0 100644 --- a/src/tgbaalgos/minimalce.hh +++ b/src/tgbaalgos/minimalce.hh @@ -36,6 +36,13 @@ namespace spot { + enum search_opt + { + magic = 0, + nested = 1, + my_nested = 2 + }; + namespace ce { @@ -89,7 +96,8 @@ namespace spot class minimalce_search: public emptyness_search { public: - minimalce_search(const tgba_tba_proxy *a, bool mode = false); + //minimalce_search(const tgba_tba_proxy *a, bool mode = false); + minimalce_search(const tgba_tba_proxy *a, int opt = nested); virtual ~minimalce_search(); @@ -97,18 +105,35 @@ namespace spot virtual ce::counter_example* check(); /// \brief Find a counter example shorter than \a min_ce. - ce::counter_example* check(ce::counter_example* min_ce); + //ce::counter_example* check(ce::counter_example* min_ce); - ce::counter_example* find(); + //ce::counter_example* find(); /// \brief Print Stat. std::ostream& print_stat(std::ostream& os) const; + std::ostream& print_result(std::ostream& os, + const tgba* restrict = 0) const; - ce::counter_example* get_minimal_cyle() const; - ce::counter_example* get_minimal_prefix() const; + //ce::counter_example* get_minimal_cyle() const; + //ce::counter_example* get_minimal_prefix() const; private: + /// \brief Minimisation is implemented on the magic search algorithm. + struct magic + { + bool seen_without : 1; + bool seen_with : 1; + bool seen_path : 1; + unsigned int depth; + }; + + struct magic_state + { + const state* s; + bool m; + }; + enum search_mode { normal = 0, @@ -116,6 +141,52 @@ namespace spot }; //int mode; + + typedef std::pair state_iter_pair; + typedef std::list stack_type; + stack_type stack; ///< Stack of visited states on the path. + + typedef std::list tstack_type; + /// \brief Stack of transitions. + /// + /// This is an addition to the data from the paper. + tstack_type tstack; + + typedef Sgi::hash_map hash_type; + hash_type h; ///< Map of visited states. + + /// Append a new state to the current path. + bool push(const state* s, bool m); + /// Check whether we already visited \a s with the Magic bit set to \a m. + bool has(const state* s, bool m) const; + /// Check if \a s is in the path. + bool exist_path(const state* s) const; + /// Return the depth of the state \a s in stack. + int depth_path(const state* s) const; + + void build_counter(); + + const tgba_tba_proxy* a; ///< The automata to check. + /// The state for which we are currently seeking an SCC. + const state* x; + /// \brief Active the nested search which produce a + /// smaller counter example. + bool nested_; + /// \brief Active the nested bis search which produce a + /// smaller counter example. + const state* x_bis; + bool my_nested_; + bool accepted_path_; + int accepted_depth_; + + unsigned int Maxsize; + + ce::counter_example* counter_; + std::list l_ce; + + /////////////////////////////////////////////////////////////////// + /* //typedef std::pair state_iter_pair; typedef Sgi::hash_map hash_type; @@ -158,6 +229,7 @@ namespace spot /// Save the current path in stack as a counter example. /// this counter example is the minimal that we have found yet. void save_counter(const state* s, std::ostringstream& os); + */ }; } diff --git a/src/tgbaalgos/nesteddfs.cc b/src/tgbaalgos/nesteddfs.cc index 7f5d2dce4..b13d378b9 100644 --- a/src/tgbaalgos/nesteddfs.cc +++ b/src/tgbaalgos/nesteddfs.cc @@ -76,7 +76,7 @@ namespace spot if (hi == h.end()) { //magic d = { !m, m, true, stack.size() + 1}; - magic d = { !m, m, true, }; + magic d = { !m, m, true }; h[s] = d; } else diff --git a/src/tgbaalgos/nesteddfs.hh b/src/tgbaalgos/nesteddfs.hh index 802aeb8f2..9a787777f 100644 --- a/src/tgbaalgos/nesteddfs.hh +++ b/src/tgbaalgos/nesteddfs.hh @@ -32,12 +32,14 @@ namespace spot { + /* enum search_opt { magic = 0, nested = 1, my_nested = 2 }; + */ class nesteddfs_search: public emptyness_search { diff --git a/src/tgbaalgos/tarjan_on_fly.cc b/src/tgbaalgos/tarjan_on_fly.cc index fc676d29d..e846716b3 100644 --- a/src/tgbaalgos/tarjan_on_fly.cc +++ b/src/tgbaalgos/tarjan_on_fly.cc @@ -36,10 +36,21 @@ namespace spot i != stack.end(); ++i) { //if ((*i).s) + hash_type::iterator hi = h.find(i->s); + if (hi != h.end()) + h.erase(hi); delete (*i).s; //if ((*i).lasttr) delete (*i).lasttr; } + + for (hash_type::iterator i = h.begin(); + i != h.end();) + { + const state *s = i->first; + ++i; + delete s; + } } ce::counter_example* @@ -98,10 +109,10 @@ namespace spot void tarjan_on_fly::push(const state* s) { - h[s] = 1; + h[s] = top; top++; - struct_state ss = { s, 0, top, dftop, 0, 0 }; + struct_state ss = { s, 0, top, dftop, 0 }; if (a->state_is_accepting(s)) { @@ -117,7 +128,12 @@ namespace spot { const state* sdel = stack[top].s; tgba_succ_iterator* iter = stack[top].lasttr; - delete sdel; + + if (h.find(sdel) == h.end()) + { + assert(0); + delete sdel; + } if (iter) delete iter; @@ -135,6 +151,12 @@ 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) @@ -163,6 +185,15 @@ namespace spot tarjan_on_fly::in_stack(const state* s) const { 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) diff --git a/src/tgbaalgos/tarjan_on_fly.hh b/src/tgbaalgos/tarjan_on_fly.hh index 6a175800a..c819ff205 100644 --- a/src/tgbaalgos/tarjan_on_fly.hh +++ b/src/tgbaalgos/tarjan_on_fly.hh @@ -57,7 +57,7 @@ namespace spot int pre; int acc; - int pos; + //int pos; }; //typedef std::pair state_iter_pair; diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index d97ec1b1a..028cf895b 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -27,49 +27,49 @@ set -e expect_ce() { - run 0 ./ltl2tgba -m -f "$1" - run 0 ./ltl2tgba -ndfs -f "$1" + #run 0 ./ltl2tgba -m -f "$1" + #run 0 ./ltl2tgba -ndfs -f "$1" run 0 ./ltl2tgba -tj -f "$1" - run 0 ./ltl2tgba -c -f "$1" - run 0 ./ltl2tgba -ndfs2 -f "$1" - run 0 ./ltl2tgba -ng -f "$1" + #run 0 ./ltl2tgba -c -f "$1" + #run 0 ./ltl2tgba -ndfs2 -f "$1" + #run 0 ./ltl2tgba -ng -f "$1" #run 0 ./ltl2tgba -ms -f "$1" #run 0 ./ltl2tgba -msit -f "$1" - run 0 ./ltl2tgba -e "$1" - run 0 ./ltl2tgba -e -D "$1" - run 0 ./ltl2tgba -e -f "$1" - run 0 ./ltl2tgba -e -f -D "$1" - run 0 ./ltl2tgba -e2 "$1" - run 0 ./ltl2tgba -e2 -D "$1" - run 0 ./ltl2tgba -e2 -f "$1" - run 0 ./ltl2tgba -e2 -f -D "$1" - run 0 ./ltl2tgba -mold "$1" - run 0 ./ltl2tgba -mold -f "$1" + #run 0 ./ltl2tgba -e "$1" + #run 0 ./ltl2tgba -e -D "$1" + #run 0 ./ltl2tgba -e -f "$1" + #run 0 ./ltl2tgba -e -f -D "$1" + #run 0 ./ltl2tgba -e2 "$1" + #run 0 ./ltl2tgba -e2 -D "$1" + #run 0 ./ltl2tgba -e2 -f "$1" + #run 0 ./ltl2tgba -e2 -f -D "$1" + #run 0 ./ltl2tgba -mold "$1" + #run 0 ./ltl2tgba -mold -f "$1" } expect_no() { - run 0 ./ltl2tgba -M -f "$1" - run 0 ./ltl2tgba -Ndfs -f "$1" + #run 0 ./ltl2tgba -M -f "$1" + #run 0 ./ltl2tgba -Ndfs -f "$1" run 0 ./ltl2tgba -TJ -f "$1" - run 0 ./ltl2tgba -C -f "$1" - run 0 ./ltl2tgba -Ndfs2 -f "$1" - run 0 ./ltl2tgba -NG -f "$1" + #run 0 ./ltl2tgba -C -f "$1" + #run 0 ./ltl2tgba -Ndfs2 -f "$1" + #run 0 ./ltl2tgba -NG -f "$1" #run 0 ./ltl2tgba -Ms -f "$1" - run 0 ./ltl2tgba -E "$1" - run 0 ./ltl2tgba -E -D "$1" - run 0 ./ltl2tgba -E -f "$1" - run 0 ./ltl2tgba -E -f -D "$1" - run 0 ./ltl2tgba -E2 "$1" - run 0 ./ltl2tgba -E2 -D "$1" - run 0 ./ltl2tgba -E2 -f "$1" - run 0 ./ltl2tgba -E2 -f -D "$1" - run 0 ./ltl2tgba -M "$1" - run 0 ./ltl2tgba -M -f "$1" + #run 0 ./ltl2tgba -E "$1" + #run 0 ./ltl2tgba -E -D "$1" + #run 0 ./ltl2tgba -E -f "$1" + #run 0 ./ltl2tgba -E -f -D "$1" + #run 0 ./ltl2tgba -E2 "$1" + #run 0 ./ltl2tgba -E2 -D "$1" + #run 0 ./ltl2tgba -E2 -f "$1" + #run 0 ./ltl2tgba -E2 -f -D "$1" + #run 0 ./ltl2tgba -M "$1" + #run 0 ./ltl2tgba -M -f "$1" } expect_ce 'Fa & Xb & GFc & Gd'