diff --git a/ChangeLog b/ChangeLog index fb1b0725b..d6744a391 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2004-04-13 Alexandre Duret-Lutz + * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move + into ... + (emptiness_check_shy): This new subclass of emptiness_check. + * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, + iface/gspn/ltlgspn.cc: Adjust. + * src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig. * src/tgbaalgo/semptinesscheck.hh (counter_example): New class, diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 3ff30e58e..d55e6f7b4 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -169,13 +169,16 @@ main(int argc, char **argv) case Couvreur: case Couvreur2: { - spot::emptiness_check ec(prod); - bool res; + spot::emptiness_check* ec; + if (check == Couvreur) - res = ec.check(); + ec = new spot::emptiness_check(prod); else - res = ec.check2(); - const spot::emptiness_check_status* ecs = ec.result(); + ec = new spot::emptiness_check_shy(prod); + + bool res = ec->check(); + + const spot::emptiness_check_status* ecs = ec->result(); if (!res) { if (compute_counter_example) @@ -196,6 +199,7 @@ main(int argc, char **argv) ecs->print_stats(std::cout); } std::cout << std::endl; + delete ec; if (!res) exit(1); } diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 1bfdbcc67..e3b925a29 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -111,8 +111,6 @@ namespace spot typedef std::pair pair_state_iter; - - emptiness_check::emptiness_check(const tgba* a) { ecs_ = new emptiness_check_status(a); @@ -309,6 +307,23 @@ namespace spot return true; } + const emptiness_check_status* + emptiness_check::result() const + { + return ecs_; + } + + ////////////////////////////////////////////////////////////////////// + + emptiness_check_shy::emptiness_check_shy(const tgba* a) + : emptiness_check(a) + { + } + + emptiness_check_shy::~emptiness_check_shy() + { + } + struct successor { bdd acc; const spot::state* s; @@ -316,7 +331,7 @@ namespace spot }; bool - emptiness_check::check2() + emptiness_check_shy::check() { // We use five main data in this algorithm: // * emptiness_check::root, a stack of strongly connected components (SCC), @@ -474,12 +489,6 @@ namespace spot } } - const emptiness_check_status* - emptiness_check::result() const - { - return ecs_; - } - ////////////////////////////////////////////////////////////////////// bool diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 03717f52d..e45b8d620 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -80,6 +80,7 @@ namespace spot void print_stats(std::ostream& os) const; }; + //@{ /// \brief Check whether the language of an automate is empty. /// /// This is based on the following paper. @@ -100,41 +101,39 @@ namespace spot /// isbn = {3-540-66587-0} /// } /// \endverbatim + /// + /// check() returns true if the automaton's language is empty. When + /// it return false, a stack of SCC has been built and can + /// later be used by counter_example(). + /// + /// There are two variants of this algorithm: emptiness_check() and + /// emptiness_check_shy(). They differ in their memory usage, the + /// number for successors computed before they are used and the way + /// the depth first search is directed. + /// + /// emptiness_check() performs a straightforward depth first search. + /// The DFS stacks store tgba_succ_iterators, so that only the + /// iterators which really are explored are computed. + /// + /// emptiness_check_shy() try to explore successors which are + /// visited states first. this helps to merge SCCs and generally + /// helps to produce shorter counter-examples. However this + /// algorithm cannot stores unprocessed successors as + /// tgba_succ_iterators: it must compute all successors of a state + /// at once in order to decide which to explore first, and must keep + /// a list of all unexplored successors in its DFS stack. class emptiness_check { public: emptiness_check(const tgba* a); - ~emptiness_check(); + virtual ~emptiness_check(); - //@{ - /// \brief check whether an automaton's language is empty - /// - /// Returns true if the automaton's language is empty. When - /// it return false, a stack of SCC has been built and can - /// later be used by counter_example(). - /// - /// There are two variants of this algorithm: check() and check2(). - /// They differ in their memory usage, the number for successors computed - /// before they are used and the way the depth first search is directed. - /// - /// check() performs a straightforward depth first search. The DFS - /// stacks store tgba_succ_iterators, so that only the iterators which - /// really are explored are computed. - /// - /// check2() try to explore successors which are visited states first. - /// this helps to merge SCCs and generally helps to produce shorter - /// counter-examples. However this algorithm cannot stores unprocessed - /// successors as tgba_succ_iterators: it must compute all successors - /// of a state at once in order to decide which to explore first, and - /// must keep a list of all unexplored successors in its DFS stack. - bool check(); - bool check2(); - //@} + /// check whether the automaton's language is empty + virtual bool check(); const emptiness_check_status* result() const; - private: - + protected: emptiness_check_status* ecs_; /// \brief Remove a strongly component from the hash. /// @@ -142,9 +141,18 @@ namespace spot /// state. In other words, it removes the strongly connected /// component that contains this state. void remove_component(const state* start_delete); - }; + class emptiness_check_shy : public emptiness_check + { + public: + emptiness_check_shy(const tgba* a); + virtual ~emptiness_check_shy(); + + virtual bool check(); + }; + //@} + class counter_example { diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 4002823c9..f3eab4d64 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -364,28 +364,30 @@ main(int argc, char** argv) case Couvreur: case Couvreur2: { - spot::emptiness_check ec = spot::emptiness_check(a); - bool res; - + spot::emptiness_check* ec; if (echeck == Couvreur) - res = ec.check(); + ec = new spot::emptiness_check(a); else - res = ec.check2(); + ec = new spot::emptiness_check_shy(a); + + bool res = ec->check(); if (expect_counter_example) { if (res) { exit_code = 1; + delete ec; break; } - spot::counter_example ce(ec.result()); + spot::counter_example ce(ec->result()); ce.print_result(std::cout); } else { exit_code = !res; } + delete ec; } break; case MagicSearch: