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

Further refactoring of settings classes. 

Former-commit-id: ed79d0fa4a
tempestpy_adaptions
dehnert 10 years ago
parent
9ad12616e2
commit
ff50fbe12d
20 changed files with 475 additions and 151 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. 11
      src/settings/SettingsManager.cpp
  2. 165
      src/settings/SettingsManager.h
  3. 23
      src/settings/modules/CounterexampleGeneratorSettings.cpp
  4. 22
      src/settings/modules/CounterexampleGeneratorSettings.h
  5. 40
      src/settings/modules/CuddSettings.cpp
  6. 22
      src/settings/modules/CuddSettings.h
  7. 18
      src/settings/modules/DebugSettings.cpp
  8. 22
      src/settings/modules/DebugSettings.h
  9. 48
      src/settings/modules/GeneralSettings.cpp
  10. 10
      src/settings/modules/GeneralSettings.h
  11. 15
      src/settings/modules/GlpkSettings.cpp
  12. 22
      src/settings/modules/GlpkSettings.h
  13. 47
      src/settings/modules/GmmxxSettings.cpp
  14. 22
      src/settings/modules/GmmxxSettings.h
  15. 22
      src/settings/modules/GurobiSettings.cpp
  16. 22
      src/settings/modules/GurobiSettings.h
  17. 6
      src/settings/modules/ModuleSettings.cpp
  18. 36
      src/settings/modules/ModuleSettings.h
  19. 31
      src/settings/modules/NativeEquationSolver.cpp
  20. 22
      src/settings/modules/NativeEquationSolverSettings.h

11
src/settings/SettingsManager.cpp
View File

