diff --git a/ChangeLog b/ChangeLog index a2e4a0751..b566126cb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2004-04-13 Alexandre Duret-Lutz + * src/tgbaalgo/semptinesscheck.hh (counter_example): New class, + extracted from ... + (emptiness_check): ... here. + * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, + iface/gspn/ltlgspn.cc: Adjust. + * wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx) ($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c. diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 345f19f79..3ff30e58e 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -175,24 +175,27 @@ main(int argc, char **argv) res = ec.check(); else res = ec.check2(); + const spot::emptiness_check_status* ecs = ec.result(); if (!res) { if (compute_counter_example) { - ec.counter_example(); - ec.print_result(std::cout, proj ? model : 0); + spot::counter_example ce(ecs); + ce.print_result(std::cout, proj ? model : 0); + ce.print_stats(std::cout); } else { std::cout << "non empty" << std::endl; + ecs->print_stats(std::cout); } } else { std::cout << "empty" << std::endl; + ecs->print_stats(std::cout); } std::cout << std::endl; - ec.print_stats(std::cout); if (!res) exit(1); } diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 443f39684..1bfdbcc67 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -96,6 +96,14 @@ namespace spot return i->first; } + void + emptiness_check_status::print_stats(std::ostream& os) const + { + os << h.size() << " unique states visited" << std::endl; + os << root.size() + << " strongly connected components in search stack" + << std::endl; + } ////////////////////////////////////////////////////////////////////// @@ -105,13 +113,6 @@ namespace spot - bool - emptiness_check::connected_component_set::has_state(const state* s) const - { - return states.find(s) != states.end(); - } - - emptiness_check::emptiness_check(const tgba* a) { ecs_ = new emptiness_check_status(a); @@ -473,68 +474,42 @@ namespace spot } } - - std::ostream& - emptiness_check::print_result(std::ostream& os, const tgba* restrict) const + const emptiness_check_status* + emptiness_check::result() const { - os << "Prefix:" << std::endl; - const bdd_dict* d = ecs_->aut->get_dict(); - for (state_sequence::const_iterator i_se = suffix.begin(); - i_se != suffix.end(); ++i_se) - { - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(*i_se, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(*i_se) << std::endl; - } - } - os << "Cycle:" <second) << std::endl; - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(it->first, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(it->first) << std::endl; - } - } - return os; + return ecs_; } - void - emptiness_check::counter_example() + ////////////////////////////////////////////////////////////////////// + + bool + counter_example::connected_component_set::has_state(const state* s) const + { + return states.find(s) != states.end(); + } + + ////////////////////////////////////////////////////////////////////// + + counter_example::counter_example(const emptiness_check_status* ecs) + : ecs_(ecs) { assert(!ecs_->root.empty()); assert(suffix.empty()); - int comp_size = ecs_->root.size(); + scc_stack::stack_type root = ecs_->root.s; + int comp_size = root.size(); // Transform the stack of connected component into an array. connected_component_set* scc = new connected_component_set[comp_size]; for (int j = comp_size - 1; 0 <= j; --j) { - scc[j].index = ecs_->root.top().index; - scc[j].condition = ecs_->root.top().condition; - ecs_->root.pop(); + scc[j].index = root.top().index; + scc[j].condition = root.top().condition; + root.pop(); } - assert(ecs_->root.empty()); + assert(root.empty()); // Build the set of states for all SCCs. - for (emptiness_check_status::hash_type::iterator i = ecs_->h.begin(); + for (emptiness_check_status::hash_type::const_iterator i = ecs_->h.begin(); i != ecs_->h.end(); ++i) { int index = i->second; @@ -635,7 +610,7 @@ namespace spot } void - emptiness_check::complete_cycle(const connected_component_set& scc, + counter_example::complete_cycle(const connected_component_set& scc, const state* from, const state* to) { @@ -727,7 +702,7 @@ namespace spot } void - emptiness_check::accepting_path(const connected_component_set& scc, + counter_example::accepting_path(const connected_component_set& scc, const state* start, bdd acc_to_traverse) { // State seen during the DFS. @@ -861,16 +836,55 @@ namespace spot complete_cycle(scc, start, suffix.back()); } + std::ostream& + counter_example::print_result(std::ostream& os, const tgba* restrict) const + { + os << "Prefix:" << std::endl; + const bdd_dict* d = ecs_->aut->get_dict(); + for (state_sequence::const_iterator i_se = suffix.begin(); + i_se != suffix.end(); ++i_se) + { + os << " "; + if (restrict) + { + const state* s = ecs_->aut->project_state(*i_se, restrict); + assert(s); + os << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << ecs_->aut->format_state(*i_se) << std::endl; + } + } + os << "Cycle:" <second) << std::endl; + os << " "; + if (restrict) + { + const state* s = ecs_->aut->project_state(it->first, restrict); + assert(s); + os << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << ecs_->aut->format_state(it->first) << std::endl; + } + } + return os; + } + void - emptiness_check::print_stats(std::ostream& os) const + counter_example::print_stats(std::ostream& os) const { - os << ecs_->h.size() << " unique states visited" << std::endl; + ecs_->print_stats(os); os << suffix.size() << " states in suffix" << std::endl; os << period.size() << " states in period" << std::endl; - os << ecs_->root.size() - << " strongly connected components in search stack" - << std::endl; } } diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index c1b2af8b4..03717f52d 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -53,7 +53,8 @@ namespace spot size_t size() const; bool empty() const; - std::stack s; + typedef std::stack stack_type; + stack_type s; }; class emptiness_check_status @@ -74,6 +75,9 @@ namespace spot typedef Sgi::hash_map hash_type; hash_type h; ///< Map of visited states. + + /// Output statistics about this object. + void print_stats(std::ostream& os) const; }; /// \brief Check whether the language of an automate is empty. @@ -98,9 +102,6 @@ namespace spot /// \endverbatim class emptiness_check { - typedef std::list state_sequence; - typedef std::pair state_proposition; - typedef std::list cycle_path; public: emptiness_check(const tgba* a); ~emptiness_check(); @@ -130,8 +131,31 @@ namespace spot bool check2(); //@} - /// Compute a counter example if tgba_emptiness_check() returned false. - void counter_example(); + const emptiness_check_status* result() const; + + private: + + emptiness_check_status* ecs_; + /// \brief Remove a strongly component from the hash. + /// + /// This function remove all accessible state from a given + /// state. In other words, it removes the strongly connected + /// component that contains this state. + void remove_component(const state* start_delete); + + }; + + + class counter_example + { + public: + counter_example(const emptiness_check_status* ecs); + + typedef std::pair state_proposition; + typedef std::list state_sequence; + typedef std::list cycle_path; + state_sequence suffix; + cycle_path period; /// \brief Display the example computed by counter_example(). /// @@ -142,8 +166,7 @@ namespace spot /// Output statistics about this object. void print_stats(std::ostream& os) const; - private: - + protected: struct connected_component_set: public scc_stack::connected_component { typedef Sgi::hash_set