diff --git a/ChangeLog b/ChangeLog index 54a96bd36..d03d61e62 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2005-02-17 Alexandre Duret-Lutz + * src/tgbaalgos/emptiness.hh, + src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method. + * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, + src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Implement it. + * src/tgbatest/randtgba.cc: Simplify. + * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Provide wrapper functions that read the hash-map size from a "bsh" option. diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index b9870fbeb..1efc71924 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -51,9 +51,10 @@ namespace spot } } - std::ostream& print_tgba_run(std::ostream& os, - const tgba* a, - const tgba_run* run) + std::ostream& + print_tgba_run(std::ostream& os, + const tgba* a, + const tgba_run* run) { bdd_dict* d = a->get_dict(); os << "Prefix:" << std::endl; @@ -105,6 +106,21 @@ namespace spot return dynamic_cast(this); } + const char* + emptiness_check_result::parse_options(char* options) + { + option_map old(o_); + const char* s = o_.parse_options(options); + options_updated(old); + return s; + } + + void + emptiness_check_result::options_updated(const option_map&) + { + } + + emptiness_check::~emptiness_check() { } @@ -115,6 +131,26 @@ namespace spot return dynamic_cast(this); } + const char* + emptiness_check::parse_options(char* options) + { + option_map old(o_); + const char* s = o_.parse_options(options); + options_updated(old); + return s; + } + + void + emptiness_check::options_updated(const option_map&) + { + } + + bool + emptiness_check::safe() const + { + return true; + } + std::ostream& emptiness_check::print_stats(std::ostream& os) const { @@ -131,7 +167,8 @@ namespace spot } } - tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run) + tgba* + tgba_run_to_tgba(const tgba* a, const tgba_run* run) { tgba_explicit* res = new tgba_explicit(a->get_dict()); res->copy_acceptance_conditions_of(a); diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 40d1b73fe..c22456437 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -114,29 +114,18 @@ namespace spot return o_; } - /// Modify the options parametrizing how the accepting run is computed. - const char* - parse_options(char* options) - { - option_map old(o_); - const char* s = o_.parse_options(options); - options_updated(old); - return s; - } + /// Modify the algorithm options. + const char* parse_options(char* options); /// Return statistics, if available. virtual const unsigned_statistics* statistics() const; protected: - /// React when options are modified. - virtual void - options_updated(const option_map& old) - { - (void)old; - } + /// Notify option updates. + virtual void options_updated(const option_map& old); const tgba* a_; ///< The automaton. - option_map o_; ///< The options + option_map o_; ///< The options. }; /// Common interface to emptiness check algorithms. @@ -163,19 +152,15 @@ namespace spot return o_; } - /// Modify the options parametrizing how the accepting run is realized. - const char* - parse_options(char* options) - { - option_map old(o_); - const char* s = o_.parse_options(options); - options_updated(old); - return s; - } + /// Modify the algorithm options. + const char* parse_options(char* options); + + /// Return false iff accepting_run() can return 0 for non-empty automata. + virtual bool safe() const; /// \brief Check whether the automaton contain an accepting run. /// - /// Return 0 if the automaton accept no run. Return an instance + /// Return 0 if the automaton accepts no run. Return an instance /// of emptiness_check_result otherwise. This instance might /// allow to obtain one sample acceptance run. The result has to /// be destroyed before the emptiness_check instance that @@ -183,6 +168,10 @@ namespace spot /// /// Some emptiness_check algorithms may allow check() to be called /// several time, but generally you should not assume that. + /// + /// Some emptiness_check algorithms, especially those using bit state + /// hashing may return 0 even if the automaton is not empty. + /// \see safe() virtual emptiness_check_result* check() = 0; /// Return statistics, if available. @@ -191,11 +180,8 @@ namespace spot /// Print statistics, if any. virtual std::ostream& print_stats(std::ostream& os) const; - /// React when options are modified. - virtual void options_updated(const option_map& old) - { - (void)old; - } + /// Notify option updates. + virtual void options_updated(const option_map& old); protected: const tgba* a_; ///< The automaton. diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index cb600f7ef..94164558d 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -125,20 +125,25 @@ namespace spot return os; } + virtual bool safe() const + { + return heap::Safe; + } + const heap& get_heap() const - { - return h; - } + { + return h; + } const stack_type& get_st_blue() const - { - return st_blue; - } + { + return st_blue; + } const stack_type& get_st_red() const - { - return st_red; - } + { + return st_red; + } private: void push(stack_type& st, const state* s, @@ -421,6 +426,8 @@ namespace spot class explicit_magic_search_heap { public: + enum { Safe = 1 }; + class color_ref { public: @@ -505,6 +512,8 @@ namespace spot class bsh_magic_search_heap { public: + enum { Safe = 0 }; + class color_ref { public: diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 8f56e2412..7b858933b 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -125,24 +125,29 @@ namespace spot return os; } + virtual bool safe() const + { + return heap::Safe; + } + const heap& get_heap() const - { - return h; - } + { + return h; + } const stack_type& get_st_blue() const - { - return st_blue; - } + { + return st_blue; + } const stack_type& get_st_red() const - { - return st_red; - } + { + return st_red; + } private: void push(stack_type& st, const state* s, - const bdd& label, const bdd& acc) + const bdd& label, const bdd& acc) { inc_depth(); tgba_succ_iterator* i = a_->succ_iter(s); @@ -436,6 +441,8 @@ namespace spot typedef Sgi::hash_map hash_type; public: + enum { Safe = 1 }; + class color_ref { public: @@ -568,6 +575,8 @@ namespace spot typedef Sgi::hash_set hcyan_type; public: + enum { Safe = 0 }; + class color_ref { public: diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 91a07fdda..6e04d0d66 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -75,37 +75,36 @@ struct ec_algo spot::emptiness_check* (*construct)(const spot::tgba*, spot::option_map o); unsigned int min_acc; unsigned int max_acc; - bool safe; }; ec_algo ec_algos[] = { { "Cou99", "!poprem", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "Cou99_shy-", "!poprem shy !group", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "Cou99_shy", "!poprem shy group", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "Cou99_rem", "poprem", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "Cou99_rem_shy-", "poprem shy !group", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "Cou99_rem_shy", "poprem shy group", - couvreur99_cons, 0, -1U, true }, + couvreur99_cons, 0, -1U }, { "CVWY90", 0, - spot::magic_search, 0, 1, true }, + spot::magic_search, 0, 1 }, { "CVWY90_bsh", "bsh=4K", - spot::magic_search, 0, 1, false }, + spot::magic_search, 0, 1 }, { "GV04", 0, - spot::explicit_gv04_check, 0, 1, true }, + spot::explicit_gv04_check, 0, 1 }, { "SE05", 0, - spot::se05, 0, 1, true }, + spot::se05, 0, 1 }, { "SE05_bsh", "bsh=4K", - spot::se05, 0, 1, false }, + spot::se05, 0, 1 }, { "Tau03", 0, - spot::explicit_tau03_search, 1, -1U, true }, + spot::explicit_tau03_search, 1, -1U }, { "Tau03_opt", 0, - spot::explicit_tau03_opt_search, 0, -1U, true }, + spot::explicit_tau03_opt_search, 0, -1U }, }; spot::option_map options; @@ -1038,7 +1037,7 @@ main(int argc, char** argv) } else { - if (ec_algos[i].safe) + if (ec->safe()) { if (!opt_paper) std::cout << "empty language" << std::endl;