sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Will this ever end? 

Former-commit-id: fbe20506cd
tempestpy_adaptions
dehnert 10 years ago
parent
9547f3a91a
commit
acdced1fee
16 changed files with 375 additions and 328 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 61
      src/settings/InternalSettingsMemento.h
  2. 22
      src/settings/SettingMemento.cpp
  3. 45
      src/settings/SettingMemento.h
  4. 1
      src/settings/SettingsManager.cpp
  5. 299
      src/settings/SettingsManager.h
  6. 46
      src/settings/modules/GeneralSettings.h
  7. 3
      src/settings/modules/GlpkSettings.cpp
  8. 1
      src/settings/modules/GlpkSettings.h
  9. 22
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  10. 20
      src/settings/modules/GmmxxEquationSolverSettings.h
  11. 17
      src/settings/modules/GurobiSettings.cpp
  12. 33
      src/settings/modules/GurobiSettings.h
  13. 8
      src/settings/modules/ModuleSettings.cpp
  14. 53
      src/settings/modules/ModuleSettings.h
  15. 29
      src/settings/modules/NativeEquationSolverSettings.cpp
  16. 43
      src/settings/modules/NativeEquationSolverSettings.h

61
src/settings/InternalSettingsMemento.h
View File

@ -1,61 +0,0 @@
#ifndef STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_
#define STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_
#include "src/settings/SettingsManager.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace settings {
/*!
* NOTE: THIS CLASS IS FOR INTERNAL USE IN THE TESTS ONLY.
*
* If an option is required to be set when executing a test the test may instantiate an object of this class
* while the test itself is executed. This object then ensures that the option has the requested value and
* resets it to its previous value as soon as its destructor is called.
*/
class InternalSettingMemento {
public:
/*!
* Constructs a new memento for the specified option.
*
* @param moduleName The name of the module that registered the option.
* @param longOptionName The long name of the option.
* @param requiredHasBeenSetState A flag that indicates whether the setting is to be temporarily set to
* true or false.
*/
InternalOptionMemento(std::string const& moduleName, std::string const& longOptionName, bool requiredHasBeenSetState): optionName(longOptionName), stateBefore() {
this->stateBefore = storm::settings::SettingsManager::manager().isSet(optionName);
if (requiredHasBeenSetState) {
storm::settings::SettingsManager::manager()..set(optionName);
} else {
storm::settings::SettingsManager::manager().unset(optionName);
}
}
/*!
* Destructs the memento object and resets the value of the option to its original state.
*/
virtual ~InternalOptionMemento() {
if (stateBefore) {
storm::settings::SettingsManager::manager().set(optionName);
} else {
storm::settings::SettingsManager::manager().unset(optionName);
}
}
private:
// The long name of the option that was temporarily set.
std::string const optionName;
// The state of the option before it was set.
bool stateBefore;
};
} // namespace settings
} // namespace storm
#endif // STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_

22
src/settings/SettingMemento.cpp
View File

@ -0,0 +1,22 @@
#include "src/settings/SettingsMemento.h"
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
SettingMemento::SettingMemento(ModuleSettings& settings, std::string const& longOptionName, bool resetToState) : settings(settings), optionName(longOptionName), resetToState(resetToState) {
// Intentionally left empty.
}
/*!
* Destructs the memento object and resets the value of the option to its original state.
*/
virtual SettingMemento::~SettingMemento() {
if (resetToState) {
settings.set(optionName);
} else {
settings.unset(optionName);
}
}
}
}

45
src/settings/SettingMemento.h
View File

@ -0,0 +1,45 @@
#ifndef STORM_SETTINGS_SETTINGMEMENTO_H_
#define STORM_SETTINGS_SETTINGMEMENTO_H_
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
class ModuleSettings;
/*!
* This class is used to reset the state of an option that was temporarily set to a different status.
*/
class SettingMemento {
public:
/*!
* Constructs a new memento for the specified option.
*
* @param settings The settings object in which to restore the state of the option.
* @param longOptionName The long name of the option.
* @param resetToState A flag that indicates the status to which the option is to be reset upon
* deconstruction of this object.
*/
SettingMemento(ModuleSettings& settings, std::string const& longOptionName, bool resetToState);
/*!
* Destructs the memento object and resets the value of the option to its original state.
*/
virtual ~SettingMemento();
private:
// The settings object in which the setting is to be restored.
ModuleSettings& settings;
// The long name of the option that was temporarily set.
std::string const optionName;
// The state of the option before it was set.
bool resetToState;
};
} // namespace settings
} // namespace storm
#endif // STORM_SETTINGS_SETTINGMEMENTO_H_

