diff --git a/ChangeLog b/ChangeLog index 2f13fb803..edb14e13b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2005-02-16 Alexandre Duret-Lutz + + * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get, + option_map::set): Handle default values. + (anonymous::to_int): Do not print anything. + * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh, + src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh, + src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in + the constructor. + * src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise. Handle + the "poprem", "group", and "shy" options via the option_map. + Supply a couvreur99() wrapper to the shy/non-shy variant. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc, + iface/gspn/ssp.cc: Adjust. + 2005-02-08 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Factorize more code using the diff --git a/INSTALL b/INSTALL index 54caf7c19..56b077d6a 100644 --- a/INSTALL +++ b/INSTALL @@ -1,13 +1,16 @@ -Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software -Foundation, Inc. +Installation Instructions +************************* - This file is free documentation; the Free Software Foundation gives +Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002, 2004, 2005 Free +Software Foundation, Inc. + +This file is free documentation; the Free Software Foundation gives unlimited permission to copy, distribute and modify it. Basic Installation ================== - These are generic installation instructions. +These are generic installation instructions. The `configure' shell script attempts to guess correct values for various system-dependent variables used during compilation. It uses @@ -67,9 +70,9 @@ The simplest way to compile this package is: Compilers and Options ===================== - Some systems require unusual options for compilation or linking that -the `configure' script does not know about. Run `./configure --help' -for details on some of the pertinent environment variables. +Some systems require unusual options for compilation or linking that the +`configure' script does not know about. Run `./configure --help' for +details on some of the pertinent environment variables. You can give `configure' initial values for configuration parameters by setting variables in the command line or in the environment. Here @@ -82,7 +85,7 @@ is an example: Compiling For Multiple Architectures ==================================== - You can compile the package for more than one kind of computer at the +You can compile the package for more than one kind of computer at the same time, by placing the object files for each architecture in their own directory. To do this, you must use a version of `make' that supports the `VPATH' variable, such as GNU `make'. `cd' to the @@ -99,19 +102,19 @@ for another architecture. Installation Names ================== - By default, `make install' will install the package's files in +By default, `make install' will install the package's files in `/usr/local/bin', `/usr/local/man', etc. You can specify an installation prefix other than `/usr/local' by giving `configure' the -option `--prefix=PATH'. +option `--prefix=PREFIX'. You can specify separate installation prefixes for architecture-specific files and architecture-independent files. If you -give `configure' the option `--exec-prefix=PATH', the package will use -PATH as the prefix for installing programs and libraries. +give `configure' the option `--exec-prefix=PREFIX', the package will +use PREFIX as the prefix for installing programs and libraries. Documentation and other data files will still use the regular prefix. In addition, if you use an unusual directory layout you can give -options like `--bindir=PATH' to specify different values for particular +options like `--bindir=DIR' to specify different values for particular kinds of files. Run `configure --help' for a list of the directories you can set and what kinds of files go in them. @@ -122,7 +125,7 @@ option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'. Optional Features ================= - Some packages pay attention to `--enable-FEATURE' options to +Some packages pay attention to `--enable-FEATURE' options to `configure', where FEATURE indicates an optional part of the package. They may also pay attention to `--with-PACKAGE' options, where PACKAGE is something like `gnu-as' or `x' (for the X Window System). The @@ -137,11 +140,11 @@ you can use the `configure' options `--x-includes=DIR' and Specifying the System Type ========================== - There may be some features `configure' cannot figure out -automatically, but needs to determine by the type of machine the package -will run on. Usually, assuming the package is built to be run on the -_same_ architectures, `configure' can figure that out, but if it prints -a message saying it cannot guess the machine type, give it the +There may be some features `configure' cannot figure out automatically, +but needs to determine by the type of machine the package will run on. +Usually, assuming the package is built to be run on the _same_ +architectures, `configure' can figure that out, but if it prints a +message saying it cannot guess the machine type, give it the `--build=TYPE' option. TYPE can either be a short name for the system type, such as `sun4', or a canonical name which has the form: @@ -167,9 +170,9 @@ eventually be run) with `--host=TYPE'. Sharing Defaults ================ - If you want to set default values for `configure' scripts to share, -you can create a site shell script called `config.site' that gives -default values for variables like `CC', `cache_file', and `prefix'. +If you want to set default values for `configure' scripts to share, you +can create a site shell script called `config.site' that gives default +values for variables like `CC', `cache_file', and `prefix'. `configure' looks for `PREFIX/share/config.site' if it exists, then `PREFIX/etc/config.site' if it exists. Or, you can set the `CONFIG_SITE' environment variable to the location of the site script. @@ -178,7 +181,7 @@ A warning: not all `configure' scripts look for a site script. Defining Variables ================== - Variables not defined in a site shell script can be set in the +Variables not defined in a site shell script can be set in the environment passed to `configure'. However, some packages may run configure again during the build, and the customized values of these variables may be lost. In order to avoid this problem, you should set @@ -186,14 +189,18 @@ them in the `configure' command line, using `VAR=value'. For example: ./configure CC=/usr/local2/bin/gcc -will cause the specified gcc to be used as the C compiler (unless it is -overridden in the site shell script). +causes the specified `gcc' to be used as the C compiler (unless it is +overridden in the site shell script). Here is a another example: + + /bin/bash ./configure CONFIG_SHELL=/bin/bash + +Here the `CONFIG_SHELL=/bin/bash' operand causes subsequent +configuration-related scripts to be executed by `/bin/bash'. `configure' Invocation ====================== - `configure' recognizes the following options to control how it -operates. +`configure' recognizes the following options to control how it operates. `--help' `-h' diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index dd37b5106..c9e4ce1ba 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -913,9 +913,9 @@ namespace spot public: couvreur99_check_shy_ssp(const tgba* a) : couvreur99_check_shy(a, - true, + option_map(), numbered_state_heap_ssp_factory_semi::instance()) - { + { } protected: @@ -995,6 +995,7 @@ namespace spot assert(dynamic_cast(ssp_automata)); return new couvreur99_check(ssp_automata, + option_map(), numbered_state_heap_ssp_factory_semi::instance()); } @@ -1005,7 +1006,7 @@ namespace spot return new couvreur99_check_shy (ssp_automata, - true, + option_map(), numbered_state_heap_ssp_factory_semi::instance()); } diff --git a/lbtt/INSTALL b/lbtt/INSTALL index 54caf7c19..56b077d6a 100644 --- a/lbtt/INSTALL +++ b/lbtt/INSTALL @@ -1,13 +1,16 @@ -Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software -Foundation, Inc. +Installation Instructions +************************* - This file is free documentation; the Free Software Foundation gives +Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002, 2004, 2005 Free +Software Foundation, Inc. + +This file is free documentation; the Free Software Foundation gives unlimited permission to copy, distribute and modify it. Basic Installation ================== - These are generic installation instructions. +These are generic installation instructions. The `configure' shell script attempts to guess correct values for various system-dependent variables used during compilation. It uses @@ -67,9 +70,9 @@ The simplest way to compile this package is: Compilers and Options ===================== - Some systems require unusual options for compilation or linking that -the `configure' script does not know about. Run `./configure --help' -for details on some of the pertinent environment variables. +Some systems require unusual options for compilation or linking that the +`configure' script does not know about. Run `./configure --help' for +details on some of the pertinent environment variables. You can give `configure' initial values for configuration parameters by setting variables in the command line or in the environment. Here @@ -82,7 +85,7 @@ is an example: Compiling For Multiple Architectures ==================================== - You can compile the package for more than one kind of computer at the +You can compile the package for more than one kind of computer at the same time, by placing the object files for each architecture in their own directory. To do this, you must use a version of `make' that supports the `VPATH' variable, such as GNU `make'. `cd' to the @@ -99,19 +102,19 @@ for another architecture. Installation Names ================== - By default, `make install' will install the package's files in +By default, `make install' will install the package's files in `/usr/local/bin', `/usr/local/man', etc. You can specify an installation prefix other than `/usr/local' by giving `configure' the -option `--prefix=PATH'. +option `--prefix=PREFIX'. You can specify separate installation prefixes for architecture-specific files and architecture-independent files. If you -give `configure' the option `--exec-prefix=PATH', the package will use -PATH as the prefix for installing programs and libraries. +give `configure' the option `--exec-prefix=PREFIX', the package will +use PREFIX as the prefix for installing programs and libraries. Documentation and other data files will still use the regular prefix. In addition, if you use an unusual directory layout you can give -options like `--bindir=PATH' to specify different values for particular +options like `--bindir=DIR' to specify different values for particular kinds of files. Run `configure --help' for a list of the directories you can set and what kinds of files go in them. @@ -122,7 +125,7 @@ option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'. Optional Features ================= - Some packages pay attention to `--enable-FEATURE' options to +Some packages pay attention to `--enable-FEATURE' options to `configure', where FEATURE indicates an optional part of the package. They may also pay attention to `--with-PACKAGE' options, where PACKAGE is something like `gnu-as' or `x' (for the X Window System). The @@ -137,11 +140,11 @@ you can use the `configure' options `--x-includes=DIR' and Specifying the System Type ========================== - There may be some features `configure' cannot figure out -automatically, but needs to determine by the type of machine the package -will run on. Usually, assuming the package is built to be run on the -_same_ architectures, `configure' can figure that out, but if it prints -a message saying it cannot guess the machine type, give it the +There may be some features `configure' cannot figure out automatically, +but needs to determine by the type of machine the package will run on. +Usually, assuming the package is built to be run on the _same_ +architectures, `configure' can figure that out, but if it prints a +message saying it cannot guess the machine type, give it the `--build=TYPE' option. TYPE can either be a short name for the system type, such as `sun4', or a canonical name which has the form: @@ -167,9 +170,9 @@ eventually be run) with `--host=TYPE'. Sharing Defaults ================ - If you want to set default values for `configure' scripts to share, -you can create a site shell script called `config.site' that gives -default values for variables like `CC', `cache_file', and `prefix'. +If you want to set default values for `configure' scripts to share, you +can create a site shell script called `config.site' that gives default +values for variables like `CC', `cache_file', and `prefix'. `configure' looks for `PREFIX/share/config.site' if it exists, then `PREFIX/etc/config.site' if it exists. Or, you can set the `CONFIG_SITE' environment variable to the location of the site script. @@ -178,7 +181,7 @@ A warning: not all `configure' scripts look for a site script. Defining Variables ================== - Variables not defined in a site shell script can be set in the +Variables not defined in a site shell script can be set in the environment passed to `configure'. However, some packages may run configure again during the build, and the customized values of these variables may be lost. In order to avoid this problem, you should set @@ -186,14 +189,18 @@ them in the `configure' command line, using `VAR=value'. For example: ./configure CC=/usr/local2/bin/gcc -will cause the specified gcc to be used as the C compiler (unless it is -overridden in the site shell script). +causes the specified `gcc' to be used as the C compiler (unless it is +overridden in the site shell script). Here is a another example: + + /bin/bash ./configure CONFIG_SHELL=/bin/bash + +Here the `CONFIG_SHELL=/bin/bash' operand causes subsequent +configuration-related scripts to be executed by `/bin/bash'. `configure' Invocation ====================== - `configure' recognizes the following options to control how it -operates. +`configure' recognizes the following options to control how it operates. `--help' `-h' diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc index caa366b22..a2430dc77 100644 --- a/src/misc/optionmap.cc +++ b/src/misc/optionmap.cc @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include #include #include #include "optionmap.hh" @@ -34,44 +33,43 @@ namespace spot char* endptr; int res = strtol(s, &endptr, 10); if (*endptr) - { - std::cerr << "Failed to parse `" << s << "' as an integer." - << std::endl; - return false; - } + return false; i = res; return true; } }; - const char* option_map::parse_options(char* options) + const char* + option_map::parse_options(char* options) { - char* opt = strtok(options, ", \t;"); - while (opt) - { - char* equal; - if ((equal = strchr(opt, '=')) != 0) - { - *equal = 0; - int val; - if (!to_int(equal+1, val)) - return opt; - options_[opt] = val; - } - else - // default value if declared - options_[opt] = 1; - opt = strtok(0, ", \t;"); - } - return 0; + char* opt = strtok(options, ", \t;"); + while (opt) + { + char* equal = strchr(opt, '='); + if (equal) + { + *equal = 0; + int val; + if (!to_int(equal + 1, val)) + return opt; + options_[opt] = val; + } + else + { + options_[opt] = 1; + } + opt = strtok(0, ", \t;"); + } + return 0; } - int option_map::get(const char* option) const + int + option_map::get(const char* option, int def) const { std::map::const_iterator it = options_.find(option); if (it == options_.end()) // default value if not declared - return 0; + return def; else return it->second; } @@ -81,22 +79,25 @@ namespace spot return get(option); } - int option_map::set(const char* option, int val) + int + option_map::set(const char* option, int val, int def) { - int old = get(option); + int old = get(option, def); options_[option] = val; return old; } - int& option_map::operator[](const char* option) + int& + option_map::operator[](const char* option) { return options_[option]; } - std::ostream& operator<<(std::ostream& os, const option_map& m) + std::ostream& + operator<<(std::ostream& os, const option_map& m) { for (std::map::const_iterator it = m.options_.begin(); - it != m.options_.end(); ++it) + it != m.options_.end(); ++it) os << "\"" << it->first << "\" = " << it->second << std::endl; return os; } diff --git a/src/misc/optionmap.hh b/src/misc/optionmap.hh index 610ddf864..baa66d5f7 100644 --- a/src/misc/optionmap.hh +++ b/src/misc/optionmap.hh @@ -46,19 +46,22 @@ namespace spot /// \brief Get the value of \a option. /// - /// \return The value associated to \a option if it exists, 0 otherwise. - int get(const char* option) const; + /// \return The value associated to \a option if it exists, + /// \a def otherwise. + /// \see operator[]() + int get(const char* option, int def = 0) const; /// \brief Get the value of \a option. /// /// \return The value associated to \a option if it exists, 0 otherwise. + /// \see get() int operator[](const char* option) const; /// \brief Set the value of \a option to \a val. /// - /// \return The current value associated to \a option if declared, - /// 0 otherwise. - int set(const char* option, int val); + /// \return The previous value associated to \a option if declared, + /// or \a def otherwise. + int set(const char* option, int val, int def = 0); /// \brief Get a reference to the current value of \a option. int& operator[](const char* option); diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 996e6c387..40d1b73fe 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -129,7 +129,8 @@ namespace spot protected: /// React when options are modified. - virtual void options_updated(const option_map& old) + virtual void + options_updated(const option_map& old) { (void)old; } diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 3bd34ff20..8c4f56d4c 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -77,8 +77,8 @@ namespace spot } couvreur99_check_result::couvreur99_check_result - (const couvreur99_check_status* ecs) - : emptiness_check_result(ecs->aut), ecs_(ecs) + (const couvreur99_check_status* ecs, option_map o) + : emptiness_check_result(ecs->aut, o), ecs_(ecs) { } diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index 76102c2c0..255ef39ae 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -34,7 +34,8 @@ namespace spot public acss_statistics { public: - couvreur99_check_result(const couvreur99_check_status* ecs); + couvreur99_check_result(const couvreur99_check_status* ecs, + option_map o = option_map()); virtual tgba_run* accepting_run(); diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 82d7a6e63..2a06d4c50 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -30,10 +30,11 @@ namespace spot } couvreur99_check::couvreur99_check(const tgba* a, - bool poprem, + option_map o, const numbered_state_heap_factory* nshf) - : emptiness_check(a), poprem_(poprem) + : emptiness_check(a, o) { + poprem_ = o.get("poprem", 1); ecs_ = new couvreur99_check_status(a, nshf); } @@ -262,7 +263,7 @@ namespace spot // cycle. ecs_->cycle_seed = spi.first; set_states(ecs_->states()); - return new couvreur99_check_result(ecs_); + return new couvreur99_check_result(ecs_, options()); } } // This automaton recognizes no word. @@ -288,12 +289,13 @@ namespace spot ////////////////////////////////////////////////////////////////////// couvreur99_check_shy::couvreur99_check_shy(const tgba* a, - bool poprem, - bool group, + option_map o, const numbered_state_heap_factory* nshf) - : couvreur99_check(a, poprem, nshf), num(1), group_(group) + : couvreur99_check(a, o, nshf), num(1) { + group_ = o.get("group", 1); + // Setup depth-first search from the initial state. todo.push_back(todo_item(0, 0)); todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state())); @@ -409,7 +411,7 @@ namespace spot // We have found an accepting SCC. Clean up TODO. clear_todo(); set_states(ecs_->states()); - return new couvreur99_check_result(ecs_); + return new couvreur99_check_result(ecs_, options()); } continue; @@ -491,7 +493,7 @@ namespace spot clear_todo(); set_states(ecs_->states()); delete iter; - return new couvreur99_check_result(ecs_); + return new couvreur99_check_result(ecs_, options()); } // Group the pending successors of formed SCC if requested. if (group_) @@ -560,7 +562,7 @@ namespace spot // We have found an accepting SCC. Clean up TODO. clear_todo(); set_states(ecs_->states()); - return new couvreur99_check_result(ecs_); + return new couvreur99_check_result(ecs_, options()); } } } @@ -573,4 +575,14 @@ namespace spot return ecs_->h->find(s).second; } + emptiness_check* + couvreur99(const tgba* a, + option_map o, + const numbered_state_heap_factory* nshf) + { + if (o.get("shy")) + return new couvreur99_check_shy(a, o, nshf); + return new couvreur99_check(a, o, nshf); + } + } diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index c49a37203..c2f3a45ac 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -113,19 +113,43 @@ namespace spot /// at once in order to decide which to explore first, and must keep /// a list of all unexplored successors in its DFS stack. /// - /// The \c poprem parameter specifies how the algorithm should - /// handle the destruction of non-accepting maximal strongly - /// connected components. If \c poprem is true, the algorithm will - /// keep a list of all states of a SCC that are fully processed and - /// should be removed once the MSCC is popped. If \c poprem is - /// false, the MSCC will be traversed again (i.e. generating the - /// successors of the root recursively) for deletion. This is - /// a choice between memory and speed. + /// The couvreur99() function is a wrapper around these two flavors + /// of the algorithm. \a options is an option map that specifies + /// which algorithms should be used, and how. + /// + /// The following options are available. + /// \li \c "shy" : if non zero, then spot::couvreur99_check_shy is used, + /// otherwise (and by default) spot::couvreur99_check is used. + /// + /// \li \c "poprem" : specifies how the algorithm should handle the + /// destruction of non-accepting maximal strongly connected + /// components. If \c poprem is non null, the algorithm will keep a + /// list of all states of a SCC that are fully processed and should + /// be removed once the MSCC is popped. If \c poprem is null (the + /// default), the MSCC will be traversed again (i.e. generating the + /// successors of the root recursively) for deletion. This is a + /// choice between memory and speed. + /// + /// \li \c "group" : this options is used only by spot::couvreur99_check_shy. + /// If non null (the default), the successors of all the + /// states that belong to the same SCC will be considered when + /// choosing a successor. Otherwise, only the successor of the + /// topmost state on the DFS stack are considered. + emptiness_check* + couvreur99(const tgba* a, + option_map options = option_map(), + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); + + + /// \brief An implementation of the Couvreur99 emptiness-check algorithm. + /// + /// See the documentation for spot::couvreur99. class couvreur99_check: public emptiness_check, public ec_statistics { public: couvreur99_check(const tgba* a, - bool poprem = true, + option_map o = option_map(), const numbered_state_heap_factory* nshf = numbered_state_heap_hash_map_factory::instance()); virtual ~couvreur99_check(); @@ -161,18 +185,12 @@ namespace spot /// \brief A version of spot::couvreur99_check that tries to visit /// known states first. /// - /// If \a group is true (the default), the successors of all the - /// states that belong to the same SCC will be considered when - /// choosing a successor. Otherwise, only the successor of the - /// topmost state on the DFS stack are considered. - /// - /// See the documentation for spot::couvreur99_check + /// See the documentation for spot::couvreur99. class couvreur99_check_shy : public couvreur99_check { public: couvreur99_check_shy(const tgba* a, - bool poprem = true, - bool group = true, + option_map o = option_map(), const numbered_state_heap_factory* nshf = numbered_state_heap_hash_map_factory::instance()); virtual ~couvreur99_check_shy(); @@ -231,6 +249,7 @@ namespace spot virtual int* find_state(const state* s); }; + /// @} } diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 25f868479..daf7b52cb 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -69,8 +69,8 @@ namespace spot int dftop; // Top of DFS stack. bool violation; // Whether an accepting run was found. - gv04(const tgba *a) - : emptiness_check(a), accepting(a->all_acceptance_conditions()) + gv04(const tgba *a, option_map o) + : emptiness_check(a, o), accepting(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -243,7 +243,8 @@ namespace spot gv04& data; result(gv04& data) - : emptiness_check_result(data.automaton()), data(data) + : emptiness_check_result(data.automaton(), data.options()), + data(data) { } @@ -405,8 +406,8 @@ namespace spot } // anonymous emptiness_check* - explicit_gv04_check(const tgba* a) + explicit_gv04_check(const tgba* a, option_map o) { - return new gv04(a); + return new gv04(a, o); } } diff --git a/src/tgbaalgos/gv04.hh b/src/tgbaalgos/gv04.hh index 4a17cf95c..88ef0e88b 100644 --- a/src/tgbaalgos/gv04.hh +++ b/src/tgbaalgos/gv04.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. // @@ -22,6 +22,8 @@ #ifndef SPOT_TGBAALGOS_GV04_HH # define SPOT_TGBAALGOS_GV04_HH +#include "misc/optionmap.hh" + namespace spot { class tgba; @@ -51,7 +53,8 @@ namespace spot /// isbn = {3-540-21299-X} /// } /// \endverbatim - emptiness_check* explicit_gv04_check(const tgba* a); + emptiness_check* explicit_gv04_check(const tgba* a, + option_map o = option_map()); } #endif // SPOT_TGBAALGOS_GV04_HH diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index 5f19ce139..fd24af89a 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -131,7 +131,7 @@ namespace spot /// \sa spot::explicit_se05_search /// emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size, - option_map o = option_map()); + option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 5e2b9404b..39ad387a6 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -53,8 +53,8 @@ namespace spot { public: /// \brief Initialize the search algorithm on the automaton \a a - tau03_search(const tgba *a, size_t size) - : emptiness_check(a), + tau03_search(const tgba *a, size_t size, option_map o) + : emptiness_check(a, o), h(size), all_cond(a->all_acceptance_conditions()) { @@ -375,9 +375,9 @@ namespace spot } // anonymous - emptiness_check* explicit_tau03_search(const tgba *a) + emptiness_check* explicit_tau03_search(const tgba *a, option_map o) { - return new tau03_search(a, 0); + return new tau03_search(a, 0, o); } } diff --git a/src/tgbaalgos/tau03.hh b/src/tgbaalgos/tau03.hh index b63b7c9dd..0e386e049 100644 --- a/src/tgbaalgos/tau03.hh +++ b/src/tgbaalgos/tau03.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. // @@ -93,7 +93,8 @@ namespace spot /// } /// \endverbatim /// - emptiness_check* explicit_tau03_search(const tgba *a); + emptiness_check* explicit_tau03_search(const tgba *a, + option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index f8dc61263..1e4d21bda 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -62,8 +62,8 @@ namespace spot { public: /// \brief Initialize the search algorithm on the automaton \a a - tau03_opt_search(const tgba *a, size_t size) - : emptiness_check(a), + tau03_opt_search(const tgba *a, size_t size, option_map o) + : emptiness_check(a, o), current_weight(a->neg_acceptance_conditions()), h(size), all_acc(a->all_acceptance_conditions()) @@ -497,9 +497,9 @@ namespace spot } // anonymous - emptiness_check* explicit_tau03_opt_search(const tgba *a) + emptiness_check* explicit_tau03_opt_search(const tgba *a, option_map o) { - return new tau03_opt_search(a, 0); + return new tau03_opt_search(a, 0, o); } } diff --git a/src/tgbaalgos/tau03opt.hh b/src/tgbaalgos/tau03opt.hh index bd942bd59..2d2449356 100644 --- a/src/tgbaalgos/tau03opt.hh +++ b/src/tgbaalgos/tau03opt.hh @@ -95,7 +95,8 @@ namespace spot /// the path stored in the blue stack. Such a vector is associated to each /// state of this stack. /// - emptiness_check* explicit_tau03_opt_search(const tgba *a); + emptiness_check* explicit_tau03_opt_search(const tgba *a, + option_map o = option_map()); /// @} } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d7eb1ac09..260de9426 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -744,6 +744,10 @@ main(int argc, char** argv) assert(!"unknown output option"); } + spot::option_map o; + o.set("poprem", poprem); + o.set("group", couv_group); + spot::emptiness_check* ec = 0; switch (echeck) { @@ -751,11 +755,11 @@ main(int argc, char** argv) break; case Couvreur: - ec = new spot::couvreur99_check(a, poprem); + ec = new spot::couvreur99_check(a, o); break; case Couvreur2: - ec = new spot::couvreur99_check_shy(a, poprem, couv_group); + ec = new spot::couvreur99_check_shy(a, o); break; case MagicSearch: diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 4fa936a64..5caa006bb 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -62,72 +62,41 @@ #include "tgbaalgos/tau03opt.hh" #include "tgbaalgos/replayrun.hh" -spot::option_map options; - spot::emptiness_check* -couvreur99_cons(const spot::tgba* a) +couvreur99_cons(const spot::tgba* a, spot::option_map o) { - return new spot::couvreur99_check(a, false); + return spot::couvreur99(a, o); } spot::emptiness_check* -couvreur99_shy_cons(const spot::tgba* a) +ms_cons(const spot::tgba* a, spot::option_map o) { - return new spot::couvreur99_check_shy(a, false); + return spot::explicit_magic_search(a, o); } spot::emptiness_check* -couvreur99_shy_minus_cons(const spot::tgba* a) +se05_cons(const spot::tgba* a, spot::option_map o) { - return new spot::couvreur99_check_shy(a, false, false); + return spot::explicit_se05_search(a, o); } spot::emptiness_check* -couvreur99_rem_cons(const spot::tgba* a) +bsh_ms_cons(const spot::tgba* a, spot::option_map o) { - return new spot::couvreur99_check(a, true); + return spot::bit_state_hashing_magic_search(a, 4096, o); } spot::emptiness_check* -couvreur99_rem_shy_cons(const spot::tgba* a) +bsh_se05_cons(const spot::tgba* a, spot::option_map o) { - return new spot::couvreur99_check_shy(a, true); -} - -spot::emptiness_check* -couvreur99_rem_shy_minus_cons(const spot::tgba* a) -{ - return new spot::couvreur99_check_shy(a, true, false); -} - -spot::emptiness_check* -ms_cons(const spot::tgba* a) -{ - return spot::explicit_magic_search(a, options); -} - -spot::emptiness_check* -se05_cons(const spot::tgba* a) -{ - return spot::explicit_se05_search(a, options); -} - -spot::emptiness_check* -bsh_ms_cons(const spot::tgba* a) -{ - return spot::bit_state_hashing_magic_search(a, 4096, options); -} - -spot::emptiness_check* -bsh_se05_cons(const spot::tgba* a) -{ - return spot::bit_state_hashing_se05_search(a, 4096, options); + return spot::bit_state_hashing_se05_search(a, 4096, o); } struct ec_algo { const char* name; - spot::emptiness_check* (*construct)(const spot::tgba*); + const char* options; + spot::emptiness_check* (*construct)(const spot::tgba*, spot::option_map o); unsigned int min_acc; unsigned int max_acc; bool safe; @@ -135,29 +104,53 @@ struct ec_algo ec_algo ec_algos[] = { - { "Cou99", couvreur99_cons, 0, -1U, true }, - { "Cou99_shy-", couvreur99_shy_minus_cons, 0, -1U, true }, - { "Cou99_shy", couvreur99_shy_cons, 0, -1U, true }, - { "Cou99_rem", couvreur99_rem_cons, 0, -1U, true }, - { "Cou99_rem_shy-", couvreur99_rem_shy_minus_cons, 0, -1U, true }, - { "Cou99_rem_shy", couvreur99_rem_shy_cons, 0, -1U, true }, - { "CVWY90", ms_cons, 0, 1, true }, - { "CVWY90_bsh", bsh_ms_cons, 0, 1, false }, - { "GV04", spot::explicit_gv04_check, 0, 1, true }, - { "SE05", se05_cons, 0, 1, true }, - { "SE05_bsh", bsh_se05_cons, 0, 1, false }, - { "Tau03", spot::explicit_tau03_search, 1, -1U, true }, - { "Tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true }, + { "Cou99", "poprem=0", + couvreur99_cons, 0, -1U, true }, + { "Cou99_shy-", "poprem=0,shy=1,group=0", + couvreur99_cons, 0, -1U, true }, + { "Cou99_shy", "poprem=0,shy=1,group=1", + couvreur99_cons, 0, -1U, true }, + { "Cou99_rem", "poprem=1", + couvreur99_cons, 0, -1U, true }, + { "Cou99_rem_shy-", "poprem=1,shy=1,group=0", + couvreur99_cons, 0, -1U, true }, + { "Cou99_rem_shy", "poprem=1,shy=1,group=1", + couvreur99_cons, 0, -1U, true }, + { "CVWY90", 0, + ms_cons, 0, 1, true }, + { "CVWY90_bsh", 0, + bsh_ms_cons, 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 }, + { "Tau03", 0, + spot::explicit_tau03_search, 1, -1U, true }, + { "Tau03_opt", 0, + spot::explicit_tau03_opt_search, 0, -1U, true }, }; +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) + { + char* x = strdup(ec_algos[num].options); + const char* err = o.parse_options(x); + assert(!err); + (void)err; + free(x); + } if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc) a = degen; if (a) - return ec_algos[num].construct(a); + return ec_algos[num].construct(a, o); return 0; }