From c1d0cab3af68b7d882dcb00eb3e77bccb7cde7f8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Feb 2005 16:09:56 +0000 Subject: [PATCH] * 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. * src/tgbatest/randtgba.cc: Simplify. --- ChangeLog | 5 +++++ src/tgbaalgos/magic.cc | 31 ++++++++++++++++++++----------- src/tgbaalgos/magic.hh | 14 ++++++++++++-- src/tgbaalgos/se05.cc | 9 +++++++++ src/tgbaalgos/se05.hh | 9 +++++++++ src/tgbatest/randtgba.cc | 36 ++++++------------------------------ 6 files changed, 61 insertions(+), 43 deletions(-) diff --git a/ChangeLog b/ChangeLog index 9cff3f881..54a96bd36 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2005-02-17 Alexandre Duret-Lutz + * 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. + * src/tgbatest/randtgba.cc: Simplify. + * src/misc/optionmap.hh, src/misc/optionmap.cc (option_map::parse_options): Rewrite. Do not modify the input string, allow !foo as a shorthand for foo=0, and support K and diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 108779564..cb600f7ef 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -46,14 +46,14 @@ namespace spot /// \brief Emptiness checker on spot::tgba automata having at most one /// accepting condition (i.e. a TBA). template - class magic_search : public emptiness_check, public ec_statistics + class magic_search_ : public emptiness_check, public ec_statistics { public: /// \brief Initialize the Magic Search algorithm on the automaton \a a /// /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). - magic_search(const tgba *a, size_t size, option_map o = option_map()) + magic_search_(const tgba *a, size_t size, option_map o = option_map()) : emptiness_check(a, o), h(size), all_cond(a->all_acceptance_conditions()) @@ -61,7 +61,7 @@ namespace spot assert(a->number_of_acceptance_conditions() <= 1); } - virtual ~magic_search() + virtual ~magic_search_() { // Release all iterators on the stacks. while (!st_blue.empty()) @@ -318,7 +318,7 @@ namespace spot public acss_statistics { public: - result_from_stack(magic_search& ms) + result_from_stack(magic_search_& ms) : emptiness_check_result(ms.automaton()), ms_(ms) { } @@ -366,7 +366,7 @@ namespace spot return 0; } private: - magic_search& ms_; + magic_search_& ms_; }; # define FROM_STACK "ar:from_stack" @@ -374,13 +374,13 @@ namespace spot class magic_search_result: public emptiness_check_result { public: - magic_search_result(magic_search& m, option_map o = option_map()) + magic_search_result(magic_search_& m, option_map o = option_map()) : emptiness_check_result(m.automaton(), o), ms(m) { if (options()[FROM_STACK]) computer = new result_from_stack(ms); else - computer = new ndfs_result, heap>(ms); + computer = new ndfs_result, heap>(ms); } virtual void options_updated(const option_map& old) @@ -388,7 +388,7 @@ namespace spot if (old[FROM_STACK] && !options()[FROM_STACK]) { delete computer; - computer = new ndfs_result, heap>(ms); + computer = new ndfs_result, heap>(ms); } else if (!old[FROM_STACK] && options()[FROM_STACK]) { @@ -414,7 +414,7 @@ namespace spot private: emptiness_check_result* computer; - magic_search& ms; + magic_search_& ms; }; }; @@ -575,13 +575,22 @@ namespace spot emptiness_check* explicit_magic_search(const tgba *a, option_map o) { - return new magic_search(a, 0, o); + return new magic_search_(a, 0, o); } emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size, option_map o) { - return new magic_search(a, size, o); + return new magic_search_(a, size, o); + } + + emptiness_check* + magic_search(const tgba *a, option_map o) + { + size_t size = o.get("bsh"); + if (size) + return bit_state_hashing_magic_search(a, size, o); + return explicit_magic_search(a, o); } } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index be6e44187..f26da8162 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -82,7 +82,7 @@ namespace spot /// (which deals with accepting states) presented in /// /// \verbatim - /// Article{ courcoubertis.92.fmsd, + /// Article{ courcoubetis.92.fmsd, /// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre /// Wolper and Mihalis Yannakakis}, /// title = {Memory-Efficient Algorithm for the Verification of @@ -94,6 +94,8 @@ namespace spot /// } /// \endverbatim /// + /// \fixme The name is misleading. Magic-search is the algorithm + /// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd. emptiness_check* explicit_magic_search(const tgba *a, option_map o = option_map()); @@ -127,6 +129,14 @@ namespace spot emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size, option_map o = option_map()); + /// \brief Wrapper for the two magic_search implementations. + /// + /// This wrapper calls explicit_magic_search_search() or + /// bit_state_hashing_magic_search() according to the \c "bsh" option + /// in the \c option_map. If \c "bsh" is set and non null, its value + /// is used as the size of the hash map. + emptiness_check* magic_search(const tgba *a, option_map o = option_map()); + /// @} } diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 059855d44..8f56e2412 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -675,4 +675,13 @@ namespace spot return new se05_search(a, size, o); } + emptiness_check* + se05(const tgba *a, option_map o) + { + size_t size = o.get("bsh"); + if (size) + return bit_state_hashing_se05_search(a, size, o); + return explicit_se05_search(a, o); + } + } diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index fd24af89a..e8f58f062 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -133,6 +133,15 @@ namespace spot emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size, option_map o = option_map()); + + /// \brief Wrapper for the two se05 implementations. + /// + /// This wrapper calls explicit_se05_search() or + /// bit_state_hashing_se05_search() according to the \c "bsh" option + /// in the \c option_map. If \c "bsh" is set and non null, its value + /// is used as the size of the hash map. + emptiness_check* se05(const tgba *a, option_map o); + /// @} } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index b41f7cb19..91a07fdda 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -68,30 +68,6 @@ couvreur99_cons(const spot::tgba* a, spot::option_map o) return spot::couvreur99(a, o); } -spot::emptiness_check* -ms_cons(const spot::tgba* a, spot::option_map o) -{ - return spot::explicit_magic_search(a, o); -} - -spot::emptiness_check* -se05_cons(const spot::tgba* a, spot::option_map o) -{ - return spot::explicit_se05_search(a, o); -} - -spot::emptiness_check* -bsh_ms_cons(const spot::tgba* a, spot::option_map o) -{ - return spot::bit_state_hashing_magic_search(a, 4096, o); -} - -spot::emptiness_check* -bsh_se05_cons(const spot::tgba* a, spot::option_map o) -{ - return spot::bit_state_hashing_se05_search(a, 4096, o); -} - struct ec_algo { const char* name; @@ -117,15 +93,15 @@ ec_algo ec_algos[] = { "Cou99_rem_shy", "poprem shy group", couvreur99_cons, 0, -1U, true }, { "CVWY90", 0, - ms_cons, 0, 1, true }, - { "CVWY90_bsh", 0, - bsh_ms_cons, 0, 1, false }, + spot::magic_search, 0, 1, true }, + { "CVWY90_bsh", "bsh=4K", + spot::magic_search, 0, 1, false }, { "GV04", 0, spot::explicit_gv04_check, 0, 1, true }, { "SE05", 0, - se05_cons, 0, 1, true }, - { "SE05_bsh", 0, - bsh_se05_cons, 0, 1, false }, + spot::se05, 0, 1, true }, + { "SE05_bsh", "bsh=4K", + spot::se05, 0, 1, false }, { "Tau03", 0, spot::explicit_tau03_search, 1, -1U, true }, { "Tau03_opt", 0,