@ -9,6 +9,17 @@
// Static Inits
storm::settings::Destroyer storm::settings::SettingsManager::destroyer;
namespace storm {
namespace settings {
SettingsManager::SettingsManager() : generalSettings(*this), debugSettings(*this), counterexampleGeneratorSettings(*this), cuddSettings(*this), gmmxxSettings(*this), nativeEquationSolverSettings(*this), glpkSettings(*this), gurobiSettings(*this) {
// Intentionally left empty.
}
}
}
/*!
* @brief Create new instance.
*

165
src/settings/SettingsManager.h
View File

@ -18,6 +18,15 @@
#include "src/settings/ArgumentBuilder.h"
#include "src/settings/ArgumentType.h"
#include "src/settings/ArgumentTypeInferationHelper.h"
#include "src/settings/modules/ModuleSettings.h"
#include "src/settings/modules/GeneralSettings.h"
#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/NativeEquationSolverSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
// Exceptions that should be catched when performing a parsing run
#include "src/exceptions/OptionParserException.h"
@ -140,152 +149,7 @@ namespace settings {
* an instance manually, one should always use the
* newInstance() method.
*/
SettingsManager() {
this->addOption(storm::settings::OptionBuilder("StoRM Main", "help", "h", "Shows all available options, arguments and descriptions.").build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "verbose", "v", "Be verbose.").build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "debug", "", "Be very verbose (intended for debugging).").build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts).").build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the file to write to.").build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "exportdot", "", "If specified, the loaded model will be written to the specified file in the dot format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("dotFileName", "The file to export the model to.").build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the file from which to read.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from transition- and labeling files.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the file from which to read the labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given symbolic model file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("symbolicFileName", "The path and name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Performs model checking for the PRCTL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The file from which to read the PRCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Performs model checking for the CSL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Performs model checking for the LTL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given PRCTL formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("outputPath", "The path to the directory to write the generated counterexample files to.").build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the transition rewards are read from this file and added to the explicit model. Note that this requires an explicit model.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the state rewards are read from this file and added to the explicit model. Note that this requires an explicit model.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "If the model contains deadlock states, setting this option will insert self-loops for these states.").build());
this->addOption(storm::settings::OptionBuilder("StoRM Main", "timeout", "t", "If specified, computation will abort after the given number of seconds.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("seconds", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
std::vector<std::string> linearEquationSolver;
linearEquationSolver.push_back("gmm++");
linearEquationSolver.push_back("native");
this->addOption(storm::settings::OptionBuilder("StoRM Main", "linsolver", "", "Sets which solver is preferred for solving systems of linear equations.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
std::vector<std::string> nondeterministicLinearEquationSolver;
nondeterministicLinearEquationSolver.push_back("gmm++");
nondeterministicLinearEquationSolver.push_back("native");
this->addOption(storm::settings::OptionBuilder("StoRM Main", "ndsolver", "", "Sets which solver is preferred for solving systems of linear equations arising from nondeterministic systems.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nondeterministicLinearEquationSolver)).setDefaultValueString("native").build()).build());
std::vector<std::string> lpSolvers;
lpSolvers.push_back("gurobi");
lpSolvers.push_back("glpk");
this->addOption(storm::settings::OptionBuilder("StoRM Main", "lpsolver", "", "Sets which LP solver is preferred.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("LP solver name", "The name of an available LP solver. Valid values are gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
this->addOption(storm::settings::OptionBuilder("ExplicitModelAdapter", "constants", "", "Specifies the constant replacements to use in Explicit Models").addArgument(storm::settings::ArgumentBuilder::createStringArgument("constantString", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3").setDefaultValueString("").build()).build());
std::vector<std::string> techniques;
techniques.push_back("sat");
techniques.push_back("milp");
this->addOption(storm::settings::OptionBuilder("Counterexample", "mincmd", "", "Computes a counterexample for the given symbolic model in terms of a minimal command set.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("propertyFile", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Must be either \"milp\" or \"sat\".").setDefaultValueString("sat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
this->addOption(storm::settings::OptionBuilder("Counterexample", "stats", "s", "Sets whether to display statistics for certain functionalities.").build());
this->addOption(storm::settings::OptionBuilder("Counterexample", "encreach", "", "Sets whether to encode reachability for SAT-based minimal command counterexample generation.").build());
this->addOption(storm::settings::OptionBuilder("Counterexample", "schedcuts", "", "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder("GlpkLpSolver", "glpkoutput", "", "If set, the glpk output will be printed to the command line.").build());
this->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());
// Offer all available methods as a command line option.
std::vector<std::string> methods;
methods.push_back("bicgstab");
methods.push_back("qmr");
methods.push_back("gmres");
methods.push_back("jacobi");
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmlin", "", "The method to be used for solving linear equation systems with the gmm++ engine. Available are: bicgstab, qmr, gmres, jacobi.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
// Register available preconditioners.
std::vector<std::string> preconditioner;
preconditioner.push_back("ilu");
preconditioner.push_back("diagonal");
preconditioner.push_back("ildlt");
preconditioner.push_back("none");
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmpre", "", "The preconditioning technique used for solving linear equation systems with the gmm++ engine. Available are: ilu, diagonal, none.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmrestart", "", "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "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());
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "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());
this->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
this->addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "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());
this->addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-6).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
this->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());
this->addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobioutput", "", "If set, the Gurobi output will be printed to the command line.").build());
this->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());
// Offer all available methods as a command line option.
methods.clear();
methods.push_back("jacobi");
this->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());
this->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());
this->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());
this->addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
this->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());
this->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());
this->addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
// Set up options for precision and maximal memory available to Cudd.
this->addOption(storm::settings::OptionBuilder("Cudd", "cuddprec", "", "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder("Cudd", "cuddmaxmem", "", "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
// Set up option for reordering.
std::vector<std::string> reorderingTechniques;
reorderingTechniques.push_back("none");
reorderingTechniques.push_back("random");
reorderingTechniques.push_back("randompivot");
reorderingTechniques.push_back("sift");
reorderingTechniques.push_back("siftconv");
reorderingTechniques.push_back("ssift");
reorderingTechniques.push_back("ssiftconv");
reorderingTechniques.push_back("gsift");
reorderingTechniques.push_back("gsiftconv");
reorderingTechniques.push_back("win2");
reorderingTechniques.push_back("win2conv");
reorderingTechniques.push_back("win3");
reorderingTechniques.push_back("win3conv");
reorderingTechniques.push_back("win4");
reorderingTechniques.push_back("win4conv");
reorderingTechniques.push_back("annealing");
reorderingTechniques.push_back("genetic");
reorderingTechniques.push_back("exact");
this->addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"random\", \"randompivot\", \"sift\", \"siftconv\", \"ssift\", \"ssiftconv\", \"gsift\", \"gsiftconv\", \"win2\", \"win2conv\", \"win3\", \"win3conv\", \"win4\", \"win4conv\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
}
SettingsManager();
/*!
* @brief Private destructor.
@ -319,6 +183,15 @@ namespace settings {
*/
std::unordered_map<std::string, std::string> shortNames;
storm::settings::modules::GeneralSettings generalSettings;
storm::settings::modules::DebugSettings debugSettings;
storm::settings::modules::CounterexampleGeneratorSettings counterexampleGeneratorSettings;
storm::settings::modules::CuddSettings cuddSettings;
storm::settings::modules::GmmxxSettings gmmxxSettings;
storm::settings::modules::NativeEquationSolverSettings nativeEquationSolverSettings;
storm::settings::modules::GlpkSettings glpkSettings;
storm::settings::modules::GurobiSettings gurobiSettings;
/*!
* @brief Destroyer object.
*/

23
src/settings/modules/CounterexampleGeneratorSettings.cpp
View File

@ -0,0 +1,23 @@
#include "src/settings/modules/CounterexampleGeneratorSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
std::vector<std::string> techniques;
techniques.push_back("sat");
techniques.push_back("milp");
settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "mincmd", "", "Computes a counterexample for the given symbolic model in terms of a minimal command set.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("propertyFile", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Must be either \"milp\" or \"sat\".").setDefaultValueString("sat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "stats", "", "Sets whether to display statistics for certain functionalities.").build());
settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "encreach", "", "Sets whether to encode reachability for SAT-based minimal command counterexample generation.").build());
settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "schedcuts", "", "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
}
} // namespace modules
} // namespace settings
} // namespace storm

22
src/settings/modules/CounterexampleGeneratorSettings.h
View File

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_
#define STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for counterexample generation.
*/
class CounterexampleGeneratorSettings : public ModuleSettings {
public:
CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_ */

40
src/settings/modules/CuddSettings.cpp
View File

@ -0,0 +1,40 @@
#include "src/settings/modules/CuddSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// Set up options for precision and maximal memory available to Cudd.
settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "cuddprec", "", "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "cuddmaxmem", "", "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
// Set up option for reordering.
std::vector<std::string> reorderingTechniques;
reorderingTechniques.push_back("none");
reorderingTechniques.push_back("random");
reorderingTechniques.push_back("randompivot");
reorderingTechniques.push_back("sift");
reorderingTechniques.push_back("siftconv");
reorderingTechniques.push_back("ssift");
reorderingTechniques.push_back("ssiftconv");
reorderingTechniques.push_back("gsift");
reorderingTechniques.push_back("gsiftconv");
reorderingTechniques.push_back("win2");
reorderingTechniques.push_back("win2conv");
reorderingTechniques.push_back("win3");
reorderingTechniques.push_back("win3conv");
reorderingTechniques.push_back("win4");
reorderingTechniques.push_back("win4conv");
reorderingTechniques.push_back("annealing");
reorderingTechniques.push_back("genetic");
reorderingTechniques.push_back("exact");
settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"random\", \"randompivot\", \"sift\", \"siftconv\", \"ssift\", \"ssiftconv\", \"gsift\", \"gsiftconv\", \"win2\", \"win2conv\", \"win3\", \"win3conv\", \"win4\", \"win4conv\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
}
} // namespace modules
} // namespace settings
} // namespace storm

