From 4e1916ec5075ce05e68d0c2f57c4bc2f55837a44 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Feb 2005 19:14:03 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc (emptiness_check_instantiator): New class. * src/misc/optionmap.hh (set (const option_map&)): New method. * src/tgbatest/randtgba.cc: Create every emptiness check via emptiness_check_instantiator. --- ChangeLog | 6 ++ src/misc/optionmap.cc | 8 +++ src/misc/optionmap.hh | 3 + src/sanity/style.test | 2 +- src/tgbaalgos/emptiness.cc | 144 ++++++++++++++++++++++++++++++++++--- src/tgbaalgos/emptiness.hh | 51 +++++++++++++ src/tgbatest/randtgba.cc | 89 ++++++++++------------- 7 files changed, 239 insertions(+), 64 deletions(-) diff --git a/ChangeLog b/ChangeLog index d03d61e62..3ae44b0a4 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_instantiator): New class. + * src/misc/optionmap.hh (set (const option_map&)): New method. + * src/tgbatest/randtgba.cc: Create every emptiness check via + emptiness_check_instantiator. + * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method. * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc index e4e81b377..ac44bb382 100644 --- a/src/misc/optionmap.cc +++ b/src/misc/optionmap.cc @@ -134,6 +134,14 @@ namespace spot return old; } + void + option_map::set(const option_map& o) + { + for (std::map::const_iterator it = o.options_.begin(); + it != o.options_.end(); ++it) + options_[it->first] = it->second; + } + int& option_map::operator[](const char* option) { diff --git a/src/misc/optionmap.hh b/src/misc/optionmap.hh index eb88c7e54..ab98b2e11 100644 --- a/src/misc/optionmap.hh +++ b/src/misc/optionmap.hh @@ -70,6 +70,9 @@ namespace spot /// or \a def otherwise. int set(const char* option, int val, int def = 0); + /// Acquire all the settings of \a o. + void set(const option_map& o); + /// \brief Get a reference to the current value of \a option. int& operator[](const char* option); diff --git a/src/sanity/style.test b/src/sanity/style.test index ad29f8a61..5609aefc6 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -94,7 +94,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do grep '! ' $tmp && diag 'No space after unary operators (!).' - grep ",[^ \"%']" $tmp && + grep ",[^ \t\"%']" $tmp && diag 'Space after coma.' grep '[^ ]&&[^ ]' $tmp && diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 1efc71924..1edf13711 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -24,9 +24,19 @@ #include "tgba/tgba.hh" #include "tgba/bddprint.hh" #include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/gv04.hh" +#include "tgbaalgos/magic.hh" +#include "tgbaalgos/se05.hh" +#include "tgbaalgos/tau03.hh" +#include "tgbaalgos/tau03opt.hh" namespace spot { + + // tgba_run + ////////////////////////////////////////////////////////////////////// + tgba_run::~tgba_run() { for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i) @@ -51,6 +61,20 @@ namespace spot } } + tgba_run& + tgba_run::operator=(const tgba_run& run) + { + if (&run != this) + { + this->~tgba_run(); + new(this) tgba_run(run); + } + return *this; + } + + // print_tgba_run + ////////////////////////////////////////////////////////////////////// + std::ostream& print_tgba_run(std::ostream& os, const tgba* a, @@ -82,17 +106,8 @@ namespace spot return os; } - tgba_run& - tgba_run::operator=(const tgba_run& run) - { - if (&run != this) - { - this->~tgba_run(); - new(this) tgba_run(run); - } - return *this; - } - + // emptiness_check_result + ////////////////////////////////////////////////////////////////////// tgba_run* emptiness_check_result::accepting_run() @@ -121,6 +136,9 @@ namespace spot } + // emptiness_check + ////////////////////////////////////////////////////////////////////// + emptiness_check::~emptiness_check() { } @@ -157,6 +175,110 @@ namespace spot return os; } + // emptiness_check_instantiator + ////////////////////////////////////////////////////////////////////// + + namespace + { + + spot::emptiness_check* + couvreur99_cons(const spot::tgba* a, spot::option_map o) + { + return spot::couvreur99(a, o); + } + + struct ec_algo + { + const char* name; + spot::emptiness_check* (*construct)(const spot::tgba*, + spot::option_map); + unsigned int min_acc; + unsigned int max_acc; + }; + + ec_algo ec_algos[] = + { + { "Cou99", couvreur99_cons, 0, -1U }, + { "CVWY90", spot::magic_search, 0, 1 }, + { "GV04", spot::explicit_gv04_check, 0, 1 }, + { "SE05", spot::se05, 0, 1 }, + { "Tau03", spot::explicit_tau03_search, 1, -1U }, + { "Tau03_opt", spot::explicit_tau03_opt_search, 0, -1U }, + }; + } + + emptiness_check_instantiator::emptiness_check_instantiator(option_map o, + void* i) + : o_(o), info_(i) + { + } + + unsigned int + emptiness_check_instantiator::min_acceptance_conditions() const + { + return static_cast(info_)->min_acc; + } + + unsigned int + emptiness_check_instantiator::max_acceptance_conditions() const + { + return static_cast(info_)->max_acc; + } + + emptiness_check* + emptiness_check_instantiator::instantiate(const tgba* a) const + { + return static_cast(info_)->construct(a, o_); + } + + emptiness_check_instantiator* + emptiness_check_instantiator::construct(const char* name, const char** err) + { + // Skip spaces. + while (*name && strchr(" \t\n", *name)) + ++name; + + const char* opt_str = strchr(name, '('); + option_map o; + if (opt_str) + { + const char* opt_start = opt_str + 1; + const char* opt_end = strchr(opt_start, ')'); + if (!opt_end) + { + *err = opt_start; + return 0; + } + std::string opt(opt_start, opt_end); + + const char* res = o.parse_options(opt.c_str()); + if (res) + { + *err = opt.c_str() - res + opt_start; + return 0; + } + } + + if (!opt_str) + opt_str = name + strlen(name); + + // Ignore spaces before `(' (or trailing spaces). + while (opt_str > name && strchr(" \t\n", *--opt_str)) + continue; + std::string n(name, opt_str + 1); + + + ec_algo* info = ec_algos; + for (unsigned i = 0; i < sizeof(ec_algos)/sizeof(*ec_algos); ++i, ++info) + if (n == info->name) + return new emptiness_check_instantiator(o, info); + *err = name; + return 0; + } + + // tgba_run_to_tgba + ////////////////////////////////////////////////////////////////////// + namespace { std::string format_state(const tgba* a, const state* s, int n) diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index c22456437..730cd62f7 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -188,6 +188,57 @@ namespace spot option_map o_; ///< The options }; + + // Dynamically create emptiness checks. Given their name and options. + class emptiness_check_instantiator + { + public: + /// \brief Create an emptiness-check instantiator, given the name + /// of an emptiness check. + /// + /// \a name should have the form \c "name" or \c "name(options)". + /// + /// On error, the function returns 0. If the name of the algorithm + /// was unknown, \c *err will be set to \c name. If some fragment of + /// the options could not be parsed, \c *err will point to that + /// fragment. + static emptiness_check_instantiator* construct(const char* name, + const char** err); + + /// Actually instantiate the emptiness check, for \a a. + emptiness_check* instantiate(const tgba* a) const; + + /// Accessor to the options. + /// @{ + const option_map& + options() const + { + return o_; + } + + option_map& + options() + { + return o_; + } + /// @} + + /// \brief Minimum number of acceptance conditions supported by + /// the emptiness check. + unsigned int min_acceptance_conditions() const; + + /// \brief Maximum number of acceptance conditions supported by + /// the emptiness check. + /// + /// \return \c -1U if no upper bound exists. + unsigned int max_acceptance_conditions() const; + private: + emptiness_check_instantiator(option_map o, void* i); + option_map o_; + void *info_; + }; + + /// @} /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 6e04d0d66..63f2208ef 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -53,77 +53,43 @@ #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness_stats.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/gv04.hh" -#include "tgbaalgos/magic.hh" #include "tgbaalgos/reducerun.hh" -#include "tgbaalgos/se05.hh" -#include "tgbaalgos/tau03.hh" -#include "tgbaalgos/tau03opt.hh" #include "tgbaalgos/replayrun.hh" -spot::emptiness_check* -couvreur99_cons(const spot::tgba* a, spot::option_map o) -{ - return spot::couvreur99(a, o); -} - struct ec_algo { const char* name; const char* options; - spot::emptiness_check* (*construct)(const spot::tgba*, spot::option_map o); - unsigned int min_acc; - unsigned int max_acc; + spot::emptiness_check_instantiator* inst; }; ec_algo ec_algos[] = { - { "Cou99", "!poprem", - couvreur99_cons, 0, -1U }, - { "Cou99_shy-", "!poprem shy !group", - couvreur99_cons, 0, -1U }, - { "Cou99_shy", "!poprem shy group", - couvreur99_cons, 0, -1U }, - { "Cou99_rem", "poprem", - couvreur99_cons, 0, -1U }, - { "Cou99_rem_shy-", "poprem shy !group", - couvreur99_cons, 0, -1U }, - { "Cou99_rem_shy", "poprem shy group", - couvreur99_cons, 0, -1U }, - { "CVWY90", 0, - spot::magic_search, 0, 1 }, - { "CVWY90_bsh", "bsh=4K", - spot::magic_search, 0, 1 }, - { "GV04", 0, - spot::explicit_gv04_check, 0, 1 }, - { "SE05", 0, - spot::se05, 0, 1 }, - { "SE05_bsh", "bsh=4K", - spot::se05, 0, 1 }, - { "Tau03", 0, - spot::explicit_tau03_search, 1, -1U }, - { "Tau03_opt", 0, - spot::explicit_tau03_opt_search, 0, -1U }, + { "Cou99", "Cou99(!poprem)", 0 }, + { "Cou99_shy-", "Cou99(!poprem shy !group)", 0 }, + { "Cou99_shy", "Cou99(!poprem shy group)", 0 }, + { "Cou99_rem", "Cou99(poprem)", 0 }, + { "Cou99_rem_shy-", "Cou99(poprem shy !group)", 0 }, + { "Cou99_rem_shy", "Cou99(poprem shy group)", 0 }, + { "CVWY90", "CVWY90", 0 }, + { "CVWY90_bsh", "CVWY90(bsh=4K)", 0 }, + { "GV04", "GV04", 0 }, + { "SE05", "SE05", 0 }, + { "SE05_bsh", "SE05(bsh=4K)", 0 }, + { "Tau03", "Tau03", 0 }, + { "Tau03_opt", "Tau03_opt", 0 }, }; -spot::option_map options; - spot::emptiness_check* cons_emptiness_check(int num, const spot::tgba* a, const spot::tgba* degen, unsigned int n_acc) { - spot::option_map o = options; - if (ec_algos[num].options) - { - const char* err = o.parse_options(ec_algos[num].options); - assert(!err); - (void)err; - } - if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc) + spot::emptiness_check_instantiator* inst = ec_algos[num].inst; + if (n_acc < inst->min_acceptance_conditions() + || n_acc > inst->max_acceptance_conditions()) a = degen; if (a) - return ec_algos[num].construct(a, o); + return inst->instantiate(a); return 0; } @@ -602,6 +568,8 @@ main(int argc, char** argv) spot::tgba* formula = 0; spot::tgba* product = 0; + spot::option_map options; + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; spot::bdd_dict* dict = new spot::bdd_dict(); @@ -807,6 +775,23 @@ main(int argc, char** argv) int init_opt_ec = opt_ec; spot::ltl::atomic_prop_set* apf = new spot::ltl::atomic_prop_set; + if (opt_ec) + { + for (unsigned i = 0; i < sizeof(ec_algos) / sizeof(*ec_algos); ++i) + { + const char* err; + ec_algos[i].inst = + spot::emptiness_check_instantiator::construct(ec_algos[i].options, + &err); + if (ec_algos[i].inst == 0) + { + std::cerr << "Parse error after `" << err << "'" << std::endl; + exit(1); + } + ec_algos[i].inst->options().set(options); + } + } + do { if (opt_F)