diff --git a/ChangeLog b/ChangeLog index 218e651a9..a0b38cefa 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2005-02-07 Denis Poitrenaud + + * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map): New class. + * src/misc/Makefile.am: Add it. + * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: Add option + facilities to the classes emptiness_check and emptiness_result + * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, + src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh: Compute optionnaly + accepting runs from stack. + * src/tgbatest/randtgba.cc: Make this option public. + 2005-02-05 Alexandre Duret-Lutz * src/misc/ltstr.hh: Include diff --git a/INSTALL b/INSTALL index 095b1eb40..54caf7c19 100644 --- a/INSTALL +++ b/INSTALL @@ -1,16 +1,13 @@ -Installation Instructions -************************* +Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software +Foundation, Inc. -Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002, 2004 Free -Software Foundation, Inc. - -This file is free documentation; the Free Software Foundation gives + 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 @@ -70,9 +67,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 @@ -85,7 +82,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 @@ -102,19 +99,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=PREFIX'. +option `--prefix=PATH'. You can specify separate installation prefixes for architecture-specific files and architecture-independent files. If you -give `configure' the option `--exec-prefix=PREFIX', the package will -use PREFIX as the prefix for installing programs and libraries. +give `configure' the option `--exec-prefix=PATH', the package will use +PATH 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=DIR' to specify different values for particular +options like `--bindir=PATH' 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. @@ -125,7 +122,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 @@ -140,11 +137,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: @@ -170,9 +167,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. @@ -181,7 +178,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 @@ -195,7 +192,8 @@ overridden in the site shell script). `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/lbtt/INSTALL b/lbtt/INSTALL index 095b1eb40..54caf7c19 100644 --- a/lbtt/INSTALL +++ b/lbtt/INSTALL @@ -1,16 +1,13 @@ -Installation Instructions -************************* +Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software +Foundation, Inc. -Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002, 2004 Free -Software Foundation, Inc. - -This file is free documentation; the Free Software Foundation gives + 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 @@ -70,9 +67,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 @@ -85,7 +82,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 @@ -102,19 +99,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=PREFIX'. +option `--prefix=PATH'. You can specify separate installation prefixes for architecture-specific files and architecture-independent files. If you -give `configure' the option `--exec-prefix=PREFIX', the package will -use PREFIX as the prefix for installing programs and libraries. +give `configure' the option `--exec-prefix=PATH', the package will use +PATH 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=DIR' to specify different values for particular +options like `--bindir=PATH' 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. @@ -125,7 +122,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 @@ -140,11 +137,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: @@ -170,9 +167,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. @@ -181,7 +178,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 @@ -195,7 +192,8 @@ overridden in the site shell script). `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/Makefile.am b/src/misc/Makefile.am index 40ff214ae..0e78e6567 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -35,6 +35,7 @@ misc_HEADERS = \ ltstr.hh \ minato.hh \ modgray.hh \ + optionmap.hh \ random.hh \ timer.hh \ version.hh @@ -47,6 +48,7 @@ libmisc_la_SOURCES = \ freelist.cc \ minato.cc \ modgray.cc \ + optionmap.cc \ random.cc \ timer.cc \ version.cc diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc new file mode 100644 index 000000000..78cb7ff81 --- /dev/null +++ b/src/misc/optionmap.cc @@ -0,0 +1,102 @@ +// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include "optionmap.hh" + +namespace spot +{ + namespace { + bool + to_int(const char* s, int &i) + { + char* endptr; + int res = strtol(s, &endptr, 10); + if (*endptr) + { + std::cerr << "Failed to parse `" << s << "' as an integer." + << std::endl; + return false; + } + i = res; + return true; + } + }; + + 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; + } + + int option_map::get(const char* option) const + { + std::map::const_iterator it = options_.find(option); + if (it == options_.end()) + // default value if not declared + return 0; + else + return it->second; + } + + int option_map::operator[](const char* option) const + { + return get(option); + } + + int option_map::set(const char* option, int val) + { + int old = get(option); + options_[option] = val; + return old; + } + + int& option_map::operator[](const char* option) + { + return options_[option]; + } + + std::ostream& operator<<(std::ostream& os, const option_map& m) + { + for (std::map::const_iterator it = m.options_.begin(); + 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 new file mode 100644 index 000000000..ef27573a3 --- /dev/null +++ b/src/misc/optionmap.hh @@ -0,0 +1,74 @@ +// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_MISC_OPTION_MAP_HH +# define SPOT_MISC_OPTION_MAP_HH + +#include +#include +#include + +namespace spot +{ + /// \brief Manage a map of options. + /// \ingroup misc_tools + /// Each option is defined by a string and is associated to an integer value. + class option_map + { + public: + /// \brief Add the parsed options to the map. + /// + /// \a options are separated by a space, comma, semicolon or tabulation and + /// can be optionnaly followed by an integer value (preceded by an equal + /// sign). If not specified, the default value is 1. + /// + /// \return A non-null pointer to the option for which an expected integer + /// value cannot be parsed. + const char* parse_options(char* options); + + /// \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; + + /// \brief Get the value of \a option. + /// + /// \return The value associated to \a option if it exists, 0 otherwise. + 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); + + /// \brief Get a reference to the current value of \a option. + int& operator[](const char* option); + + /// \brief Print the option_map \a m. + friend std::ostream& operator<<(std::ostream& os, const option_map& m); + + private: + std::map options_; + }; +}; + +#endif diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 71f68a095..b9870fbeb 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -27,7 +27,6 @@ namespace spot { - tgba_run::~tgba_run() { for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i) diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 6d7ca0487..996e6c387 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -22,9 +22,11 @@ #ifndef SPOT_TGBAALGOS_EMPTINESS_HH # define SPOT_TGBAALGOS_EMPTINESS_HH +#include #include #include #include +#include "misc/optionmap.hh" #include "tgba/state.hh" #include "emptiness_stats.hh" @@ -74,8 +76,13 @@ namespace spot class emptiness_check_result { public: - emptiness_check_result(const tgba* a) - : a_(a) + emptiness_check_result(const tgba* a, option_map o = option_map()) + : a_(a), o_(o) + { + } + + virtual + ~emptiness_check_result() { } @@ -100,19 +107,43 @@ namespace spot return a_; } + /// Return the options parametrizing how the accepting run is computed. + const option_map& + options() const + { + 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; + } + /// 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; + } + const tgba* a_; ///< The automaton. + option_map o_; ///< The options }; /// Common interface to emptiness check algorithms. class emptiness_check { public: - emptiness_check(const tgba* a) - : a_(a) + emptiness_check(const tgba* a, option_map o = option_map()) + : a_(a), o_(o) { } virtual ~emptiness_check(); @@ -124,6 +155,23 @@ namespace spot return a_; } + /// Return the options parametrizing how the emptiness check is realized. + const option_map& + options() const + { + 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; + } + /// \brief Check whether the automaton contain an accepting run. /// /// Return 0 if the automaton accept no run. Return an instance @@ -142,8 +190,15 @@ 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; + } + protected: const tgba* a_; ///< The automaton. + option_map o_; ///< The options }; /// @} diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 5115f8ca2..108779564 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -53,8 +53,8 @@ namespace spot /// /// \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) - : emptiness_check(a), + 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()) { @@ -96,17 +96,17 @@ namespace spot h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new ndfs_result, heap>(*this); + return new magic_search_result(*this, options()); } else { h.pop_notify(st_red.front().s); pop(st_red); if (!st_red.empty() && dfs_red()) - return new ndfs_result, heap>(*this); + return new magic_search_result(*this, options()); else if (dfs_blue()) - return new ndfs_result, heap>(*this); + return new magic_search_result(*this, options()); } return 0; } @@ -314,6 +314,108 @@ namespace spot return false; } + class result_from_stack: public emptiness_check_result, + public acss_statistics + { + public: + result_from_stack(magic_search& ms) + : emptiness_check_result(ms.automaton()), ms_(ms) + { + } + + virtual tgba_run* accepting_run() + { + assert(!ms_.st_blue.empty()); + assert(!ms_.st_red.empty()); + + tgba_run* run = new tgba_run; + + typename stack_type::const_reverse_iterator i, j, end; + tgba_run::steps* l; + + l = &run->prefix; + + i = ms_.st_blue.rbegin(); + end = ms_.st_blue.rend(); --end; + j = i; ++j; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + l = &run->cycle; + + j = ms_.st_red.rbegin(); + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + + i = j; ++j; + end = ms_.st_red.rend(); --end; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + return run; + } + + unsigned acss_states() const + { + return 0; + } + private: + magic_search& ms_; + }; + +# define FROM_STACK "ar:from_stack" + + class magic_search_result: public emptiness_check_result + { + public: + 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); + } + + virtual void options_updated(const option_map& old) + { + if (old[FROM_STACK] && !options()[FROM_STACK]) + { + delete computer; + computer = new ndfs_result, heap>(ms); + } + else if (!old[FROM_STACK] && options()[FROM_STACK]) + { + delete computer; + computer = new result_from_stack(ms); + } + } + + virtual ~magic_search_result() + { + delete computer; + } + + virtual tgba_run* accepting_run() + { + return computer->accepting_run(); + } + + virtual const unsigned_statistics* statistics() const + { + return computer->statistics(); + } + + private: + emptiness_check_result* computer; + magic_search& ms; + }; }; class explicit_magic_search_heap @@ -471,15 +573,15 @@ namespace spot } // anonymous - emptiness_check* explicit_magic_search(const tgba *a) + emptiness_check* explicit_magic_search(const tgba *a, option_map o) { - return new magic_search(a, 0); + return new magic_search(a, 0, o); } - emptiness_check* bit_state_hashing_magic_search( - const tgba *a, size_t size) + emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size, + option_map o) { - return new magic_search(a, size); + return new magic_search(a, size, o); } } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 769d4de73..be6e44187 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -23,6 +23,7 @@ # define SPOT_TGBAALGOS_MAGIC_HH #include +#include "misc/optionmap.hh" namespace spot { @@ -93,7 +94,8 @@ namespace spot /// } /// \endverbatim /// - emptiness_check* explicit_magic_search(const tgba *a); + emptiness_check* explicit_magic_search(const tgba *a, + option_map o = option_map()); /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// @@ -113,13 +115,17 @@ namespace spot /// } /// \endverbatim /// - /// Consequently, the detection of an acceptence cycle is not ensured. The - /// implemented algorithm is the same as the one of + /// Consequently, the detection of an acceptence cycle is not ensured. + /// + /// The size of the heap is limited to \n size bytes. + /// + /// The implemented algorithm is the same as the one of /// spot::explicit_magic_search. /// /// \sa spot::explicit_magic_search /// - emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size); + emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size, + option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 9e2a3cc87..059855d44 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -37,8 +37,6 @@ #include "se05.hh" #include "ndfs_result.hxx" -/// FIXME: make compiling depedent the taking into account of weights. - namespace spot { namespace @@ -55,9 +53,8 @@ namespace spot /// /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). - se05_search(const tgba *a, size_t size) - : emptiness_check(a), - ec_statistics(), + se05_search(const tgba *a, size_t size, option_map o = option_map()) + : emptiness_check(a, o), h(size), all_cond(a->all_acceptance_conditions()) { @@ -99,17 +96,17 @@ namespace spot h.add_new_state(s0, CYAN); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new ndfs_result, heap>(*this); + return new se05_result(*this, options()); } else { h.pop_notify(st_red.front().s); pop(st_red); if (!st_red.empty() && dfs_red()) - return new ndfs_result, heap>(*this); + return new se05_result(*this, options()); else if (dfs_blue()) - return new ndfs_result, heap>(*this); + return new se05_result(*this, options()); } return 0; } @@ -322,6 +319,114 @@ namespace spot return false; } + class result_from_stack: public emptiness_check_result, + public acss_statistics + { + public: + result_from_stack(se05_search& ms) + : emptiness_check_result(ms.automaton()), ms_(ms) + { + } + + virtual tgba_run* accepting_run() + { + assert(!ms_.st_blue.empty()); + assert(!ms_.st_red.empty()); + + tgba_run* run = new tgba_run; + + typename stack_type::const_reverse_iterator i, j, end; + tgba_run::steps* l; + + const state* target = ms_.st_red.front().s; + + l = &run->prefix; + + i = ms_.st_blue.rbegin(); + end = ms_.st_blue.rend(); --end; + j = i; ++j; + for (; i != end; ++i, ++j) + { + if (l == &run->prefix && i->s->compare(target) == 0) + l = &run->cycle; + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + if (l == &run->prefix && i->s->compare(target) == 0) + l = &run->cycle; + assert(l == &run->cycle); + + j = ms_.st_red.rbegin(); + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + + i = j; ++j; + end = ms_.st_red.rend(); --end; + for (; i != end; ++i, ++j) + { + tgba_run::step s = { i->s->clone(), j->label, j->acc }; + l->push_back(s); + } + + return run; + } + + unsigned acss_states() const + { + return 0; + } + private: + se05_search& ms_; + }; + +# define FROM_STACK "ar:from_stack" + + class se05_result: public emptiness_check_result + { + public: + se05_result(se05_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); + } + + virtual void options_updated(const option_map& old) + { + if (old[FROM_STACK] && !options()[FROM_STACK]) + { + delete computer; + computer = new ndfs_result, heap>(ms); + } + else if (!old[FROM_STACK] && options()[FROM_STACK]) + { + delete computer; + computer = new result_from_stack(ms); + } + } + + virtual ~se05_result() + { + delete computer; + } + + virtual tgba_run* accepting_run() + { + return computer->accepting_run(); + } + + virtual const unsigned_statistics* statistics() const + { + return computer->statistics(); + } + + private: + emptiness_check_result* computer; + se05_search& ms; + }; }; class explicit_se05_search_heap @@ -559,14 +664,15 @@ namespace spot } // anonymous - emptiness_check* explicit_se05_search(const tgba *a) + emptiness_check* explicit_se05_search(const tgba *a, option_map o) { - return new se05_search(a, 0); + return new se05_search(a, 0, o); } - emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size) + emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size, + option_map o) { - return new se05_search(a, size); + return new se05_search(a, size, o); } } diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index 6ff2dd1cd..5f19ce139 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -23,6 +23,7 @@ # define SPOT_TGBAALGOS_SE05_HH #include +#include "misc/optionmap.hh" namespace spot { @@ -100,8 +101,8 @@ namespace spot /// /// \sa spot::explicit_magic_search /// - emptiness_check* explicit_se05_search(const tgba *a); - + emptiness_check* explicit_se05_search(const tgba *a, + option_map o = option_map()); /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// /// \pre The automaton \a a must have at most one accepting condition (i.e. @@ -120,13 +121,17 @@ namespace spot /// } /// \endverbatim /// - /// Consequently, the detection of an acceptence cycle is not ensured. The - /// implemented algorithm is the same as the one of + /// Consequently, the detection of an acceptence cycle is not ensured. + /// + /// The size of the heap is limited to \n size bytes. + /// + /// The implemented algorithm is the same as the one of /// spot::explicit_se05_search. /// /// \sa spot::explicit_se05_search /// - emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size); + emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size, + option_map o = option_map()); /// @} } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 5012c05fc..af325c55f 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -44,6 +44,7 @@ #include "tgbaalgos/dotty.hh" #include "tgbaparse/public.hh" #include "misc/random.hh" +#include "misc/optionmap.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbaproduct.hh" #include "misc/timer.hh" @@ -61,6 +62,7 @@ #include "tgbaalgos/tau03opt.hh" #include "tgbaalgos/replayrun.hh" +spot::option_map options; spot::emptiness_check* couvreur99_cons(const spot::tgba* a) @@ -98,16 +100,28 @@ 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); + 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); + return spot::bit_state_hashing_se05_search(a, 4096, options); } struct ec_algo @@ -127,10 +141,10 @@ ec_algo ec_algos[] = { "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", spot::explicit_magic_search, 0, 1, true }, + { "CVWY90", ms_cons, 0, 1, true }, { "CVWY90_bsh", bsh_ms_cons, 0, 1, false }, { "GV04", spot::explicit_gv04_check, 0, 1, true }, - { "SE05", spot::explicit_se05_search, 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 }, @@ -196,8 +210,10 @@ syntax(char* prog) << " -O ALGO run Only ALGO" << std::endl << " -R N repeat each emptiness-check and accepting run " << "computation N times" << std::endl - << " -r compute and replay acceptance runs (implies -e)" + << " -r compute and replay accepting runs (implies -e)" << std::endl + << " ar:MODE select the mode MODE for accepting runs computation " + << "(implies -r)" << std::endl << std::endl << "Where:" << std::endl << " F are floats between 0.0 and 1.0 inclusive" << std::endl @@ -945,6 +961,15 @@ main(int argc, char** argv) opt_n_acc = to_int_nonneg(argv[++argn], "-a"); opt_a = to_float_nonneg(argv[++argn], "-a"); } + else if (!strncmp(argv[argn], "ar:", 3)) + { + if (options.parse_options(argv[argn])) + { + std::cerr << "Failed to parse " << argv[argn] << std::endl; + exit(2); + } + + } else if (!strcmp(argv[argn], "-d")) { if (argc < argn + 2)