22
src/settings/modules/CuddSettings.h
View File

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_CUDDSETTINGS_H_
#define STORM_SETTINGS_MODULES_CUDDSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for CUDD.
*/
class CuddSettings : public ModuleSettings {
public:
CuddSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_CUDDSETTINGS_H_ */

18
src/settings/modules/DebugSettings.cpp
View File

@ -0,0 +1,18 @@
#include "src/settings/modules/DebugSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
settingsManager.addOption(storm::settings::OptionBuilder("debug", "debug", "", "Be very verbose (intended for debugging).").build());
settingsManager.addOption(storm::settings::OptionBuilder("debug", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts).").build());
settingsManager.addOption(storm::settings::OptionBuilder("debug", "logfile", "l", "If specified, the log output will also be written to this file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the file to write to.").build()).build());
}
} // namespace modules
} // namespace settings
} // namespace storm

22
src/settings/modules/DebugSettings.h
View File

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_DEBUGSETTINGS_H_
#define STORM_SETTINGS_MODULES_DEBUGSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the debug settings.
*/
class DebugSettings : public ModuleSettings {
public:
DebugSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_DEBUGSETTINGS_H_ */

48
src/settings/modules/GeneralSettings.cpp
View File

@ -1,11 +1,59 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
settingsManager.addOption(storm::settings::OptionBuilder("general", "help", "h", "Shows all available options, arguments and descriptions.").build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "verbose", "v", "Be verbose.").build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "exportdot", "", "If specified, the loaded model will be written to the specified file in the dot format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("dotFileName", "The file to export the model to.").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "config", "c", "If specified, this file will be read and parsed for additional configuration settings.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the file from which to read.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "explicit", "e", "Explicit parsing from transition- and labeling files.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the file from which to read the labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "symbolic", "s", "Parse the given symbolic model file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("symbolicFileName", "The path and name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "prctl", "", "Performs model checking for the PRCTL formulas given in the file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The file from which to read the PRCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "csl", "", "Performs model checking for the CSL formulas given in the file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "ltl", "", "Performs model checking for the LTL formulas given in the file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "counterExample", "", "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("outputPath", "The path to the directory to write the generated counterexample files to.").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "transitionRewards", "", "If specified, the transition rewards are read from this file and added to the explicit model. Note that this requires an explicit model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "stateRewards", "", "If specified, the state rewards are read from this file and added to the explicit model. Note that this requires an explicit model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "fixDeadlocks", "", "If the model contains deadlock states, setting this option will insert self-loops for these states.").build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "timeout", "t", "If specified, computation will abort after the given number of seconds.")
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("seconds", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
std::vector<std::string> linearEquationSolver;
linearEquationSolver.push_back("gmm++");
linearEquationSolver.push_back("native");
settingsManager.addOption(storm::settings::OptionBuilder("general", "linsolver", "", "Sets which solver is preferred for solving systems of linear equations.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
std::vector<std::string> nondeterministicLinearEquationSolver;
nondeterministicLinearEquationSolver.push_back("gmm++");
nondeterministicLinearEquationSolver.push_back("native");
settingsManager.addOption(storm::settings::OptionBuilder("general", "ndsolver", "", "Sets which solver is preferred for solving systems of linear equations arising from nondeterministic systems.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nondeterministicLinearEquationSolver)).setDefaultValueString("native").build()).build());
std::vector<std::string> lpSolvers;
lpSolvers.push_back("gurobi");
lpSolvers.push_back("glpk");
settingsManager.addOption(storm::settings::OptionBuilder("general", "lpsolver", "", "Sets which LP solver is preferred.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("LP solver name", "The name of an available LP solver. Valid values are gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("general", "constants", "const", "Specifies the constant replacements to use in symbolic models.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("constantString", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3").setDefaultValueString("").build()).build());
}
} // namespace modules

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

@ -1,3 +1,6 @@
#ifndef STORM_SETTINGS_MODULES_GENERALSETTINGS_H_
#define STORM_SETTINGS_MODULES_GENERALSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
@ -5,12 +8,15 @@ namespace storm {
namespace modules {
/*!
* This class represents the general options.
* This class represents the general settings.
*/
class GeneralSettings : public ModuleSettings {
public:
GeneralSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_GENERALSETTINGS_H_ */

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

@ -0,0 +1,15 @@
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
settingsManager.addOption(storm::settings::OptionBuilder("GlpkLpSolver", "glpkoutput", "", "If set, the glpk output will be printed to the command line.").build());
}
} // namespace modules
} // namespace settings
} // namespace storm

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

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_GLPKSETTINGS_H_
#define STORM_SETTINGS_MODULES_GLPKSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for glpk.
*/
class GlpkSettings : public ModuleSettings {
public:
GlpkSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_GLPKSETTINGS_H_ */

47
src/settings/modules/GmmxxSettings.cpp
View File

@ -0,0 +1,47 @@
#include "src/settings/modules/GmmxxSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
GmmxxSettings::GmmxxSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// Offer all available methods as a command line option.
std::vector<std::string> methods;
methods.push_back("bicgstab");
methods.push_back("qmr");
methods.push_back("gmres");
methods.push_back("jacobi");
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmlin", "", "The method to be used for solving linear equation systems with the gmm++ engine. Available are: bicgstab, qmr, gmres, jacobi.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
// Register available preconditioners.
std::vector<std::string> preconditioner;
preconditioner.push_back("ilu");
preconditioner.push_back("diagonal");
preconditioner.push_back("ildlt");
preconditioner.push_back("none");
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmpre", "", "The preconditioning technique used for solving linear equation systems with the gmm++ engine. Available are: ilu, diagonal, none.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmrestart", "", "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "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("GmmxxLinearEquationSolver", "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());
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "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("GmmxxNondeterminsticLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-6).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
settingsManager.addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
}
} // namespace modules
} // namespace settings
} // namespace storm