1
src/settings/SettingsManager.cpp
View File

@ -21,6 +21,7 @@ namespace storm {
return settingsManager;
}
}
}

299
src/settings/SettingsManager.h
View File

@ -4,6 +4,7 @@
#include <iostream>
#include <sstream>
#include <list>
#include <set>
#include <utility>
#include <functional>
#include <unordered_map>
@ -22,7 +23,7 @@
#include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/CounterexampleGeneratorSettings.h"
#include "src/settings/modules/CuddSettings.h"
#include "src/settings/modules/GmmxxSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
@ -31,109 +32,108 @@
#include "src/exceptions/OptionParserException.h"
namespace storm {
namespace settings {
typedef std::pair<std::string, std::string> stringPair_t;
class InternalOptionMemento;
/*!
* @brief Settings class with command line parser and type validation
*
*
* It is meant to be used as a singleton. Call
* @code storm::settings::Settings::getInstance() @endcode
* to initialize it and obtain an instance.
*
* This class can be customized by other parts of the software using
* option modules. An option module can be anything that implements the
* interface specified by registerModule() and does a static initialization call to this function.
* Provides the central API for the registration of command line options and parsing the options from the
* command line. Since this class is a singleton, the only instance is accessible via a call to the manager()
* function.
*/
class SettingsManager {
public:
// Declare the memento class as a friend so it can manipulate the internal state.
friend class InternalOptionMemento;
/*!
* This parses the command line of the application and matches it to all prior registered options
* @throws OptionParserException
*/
static void parse(int const argc, char const * const argv[]);
std::vector<std::shared_ptr<Option>> const& getOptions() const {
return this->optionPointers;
}
// PUBLIC INTERFACE OF OPTIONSACCUMULATOR (now internal)
/*!
* Returns true IFF an option with the specified longName exists.
/*!
* This function parses the given command line arguments and sets all registered options accordingly. If the
* command line cannot be matched using the known options, an exception is thrown.
*
* @param argc The number of command line arguments.
* @param argv The command line arguments.
*/
bool containsOptionByLongName(std::string const& longName) const {
return this->containsLongName(longName);
}
static void setFromCommandLine(int const argc, char const * const argv[]);
/*!
* Returns true IFF an option with the specified shortName exists.
/*!
* This function parses the given command line arguments (represented by one big string) and sets all
* registered options accordingly. If the command line cannot be matched using the known options, an
* exception is thrown.
*
* @param commandLineString The command line arguments as one string.
*/
bool containsOptionByShortName(std::string const& shortName) const {
return this->containsLongName(shortName);
}
static void setFromString(std::string const& commandLineString);
/*!
* Returns a reference to the Option with the specified longName.
* Throws an Exception of Type IllegalArgumentException if there is no such Option.
/*!
* This function parses the given command line arguments (represented by several strings) and sets all
* registered options accordingly. If the command line cannot be matched using the known options, an
* exception is thrown.
*
* @param commandLineArguments The command line arguments.
*/
Option const& getOptionByLongName(std::string const& longName) const {
return this->getByLongName(longName);
}
static void setFromExplodedString(std::vector<std::string> const& commandLineArguments);
/*!
* Returns a reference to the Option with the specified shortName.
* Throws an Exception of Type IllegalArgumentException if there is no such Option.
/*!
* This function parses the given file and sets all registered options accordingly. If the settings cannot
* be matched using the known options, an exception is thrown.
*/
Option const& getOptionByShortName(std::string const& shortName) const {
return this->getByShortName(shortName);
}
/*!
* Adds the given option to the set of known options.
* Unifying with existing options is done automatically.
* Ownership of the Option is handed over when calling this function!
* Returns a reference to the settings instance
* @throws OptionUnificationException
*/
SettingsManager& addOption(Option* option);
/*!
* Returns true iff there is an Option with the specified longName and it has been set
* @return bool true if the option exists and has been set
* @throws InvalidArgumentException
*/
bool isSet(std::string const& longName) const {
return this->getByLongName(longName).getHasOptionBeenSet();
}
/*!
* This generated a list of all registered options and their arguments together with descriptions and defaults.
* @return A std::string containing the help text, delimited by \n
*/
std::string getHelpText() const;
static void setFromConfigurationFile(std::string const& configFilename);
/*!
* Registers a new module with the given name and options. If the module could not be successfully registered,
* an exception is thrown.
* Retrieves the general settings.
*
* @param moduleName The name of the module to register.
* @param options The set of options that the module registers.
* @return An object that allows accessing the general settings.
*/
void registerModule(std::string const& moduleName, std::vector<std::shared_ptr<Option>> const& options);
/*!
* Retrieves the only existing instance of a settings manager.
storm::settings::modules::GeneralSettings const& getGeneralSettings() const;
/*!
* Retrieves the debug settings.
*
* @return The only existing instance of a settings manager
*/
static SettingsManager& manager();
* @return An object that allows accessing the debug settings.
*/
storm::settings::modules::DebugSettings const& getDebugSettings() const;
/*!
* Retrieves the counterexample generator settings.
*
* @return An object that allows accessing the counterexample generator settings.
*/
storm::settings::modules::CounterexampleGeneratorSettings const& getCounterexampleGeneratorSettings() const;
/*!
* Retrieves the CUDD settings.
*
* @return An object that allows accessing the CUDD settings.
*/
storm::settings::modules::CuddSettings const& getCuddSettings() const;
/*!
* Retrieves the settings of the gmm++-based equation solver.
*
* @return An object that allows accessing the settings of the gmm++-based equation solver.
*/
storm::settings::modules::GmmxxEquationSolverSettings const& getGmmxxEquationSolverSettings() const;
/*!
* Retrieves the settings of the native equation solver.
*
* @return An object that allows accessing the settings of the native equation solver.
*/
storm::settings::modules::NativeEquationSolverSettings const& getNativeEquationSolverSettings() const;
/*!
* Retrieves the settings of glpk.
*
* @return An object that allows accessing the settings of glpk.
*/
storm::settings::modules::GlpkSettings const& getGlpkSettings() const;
/*!
* Retrieves the settings of Gurobi.
*
* @return An object that allows accessing the settings of Gurobi.
*/
storm::settings::modules::GurobiSettings const& getGurobiSettings() const;
private:
/*!
@ -160,7 +160,7 @@ namespace storm {
storm::settings::modules::CuddSettings cuddSettings;
// An object that provides access to the gmm++ settings.
storm::settings::modules::GmmxxSettings gmmxxSettings;
storm::settings::modules::GmmxxEquationSolverSettings gmmxxEquationSolverSettings;
// An object that provides access to the native equation solver settings.
storm::settings::modules::NativeEquationSolverSettings nativeEquationSolverSettings;
@ -174,29 +174,38 @@ namespace storm {
// The single instance of the manager class. Since it's static, it will automatically be distructed upon termination.
static SettingsManager settingsManager;
// A set of all known (i.e. registered) module names.
std::set<std::string> moduleNames;
// A mapping from all known option names to the options that match it. All options for one option name need
// to be compatible in the sense that calling isCompatible(...) pairwise on all options must always return true.
std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> options;
/*!
* Parser for the commdand line parameters of the program.
* The first entry of argv will be ignored, as it represents the program name.
* @throws OptionParserException
*/
void parseCommandLine(int const argc, char const * const argv[]);
/*!
* The map holding the information regarding registered options and their types
* This function prints a help message to the standard output. Optionally, a module name can be given. If
* it is present, name must correspond to a known module. Then, only the help text for this module is
* printed.
*
* @return moduleName The name of the module for which to show the help or "all" if the full help text is to
* be printed.
*/
std::unordered_map<std::string, std::shared_ptr<Option>> options;
void printHelp(std::string const& moduleName = "all") const;
/*!
* The vector holding a pointer to all options
/*!
* Registers a new module with the given name and options. If the module could not be successfully registered,
* an exception is thrown.
*
* @param moduleName The name of the module to register.
* @param options The set of options that the module registers.
*/
std::vector<std::shared_ptr<Option>> optionPointers;
void registerModule(std::string const& moduleName, std::vector<std::shared_ptr<Option>> const& options);
/*!
* The map holding the information regarding registered options and their short names
/*!
* Retrieves the only existing instance of a settings manager.
*
* @return The only existing instance of a settings manager
*/
std::unordered_map<std::string, std::string> shortNames;
static SettingsManager& manager();
// Helper functions
stringPair_t splitOptionString(std::string const& option);
@ -205,98 +214,6 @@ namespace storm {
std::vector<std::string> argvToStringArray(int const argc, char const * const argv[]);
std::vector<bool> scanForOptions(std::vector<std::string> const& arguments);
bool checkArgumentSyntaxForOption(std::string const& argvString);
/*!
* Returns true IFF this contains an option with the specified longName.
* @return bool true iff there is an option with the specified longName
*/
bool containsLongName(std::string const& longName) const {
return (this->options.find(longName) != this->options.end());
}
/*!
* Returns true IFF this contains an option with the specified shortName.
* @return bool true iff there is an option with the specified shortName
*/
bool containsShortName(std::string const& shortName) const {
return (this->shortNames.find(shortName) != this->shortNames.end());
}
/*!
* Returns a reference to the Option with the specified longName.
* Throws an Exception of Type InvalidArgumentException if there is no such Option.
* @throws InvalidArgumentException
*/
Option& getByLongName(std::string const& longName) const {
auto longNameIterator = this->options.find(longName);
if (longNameIterator == this->options.end()) {
LOG4CPLUS_ERROR(logger, "Settings::getByLongName: This program does not contain an option named \"" << longName << "\".");
throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
}
return *longNameIterator->second.get();
}
/*!
* Returns a pointer to the Option with the specified longName.
* Throws an Exception of Type InvalidArgumentException if there is no such Option.
* @throws InvalidArgumentException
*/
Option* getPtrByLongName(std::string const& longName) const {
auto longNameIterator = this->options.find(longName);
if (longNameIterator == this->options.end()) {
LOG4CPLUS_ERROR(logger, "Settings::getPtrByLongName: This program does not contain an option named \"" << longName << "\".");
throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
}
return longNameIterator->second.get();
}
/*!
* Returns a reference to the Option with the specified shortName.
* Throws an Exception of Type InvalidArgumentException if there is no such Option.
* @throws InvalidArgumentException
*/
Option& getByShortName(std::string const& shortName) const {
auto shortNameIterator = this->shortNames.find(shortName);
if (shortNameIterator == this->shortNames.end()) {
LOG4CPLUS_ERROR(logger, "Settings::getByShortName: This program does not contain an option named \"" << shortName << "\".");
throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\"";
}
return *(this->options.find(shortNameIterator->second)->second.get());
}
/*!
* Returns a pointer to the Option with the specified shortName.
* Throws an Exception of Type InvalidArgumentException if there is no such Option.
* @throws InvalidArgumentException
*/
Option* getPtrByShortName(std::string const& shortName) const {
auto shortNameIterator = this->shortNames.find(shortName);
if (shortNameIterator == this->shortNames.end()) {
LOG4CPLUS_ERROR(logger, "Settings::getPtrByShortName: This program does not contain an option named \"" << shortName << "\".");
throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\".";
}
return this->options.find(shortNameIterator->second)->second.get();
}
/*!
* Sets the Option with the specified longName
* This function requires the Option to have no arguments
* This is for TESTING only and should not be used outside of the testing code!
* @throws InvalidArgumentException
*/
void set(std::string const& longName) const {
return this->getByLongName(longName).setHasOptionBeenSet();
}
/*!
* Unsets the Option with the specified longName
* This function requires the Option to have no arguments
* This is for TESTING only and should not be used outside of the testing code!
* @throws InvalidArgumentException
*/
void unset(std::string const& longName) const {
return this->getByLongName(longName).setHasOptionBeenSet(false);
}
};
} // namespace settings

46
src/settings/modules/GeneralSettings.h
View File

@ -12,6 +12,12 @@ namespace storm {
*/
class GeneralSettings : public ModuleSettings {
public:
// An enumeration of all available LP solvers.
enum class LpSolver { Gurobi, glpk };
// An enumeration of all available equation solvers.
enum class EquationSolver { Gmmxx, Native };
/*!
* Creates a new set of general settings that is managed by the given manager.
*
@ -216,46 +222,18 @@ namespace storm {
uint_fast64_t getTimeoutInSeconds() const;
/*!
* Retrieves whether the eqsolver option was set.
*
* @return True if the eqsolver option was set.
*/
bool isEqSolverSet() const;
/*!
* Retrieves whether the gmm++ equation solver is to be used.
*
* @return True iff the gmm++ equation solver is to be used.
*/
bool useGmmxxEquationSolver() const;
/*!
* Retrieves whether the native equation solver is to be used.
*
* @return True iff the native equation solver is to be used.
*/
bool useNativeEquationSolver() const;
/*!
* Retrieves whether the lpsolver option was set.
*
* @return True if the lpsolver option was set.
*/
bool isLpSolverSet() const;
/*!
* Retrieves whether glpk is to be used.
* Retrieves the selected equation solver.
*
* @return True iff glpk is to be used.
* @return The selected convergence criterion.
*/
bool useGlpk() const;
EquationSolver getEquationSolver() const;
/*!
* Retrieves whether Gurobi is to be used.
* Retrieves the selected LP solver.
*
* @return True iff Gurobi is to be used.
* @return The selected LP solver.
*/
bool useGurobi() const;
LpSolver getLpSolver() const;
/*!
* Retrieves whether the export-to-dot option was set.

3
src/settings/modules/GlpkSettings.cpp
View File

@ -7,13 +7,14 @@ namespace storm {
namespace modules {
const std::string GlpkSettings::moduleName = "glpk";
const std::string GlpkSettings::integerToleranceOption = "inttol";
const std::string GlpkSettings::outputOptionName = "output";
GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
options.push_back(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
options.push_back(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);
}

1
src/settings/modules/GlpkSettings.h
View File

@ -29,6 +29,7 @@ namespace storm {
private:
// Define the string names of the options as constants.
static const std::string moduleName;
static const std::string integerToleranceOption;
static const std::string outputOptionName;
};

22
src/settings/modules/GmmxxSettings.cpp → src/settings/modules/GmmxxEquationSolverSettings.cpp
View File

@ -1,4 +1,4 @@
#include "src/settings/modules/GmmxxSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/SettingsManager.h"
@ -6,16 +6,16 @@ namespace storm {
namespace settings {
namespace modules {
const std::string GmmxxSettings::moduleName = "gmm++";
const std::string GmmxxSettings::techniqueOptionName = "tech";
const std::string GmmxxSettings::preconditionOptionName = "precond";
const std::string GmmxxSettings::restartOptionName = "restart";
const std::string GmmxxSettings::maximalIterationsOptionName = "maxiter";
const std::string GmmxxSettings::maximalIterationsOptionShortName = "maxiter";
const std::string GmmxxSettings::precisionOptionName = "precision";
const std::string GmmxxSettings::absoluteOptionName = "absolute";
const std::string GmmxxEquationSolverSettings::moduleName = "gmm++";
const std::string GmmxxEquationSolverSettings::techniqueOptionName = "tech";
const std::string GmmxxEquationSolverSettings::preconditionOptionName = "precond";
const std::string GmmxxEquationSolverSettings::restartOptionName = "restart";
const std::string GmmxxEquationSolverSettings::maximalIterationsOptionName = "maxiter";
const std::string GmmxxEquationSolverSettings::maximalIterationsOptionShortName = "i";
const std::string GmmxxEquationSolverSettings::precisionOptionName = "precision";
const std::string GmmxxEquationSolverSettings::absoluteOptionName = "absolute";
GmmxxSettings::GmmxxSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
GmmxxEquationSolverSettings::GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
@ -31,7 +31,7 @@ namespace storm {
options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for deciding convergence.").build());
options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);

20
src/settings/modules/GmmxxSettings.h → src/settings/modules/GmmxxEquationSolverSettings.h
View File

@ -10,7 +10,7 @@ namespace storm {
/*!
* This class represents the settings for gmm++.
*/
class GmmxxSettings : public ModuleSettings {
class GmmxxEquationSolverSettings : public ModuleSettings {
public:
// An enumeration of all available techniques for solving linear equations.
enum class LinearEquationTechnique { Bicgstab, Qmr, Gmres, Jacobi };
@ -18,12 +18,15 @@ namespace storm {
// An enumeration of all available preconditioning techniques.
enum class PreconditioningTechnique { Ilu, Diagonal, Ildlt, None };
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
/*!
* Creates a new set of gmm++ settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
GmmxxSettings(storm::settings::SettingsManager& settingsManager);
GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
@ -61,18 +64,11 @@ namespace storm {
double getPrecision() const;
/*!
* Retrieves whether the absolute error is used for detecting convergence.
*
* @return True iff the absolute error is used convergence detection.
*/
bool useAbsoluteConvergenceCriterion() const;
/*!
* Retrieves whether the relative error is used for detecting convergence.
* Retrieves the selected convergence criterion.
*
* @return True iff the relative error is used convergence detection.
* @return The selected convergence criterion.
*/
bool useRelativeConvergenceCriterion() const;
ConvergenceCriterion getConvergenceCriterion() const;
private:
// Define the string names of the options as constants.

17
src/settings/modules/GurobiSettings.cpp
View File

@ -6,15 +6,22 @@ namespace storm {
namespace settings {
namespace modules {
const std::string GurobiSettings::moduleName = "gurobi";
const std::string GurobiSettings::integerToleranceOption = "inttol";
const std::string GurobiSettings::threadsOption = "threads";
const std::string GurobiSettings::outputOption = "output";
GurobiSettings::GurobiSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "glpkinttol", "", "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
options.push_back(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobithreads", "", "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
options.push_back(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobioutput", "", "If set, the Gurobi output will be printed to the command line.").build());
options.push_back(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobiinttol", "", "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);
}
} // namespace modules

33
src/settings/modules/GurobiSettings.h
View File

@ -12,7 +12,40 @@ namespace storm {
*/
class GurobiSettings : public ModuleSettings {
public:
/*!
* Creates a new set of Gurobi settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
GurobiSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves the integer tolerance to be used.
*
* @return The integer tolerance to be used.
*/
double getIntegerTolerance() const;
/*!
* Retrieves the maximal number of threads Gurobi is allowed to use.
*
* @return The maximally allowed number of threads.
*/
uint_fast64_t getNumberOfThreads() const;
/*!
* Retrieves whether the output option was set.
*
* @return True iff the output option was set.
*/
bool isOutputSet() const;
private:
// Define the string names of the options as constants.
static const std::string moduleName;
static const std::string integerToleranceOption;
static const std::string threadsOption;
static const std::string outputOption;
};
} // namespace modules

8
src/settings/modules/ModuleSettings.cpp
View File

@ -16,6 +16,14 @@ namespace storm {
return this->settingsManager;
}
void ModuleSettings::set(std::string const& name) const {
return this->getOption(longName).setHasOptionBeenSet();
}
void ModuleSettings::unset(std::string const& longName) const {
return this->getOption(longName).setHasOptionBeenSet(false);
}
} // namespace modules
} // namespace settings
} // namespace storm

53
src/settings/modules/ModuleSettings.h
View File

@ -2,6 +2,10 @@
#define STORM_SETTINGS_MODULES_MODULESETTINGS_H_
#include <string>
#include <unordered_map>
#include "src/settings/Option.h"
#include "src/settings/SettingMemento.h"
namespace storm {
namespace settings {
@ -29,6 +33,17 @@ namespace storm {
*/
virtual bool check() const;
/*!
* Sets the option with the given name to the required status. This requires the option to take no
* arguments. As a result, a pointer to an object is returned such that when the object is destroyed
* (i.e. the smart pointer goes out of scope), the option is reset to its original status.
*
* @param name The name of the option to (unset).
* @param requiredStatus The status that is to be set for the option.
* @return A pointer to an object that resets the change upon destruction.
*/
std::unique_ptr<storm::settings::SettingMemento> overrideOption(std::string const& name, bool requiredStatus);
protected:
/*!
* Retrieves the manager responsible for the settings.
@ -37,14 +52,52 @@ namespace storm {
*/
storm::settings::SettingsManager const& getSettingsManager() const;
/*!
* Adds the option with the given long name to the list of options of this module.
*
* @param longName The long name of the option.
* @param option The actual option associated with the given name.
*/
void addOption(std::string const& longName, std::shared_ptr<Option> const& option);
/*!
* Retrieves the option with the given long name. If no such option exists, an exception is thrown.
*
* @param longName The long name of the option to retrieve.
* @return The option associated with the given option name.
*/
Option& getOption(std::string const& longName);
/*!
* Retrieves whether the option with the given name was set.
*
* @param The name of the option.
* @return True iff the option was set.
*/
bool isSet(std::string const& optionName) const;
/*!
* Sets the option with the specified name. This requires the option to not have any arguments. This
* should be used with care and is primarily meant to be used by the SettingMemento.
*
* @param name The name of the option to set.
*/
void set(std::string const& name) const;
/*!
* Unsets the option with the specified name. This requires the option to not have any arguments. This
* should be used with care and is primarily meant to be used by the SettingMemento.
*
* @param name The name of the option to unset.
*/
void unset(std::string const& longName) const;
private:
// The settings manager responsible for the settings.
storm::settings::SettingsManager const& settingsManager;
// A mapping of option names of the module to the actual options.
std::unordered_map<std::string, std::shared_ptr<Option>> options;
};
} // namespace modules

29
src/settings/modules/NativeEquationSolverSettings.cpp
View File

@ -6,24 +6,27 @@ namespace storm {
namespace settings {
namespace modules {
const std::string NativeEquationSolverSettings::moduleName = "native";
const std::string NativeEquationSolverSettings::techniqueOptionName = "tech";
const std::string NativeEquationSolverSettings::maximalIterationsOptionName = "maxiter";
const std::string NativeEquationSolverSettings::maximalIterationsOptionShortName = "i";
const std::string NativeEquationSolverSettings::precisionOptionName = "precision";
const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute";
NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// Offer all available methods as a command line option.
std::vector<std::string> methods;
methods.clear();
methods.push_back("jacobi");
settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "nativelin", "", "The method to be used for solving linear equation systems with the native engine. Available are: jacobi.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
std::vector<std::string> methods = { "jacobi" };
options.push_back(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
options.push_back(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);
}
} // namespace modules

43
src/settings/modules/NativeEquationSolverSettings.h
View File

@ -12,7 +12,50 @@ namespace storm {
*/
class NativeEquationSolverSettings : public ModuleSettings {
public:
// An enumeration of all available techniques for solving linear equations.
enum class LinearEquationTechnique { Jacobi };
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
*
* @return The technique to use.
*/
LinearEquationTechnique getLinearEquationSystemTechnique() const;
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
* @return The maximal iteration count.
*/
uint_fast64_t getMaximalIterationCount() const;
/*!
* Retrieves the precision that is used for detecting convergence.
*
* @return The precision to use for detecting convergence.
*/
double getPrecision() const;
/*!
* Retrieves the selected convergence criterion.
*
* @return The selected convergence criterion.
*/
ConvergenceCriterion getConvergenceCriterion() const;
private:
// Define the string names of the options as constants.
static const std::string moduleName;
static const std::string techniqueOptionName;
static const std::string maximalIterationsOptionName;
static const std::string maximalIterationsOptionShortName;
static const std::string precisionOptionName;
static const std::string absoluteOptionName;
};
} // namespace modules

Write Preview
Loading…
Cancel
Save