From ff50fbe12da5fde54366870b0ef778ba4f397194 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 18 Sep 2014 16:29:31 +0200 Subject: [PATCH] Further refactoring of settings classes. Former-commit-id: ed79d0fa4ac508ff63d231a676d1318ec5389dc9 --- src/settings/SettingsManager.cpp | 11 ++ src/settings/SettingsManager.h | 165 ++---------------- .../CounterexampleGeneratorSettings.cpp | 23 +++ .../modules/CounterexampleGeneratorSettings.h | 22 +++ src/settings/modules/CuddSettings.cpp | 40 +++++ src/settings/modules/CuddSettings.h | 22 +++ src/settings/modules/DebugSettings.cpp | 18 ++ src/settings/modules/DebugSettings.h | 22 +++ src/settings/modules/GeneralSettings.cpp | 48 +++++ src/settings/modules/GeneralSettings.h | 10 +- src/settings/modules/GlpkSettings.cpp | 15 ++ src/settings/modules/GlpkSettings.h | 22 +++ src/settings/modules/GmmxxSettings.cpp | 47 +++++ src/settings/modules/GmmxxSettings.h | 22 +++ src/settings/modules/GurobiSettings.cpp | 22 +++ src/settings/modules/GurobiSettings.h | 22 +++ src/settings/modules/ModuleSettings.cpp | 6 +- src/settings/modules/ModuleSettings.h | 36 +++- src/settings/modules/NativeEquationSolver.cpp | 31 ++++ .../modules/NativeEquationSolverSettings.h | 22 +++ 20 files changed, 475 insertions(+), 151 deletions(-) create mode 100644 src/settings/modules/CounterexampleGeneratorSettings.cpp create mode 100644 src/settings/modules/CounterexampleGeneratorSettings.h create mode 100644 src/settings/modules/CuddSettings.cpp create mode 100644 src/settings/modules/CuddSettings.h create mode 100644 src/settings/modules/DebugSettings.cpp create mode 100644 src/settings/modules/DebugSettings.h create mode 100644 src/settings/modules/GlpkSettings.cpp create mode 100644 src/settings/modules/GlpkSettings.h create mode 100644 src/settings/modules/GmmxxSettings.cpp create mode 100644 src/settings/modules/GmmxxSettings.h create mode 100644 src/settings/modules/GurobiSettings.cpp create mode 100644 src/settings/modules/GurobiSettings.h create mode 100644 src/settings/modules/NativeEquationSolver.cpp create mode 100644 src/settings/modules/NativeEquationSolverSettings.h diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 0b476323d..29cad7a75 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -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. * diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 92ec18123..518782662 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -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 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 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 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 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 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 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 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 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. */ diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp new file mode 100644 index 000000000..6ac14d7ec --- /dev/null +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -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 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 \ No newline at end of file diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h new file mode 100644 index 000000000..176311f80 --- /dev/null +++ b/src/settings/modules/CounterexampleGeneratorSettings.h @@ -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_ */ diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp new file mode 100644 index 000000000..e092f6f4a --- /dev/null +++ b/src/settings/modules/CuddSettings.cpp @@ -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 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 \ No newline at end of file diff --git a/src/settings/modules/CuddSettings.h b/src/settings/modules/CuddSettings.h new file mode 100644 index 000000000..d8c2efde8 --- /dev/null +++ b/src/settings/modules/CuddSettings.h @@ -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_ */ diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp new file mode 100644 index 000000000..652364586 --- /dev/null +++ b/src/settings/modules/DebugSettings.cpp @@ -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 \ No newline at end of file diff --git a/src/settings/modules/DebugSettings.h b/src/settings/modules/DebugSettings.h new file mode 100644 index 000000000..d1edf843f --- /dev/null +++ b/src/settings/modules/DebugSettings.h @@ -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_ */ \ No newline at end of file diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index c66276eb8..d5d387dcb 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -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 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 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 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 diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 8297437d0..485ca8277 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -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 \ No newline at end of file +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_GENERALSETTINGS_H_ */ diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp new file mode 100644 index 000000000..bbd4f53cf --- /dev/null +++ b/src/settings/modules/GlpkSettings.cpp @@ -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 \ No newline at end of file diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h new file mode 100644 index 000000000..79e59253b --- /dev/null +++ b/src/settings/modules/GlpkSettings.h @@ -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_ */ diff --git a/src/settings/modules/GmmxxSettings.cpp b/src/settings/modules/GmmxxSettings.cpp new file mode 100644 index 000000000..e7b5eede6 --- /dev/null +++ b/src/settings/modules/GmmxxSettings.cpp @@ -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 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 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 \ No newline at end of file diff --git a/src/settings/modules/GmmxxSettings.h b/src/settings/modules/GmmxxSettings.h new file mode 100644 index 000000000..69486b47d --- /dev/null +++ b/src/settings/modules/GmmxxSettings.h @@ -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_ */ diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp new file mode 100644 index 000000000..ac9122dd2 --- /dev/null +++ b/src/settings/modules/GurobiSettings.cpp @@ -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 \ No newline at end of file diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h new file mode 100644 index 000000000..652033af1 --- /dev/null +++ b/src/settings/modules/GurobiSettings.h @@ -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_ */ diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp index 0662256fd..3aab04b1e 100644 --- a/src/settings/modules/ModuleSettings.cpp +++ b/src/settings/modules/ModuleSettings.cpp @@ -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 \ No newline at end of file diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h index f07a4b24f..5df5d88ab 100644 --- a/src/settings/modules/ModuleSettings.h +++ b/src/settings/modules/ModuleSettings.h @@ -1,7 +1,13 @@ -#include "src/settings/SettingsManager.h" +#ifndef STORM_SETTINGS_MODULES_MODULESETTINGS_H_ +#define STORM_SETTINGS_MODULES_MODULESETTINGS_H_ + +#include 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 \ No newline at end of file +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */ \ No newline at end of file diff --git a/src/settings/modules/NativeEquationSolver.cpp b/src/settings/modules/NativeEquationSolver.cpp new file mode 100644 index 000000000..7fa803e27 --- /dev/null +++ b/src/settings/modules/NativeEquationSolver.cpp @@ -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 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 \ No newline at end of file diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h new file mode 100644 index 000000000..15b4e2d79 --- /dev/null +++ b/src/settings/modules/NativeEquationSolverSettings.h @@ -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_ */