22
src/settings/modules/GmmxxSettings.h
View File

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_GMMXXSETTINGS_H_
#define STORM_SETTINGS_MODULES_GMMXXSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for gmm++.
*/
class GmmxxSettings : public ModuleSettings {
public:
GmmxxSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_GMMXXSETTINGS_H_ */

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

@ -0,0 +1,22 @@
#include "src/settings/modules/GurobiSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
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());
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());
settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobioutput", "", "If set, the Gurobi output will be printed to the command line.").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());
}
} // namespace modules
} // namespace settings
} // namespace storm

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

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_GUROBISETTINGS_H_
#define STORM_SETTINGS_MODULES_GUROBISETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for Gurobi.
*/
class GurobiSettings : public ModuleSettings {
public:
GurobiSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_GUROBISETTINGS_H_ */

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

@ -4,10 +4,14 @@ namespace storm {
namespace settings {
namespace modules {
ModuleSettings::ModuleSettings(storm::settings::SettingsManager& settingsManager) {
ModuleSettings::ModuleSettings(storm::settings::SettingsManager& settingsManager) : settingsManager(settingsManager) {
// Intentionally left empty.
}
storm::settings::SettingsManager const& ModuleSettings::getSettingsManager() const {
return this->settingsManager;
}
} // namespace modules
} // namespace settings
} // namespace storm

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

@ -1,7 +1,13 @@
#include "src/settings/SettingsManager.h"
#ifndef STORM_SETTINGS_MODULES_MODULESETTINGS_H_
#define STORM_SETTINGS_MODULES_MODULESETTINGS_H_
#include <string>
namespace storm {
namespace settings {
// Forward-declare SettingsManager class.
class SettingsManager;
namespace modules {
/*!
@ -15,8 +21,34 @@ namespace storm {
* @param settingsManager The manager responsible for these settings.
*/
ModuleSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
*
* @return True if the settings are consistent.
*/
virtual bool check() const = 0;
protected:
/*!
* Retrieves the manager responsible for the settings.
*
* @return The manager responsible for the settings.
*/
storm::settings::SettingsManager const& getSettingsManager() const;
/*!
* Retrieves whether the option with the given name was set.
*/
bool isSet(std::string const& optionName) const;
private:
// The settings manager responsible for the settings.
storm::settings::SettingsManager const& settingsManager;
};
} // namespace modules
} // namespace settings
} // namespace storm
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */

31
src/settings/modules/NativeEquationSolver.cpp
View File

@ -0,0 +1,31 @@
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
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());
settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").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());
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());
settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
}
} // namespace modules
} // namespace settings
} // namespace storm

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

@ -0,0 +1,22 @@
#ifndef STORM_SETTINGS_MODULES_NATIVEEQUATIONSOLVERSETTINGS_H_
#define STORM_SETTINGS_MODULES_NATIVEEQUATIONSOLVERSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for the native equation solver.
*/
class NativeEquationSolverSettings : public ModuleSettings {
public:
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_NATIVEEQUATIONSOLVERSETTINGS_H_ */
Write Preview
Loading…
Cancel
Save