From b5cd4e5758d065232ca5bfeb6ccabc4bcee5071e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 Sep 2014 14:18:06 +0200 Subject: [PATCH] Further option system refactoring. Former-commit-id: 8ac3df44624adfa59eaf67b96b90c4bf07632f48 --- src/settings/OptionBuilder.h | 27 +++--- src/settings/modules/GeneralSettings.cpp | 100 +++++++++++++++-------- src/settings/modules/GeneralSettings.h | 33 +++++++- 3 files changed, 114 insertions(+), 46 deletions(-) diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index 6899114e0..0949deec9 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -1,10 +1,3 @@ -/* - * OptionBuilder.h - * - * Created on: 11.08.2013 - * Author: Philipp Berger - */ - #ifndef STORM_SETTINGS_OPTIONBUILDER_H_ #define STORM_SETTINGS_OPTIONBUILDER_H_ @@ -15,9 +8,9 @@ #include #include -#include "ArgumentType.h" -#include "ArgumentBase.h" -#include "Option.h" +#include "src/settings/ArgumentType.h" +#include "src/settings/ArgumentBase.h" +#include "src/settings/Option.h" #include "src/exceptions/IllegalArgumentException.h" #include "src/exceptions/IllegalFunctionCallException.h" @@ -25,9 +18,21 @@ namespace storm { namespace settings { + /*! + * This class provides the interface to create an option. + */ class OptionBuilder { public: - OptionBuilder(std::string const& newOptionModuleName, std::string const& newOptionLongName, std::string const& newOptionShortName, std::string const& newOptionDescription): longName(newOptionLongName), shortName(newOptionShortName), description(newOptionDescription), moduleName(newOptionModuleName), isRequired(false), isBuild(false) {} + /*! + * Creates a new option builder for an option with the given module, name and description. + * + * @param moduleName The name of the module to which this option belongs. + * @param longName The long name of the option. + * @param shortName The short name of the option. If empty, the option does not have a short name. + * @param + * + */ + OptionBuilder(std::string const& moduleName, std::string const& longName, std::string const& shortName, std::string const& description): longName(newOptionLongName), shortName(newOptionShortName), description(newOptionDescription), moduleName(newOptionModuleName), isRequired(false), isBuild(false) {} ~OptionBuilder() {} diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index d7a1d7559..d48ab5554 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -6,48 +6,82 @@ namespace storm { namespace settings { namespace modules { + const std::string GeneralSettings::moduleName = "general"; + const std::string GeneralSettings::helpOptionName = "help"; + const std::string GeneralSettings::helpOptionShortName = "h"; + const std::string GeneralSettings::verboseOptionName = "verbose"; + const std::string GeneralSettings::verboseOptionShortName = "v"; + const std::string GeneralSettings::exportDotOptionName = "exportdot"; + const std::string GeneralSettings::configOptionName = "config"; + const std::string GeneralSettings::configOptionShortName = "c"; + const std::string GeneralSettings::explicitOptionName = "explicit"; + const std::string GeneralSettings::explicitOptionShortName = "e"; + const std::string GeneralSettings::symbolicOptionName = "symbolic"; + const std::string GeneralSettings::symbolicOptionShortName = "s"; + const std::string GeneralSettings::pctlOptionName = "pctl"; + const std::string GeneralSettings::cslOptionName = "csl"; + const std::string GeneralSettings::ltlOptionName = "ltl"; + const std::string GeneralSettings::transitionRewardsOptionName = "transrew"; + const std::string GeneralSettings::stateRewardsOptionName = "staterew"; + const std::string GeneralSettings::counterexampleOptionName = "counterexample"; + const std::string GeneralSettings::fixDeadlockOptionName = "fixDeadlocks"; + const std::string GeneralSettings::fixDeadlockOptionShortName = "fix"; + const std::string GeneralSettings::timeoutOptionName = "timeout"; + const std::string GeneralSettings::timeoutOptionShortName = "t"; + const std::string GeneralSettings::eqSolverOptionName = "eqsolver"; + const std::string GeneralSettings::lpSolverOptionName = "lpsolver"; + const std::string GeneralSettings::constantsOptionName = "constants"; + const std::string GeneralSettings::constantsOptionShortName = "const"; + 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", "pctl", "", "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()); + // First, we need to create all options of this module. + std::vector> options; + options.push_back(storm::settings::OptionBuilder(moduleName, helpOptionName, helpOptionShortName, "Shows all available options, arguments and descriptions.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, verboseOptionName, verboseOptionShortName, "Enables more verbose output.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, configOptionName, configOptionShortName, "If given, this file will be read and parsed for additional configuration settings.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, explicitOptionName, explicitOptionShortName, "Parses the model given in an explicit (sparse) representation.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, symbolicOptionName, symbolicOptionShortName, "Parses the model given in a symbolic representation.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, pctlOptionName, "", "Specifies the PCTL formulas that are to be checked on the model.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, cslOptionName, "", "Specifies the CSL formulas that are to be checked on the model.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, ltlOptionName, "", "Specifies the LTL formulas that are to be checked on the model.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, "", "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build()); + + options.push_back(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, "", "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ")."); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, fixDeadlockOptionShortName, "If the model contains deadlock states, they need to be fixed by setting this option.").build()); std::vector linearEquationSolver; linearEquationSolver.push_back("gmm++"); linearEquationSolver.push_back("native"); - settingsManager.addOption(storm::settings::OptionBuilder("general", "eqsolver", "", "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()); - + settingsManager.addOption(); + options.push_back(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, "", "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()); + options.push_back(storm::settings::OptionBuilder(moduleName, timeoutOptionName, timeoutOptionShortName, "If given, computation will abort after the timeout has been reached.") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).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(); + options.push_back(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, "", "Sets which LP solver is preferred.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, constantsOptionName, constantsOptionShortName, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").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()); + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 0f1c803d7..ca7cc4c40 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -82,14 +82,14 @@ namespace storm { * * @return True if the transition reward option was set. */ - bool isTransitionRewardSet() const; + bool isTransitionRewardsSet() const; /*! * Retrieves whether the state reward option was set. * * @return True if the state reward option was set. */ - bool isStateRewardSet() const; + bool isStateRewardsSet() const; /*! * Retrieves whether the counterexample option was set. @@ -133,6 +133,35 @@ namespace storm { */ bool isConstantsSet() const; + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string helpOptionName; + static const std::string helpOptionShortName; + static const std::string verboseOptionName; + static const std::string verboseOptionShortName; + static const std::string exportDotOptionName; + static const std::string configOptionName; + static const std::string configOptionShortName; + static const std::string explicitOptionName; + static const std::string explicitOptionShortName; + static const std::string symbolicOptionName; + static const std::string symbolicOptionShortName; + static const std::string pctlOptionName; + static const std::string cslOptionName; + static const std::string ltlOptionName; + static const std::string transitionRewardsOptionName; + static const std::string stateRewardsOptionName; + static const std::string counterexampleOptionName; + static const std::string fixDeadlockOptionName; + static const std::string fixDeadlockOptionShortName; + static const std::string timeoutOptionName; + static const std::string timeoutOptionShortName; + static const std::string eqSolverOptionName; + static const std::string lpSolverOptionName; + static const std::string constantsOptionName; + static const std::string constantsOptionShortName; + }; } // namespace modules