From 46dc2ca05a3994e2add0daeb522fa3c6d08abca0 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 22 Sep 2014 21:17:20 +0200 Subject: [PATCH] Further work on option system (we're getting there...). Former-commit-id: cae593d5a13dc85ca29a794dff3c4a69235a935f --- src/settings/SettingsManager.cpp | 22 ++- src/settings/SettingsManager.h | 7 +- .../CounterexampleGeneratorSettings.cpp | 36 +++- .../modules/CounterexampleGeneratorSettings.h | 8 +- src/settings/modules/CuddSettings.cpp | 56 +++++- src/settings/modules/DebugSettings.cpp | 22 ++- src/settings/modules/GeneralSettings.cpp | 178 ++++++++++++++++-- src/settings/modules/ModuleSettings.cpp | 12 ++ src/settings/modules/ModuleSettings.h | 8 + 9 files changed, 313 insertions(+), 36 deletions(-) diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index d8a5ab506..525cefc29 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -65,7 +65,7 @@ namespace storm { if (currentArgument.at(0) == '-') { // At this point we know that a new option is about to come. Hence, we need to assign the current // cache content to the option that was active until now. - this->setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache); + setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache); if (currentArgument.at(1) == '-') { // In this case, the argument has to be the long name of an option. Try to get all options that @@ -121,18 +121,36 @@ namespace storm { // not required for this option, we have to add both versions to our mappings, the prefixed one and the // non-prefixed one. if (!option->getRequiresModulePrefix()) { + bool isCompatible = this->isCompatible(option, option->getLongName(), this->longNameToOptions); + LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it."); this->longNameToOptions.emplace(option->getLongName(), option); } + // For the prefixed name, we don't need a compatibility check, because a module is not allowed to register the same option twice. this->longNameToOptions.emplace(option->getModuleName() + ":" + option->getLongName(), option); if (option->getHasShortName()) { if (!option->getRequiresModulePrefix()) { - this->shortNameToOptions.emplace(option->getLongName(), option); + this->shortNameToOptions.emplace(option->getShortName(), option); + bool isCompatible = this->isCompatible(option, option->getShortName(), this->shortNameToOptions); + LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it."); } this->shortNameToOptions.emplace(option->getModuleName() + ":" + option->getShortName(), option); } } + bool SettingsManager::isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap) { + auto optionIterator = optionMap.find(optionName); + if (optionIterator != optionMap.end()) { + for (auto const& otherOption : optionIterator->second) { + bool locallyCompatible = option->isCompatibleWith(*otherOption); + if (!locallyCompatible) { + return false; + } + } + } + return true; + } + void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) { auto optionIterator = optionMap.find(optionName); LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'."); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index dd16b7adc..40421019a 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -144,7 +144,12 @@ namespace storm { * @param optionMap The mapping from option names to options. * @param argumentCache The arguments of the option as string values. */ - void setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache); + static void setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache); + + /*! + * Checks whether the given option is compatible with all options with the given name in the given mapping. + */ + static bool isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap); }; /*! diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index f6ff3347c..3078c6417 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -14,12 +14,40 @@ namespace storm { CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector<std::string> techniques = {"sat", "milp"}; - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.") + this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "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. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); + } + + bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const { + return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); + } + + std::string CounterexampleGeneratorSettings::minimalCommandSetPropertyFilename() const { + return this->getOption(minimalCommandSetOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { + return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; + } + + bool CounterexampleGeneratorSettings::isUseMaxSatBasedMinimalCommandSetGenerationSet() const { + return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "maxsat"; + } + + bool CounterexampleGeneratorSettings::isEncodeReachabilitySet() const { + return this->getOption(encodeReachabilityOptionName).getHasOptionBeenSet(); + } + + bool CounterexampleGeneratorSettings::isUseSchedulerCutsSet() const { + return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet(); + } + + bool CounterexampleGeneratorSettings::isShowStatisticsSet() const { + return this->getOption(statisticsOptionName).getHasOptionBeenSet(); } } // namespace modules diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h index 33b394a6e..0cee9ff5b 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/settings/modules/CounterexampleGeneratorSettings.h @@ -40,7 +40,7 @@ namespace storm { * * @return True iff the MILP-based technique is to be used. */ - bool useMilpBasedMinimalCommandSetGeneration() const; + bool isUseMilpBasedMinimalCommandSetGenerationSet() const; /*! * Retrieves whether the MAXSAT-based technique is to be used to generate a minimal command set @@ -48,7 +48,7 @@ namespace storm { * * @return True iff the MAXSAT-based technique is to be used. */ - bool useMaxSatBasedMinimalCommandSetGeneration() const; + bool isUseMaxSatBasedMinimalCommandSetGenerationSet() const; /*! * Retrieves whether reachability of a target state is to be encoded if the MAXSAT-based technique is @@ -64,14 +64,14 @@ namespace storm { * * @return True iff scheduler cuts are to be used. */ - bool useSchedulerCuts() const; + bool isUseSchedulerCutsSet() const; /*! * Retrieves whether statistics are to be shown for counterexample generation. * * @return True iff statistics are to be shown for counterexample generation. */ - bool showStatistics() const; + bool isShowStatisticsSet() const; // The name of the module. static const std::string moduleName; diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp index dffef2457..f9eb09699 100644 --- a/src/settings/modules/CuddSettings.cpp +++ b/src/settings/modules/CuddSettings.cpp @@ -12,9 +12,9 @@ namespace storm { const std::string reorderOptionName = "reorder"; CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "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(moduleName, precisionOptionName, true, "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->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "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()); + this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build()); std::vector<std::string> reorderingTechniques; reorderingTechniques.push_back("none"); @@ -35,7 +35,57 @@ namespace storm { reorderingTechniques.push_back("annealing"); reorderingTechniques.push_back("genetic"); reorderingTechniques.push_back("exact"); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "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()); + this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "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()); + } + + double CuddSettings::getConstantPrecision() const { + return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); + } + + uint_fast64_t CuddSettings::getMaximalMemory() const { + return this->getOption(maximalMemoryOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); + } + + CuddSettings::ReorderingTechnique CuddSettings::getReorderingTechnique() const { + std::string reorderingTechniqueAsString = this->getOption(reorderOptionName).getArgumentByName("method").getValueAsString(); + if (reorderingTechniqueAsString == "none") { + return CuddSettings::ReorderingTechnique::None; + } else if (reorderingTechniqueAsString == "random") { + return CuddSettings::ReorderingTechnique::Random; + } else if (reorderingTechniqueAsString == "randompivot") { + return CuddSettings::ReorderingTechnique::RandomPivot; + } else if (reorderingTechniqueAsString == "sift") { + return CuddSettings::ReorderingTechnique::Sift; + } else if (reorderingTechniqueAsString == "siftconv") { + return CuddSettings::ReorderingTechnique::SiftConv; + } else if (reorderingTechniqueAsString == "ssift") { + return CuddSettings::ReorderingTechnique::SymmetricSift; + } else if (reorderingTechniqueAsString == "ssiftconv") { + return CuddSettings::ReorderingTechnique::SymmetricSiftConv; + } else if (reorderingTechniqueAsString == "gsift") { + return CuddSettings::ReorderingTechnique::GroupSift; + } else if (reorderingTechniqueAsString == "gsiftconv") { + return CuddSettings::ReorderingTechnique::GroupSiftConv; + } else if (reorderingTechniqueAsString == "win2") { + return CuddSettings::ReorderingTechnique::Win2; + } else if (reorderingTechniqueAsString == "win2conv") { + return CuddSettings::ReorderingTechnique::Win2Conv; + } else if (reorderingTechniqueAsString == "win3") { + return CuddSettings::ReorderingTechnique::Win3; + } else if (reorderingTechniqueAsString == "win3conv") { + return CuddSettings::ReorderingTechnique::Win3Conv; + } else if (reorderingTechniqueAsString == "win4") { + return CuddSettings::ReorderingTechnique::Win4; + } else if (reorderingTechniqueAsString == "win4conv") { + return CuddSettings::ReorderingTechnique::Win4Conv; + } else if (reorderingTechniqueAsString == "annealing") { + return CuddSettings::ReorderingTechnique::Annealing; + } else if (reorderingTechniqueAsString == "genetic") { + return CuddSettings::ReorderingTechnique::Genetic; + } else if (reorderingTechniqueAsString == "exact") { + return CuddSettings::ReorderingTechnique::Exact; + } + LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << reorderingTechniqueAsString << "' set as reordering technique of Cudd."); } } // namespace modules diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp index c78f47b14..946667732 100644 --- a/src/settings/modules/DebugSettings.cpp +++ b/src/settings/modules/DebugSettings.cpp @@ -13,12 +13,28 @@ namespace storm { const std::string DebugSettings::logfileOptionShortName = "l"; DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build()); } + bool DebugSettings::isDebugSet() const { + return this->getOption(debugOptionName).getHasOptionBeenSet(); + } + + bool DebugSettings::isTraceSet() const { + return this->getOption(traceOptionName).getHasOptionBeenSet(); + } + + bool DebugSettings::isLogfileSet() const { + return this->getOption(logfileOptionName).getHasOptionBeenSet(); + } + + std::string DebugSettings::getLogfilename() const { + return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString(); + } + } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 961f1e140..0ba8cf70a 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -37,48 +37,188 @@ namespace storm { GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector<std::string> moduleNames = {"all", "general", "debug", "cudd", "counterexample", "glpk", "gurobi", "gmm++", "native"}; - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The internally used precision.").setShortName(precisionOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The internally used precision.").setShortName(precisionOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") + this->addOption(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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) .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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") + this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.") + this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.") + this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") + this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "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()); - this->addAndRegisterOption(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 + ").") + this->addOption(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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "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 + ").") + this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build()); std::vector<std::string> linearEquationSolver = {"gmm++", "native"}; - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") + this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); - + std::vector<std::string> lpSolvers = {"gurobi", "glpk"}; - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") + this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "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()); - this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "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 + ").").setShortName(constantsOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "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 + ").").setShortName(constantsOptionShortName) .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()); } + bool GeneralSettings::isHelpSet() const { + return this->getOption(helpOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getHelpModuleName() const { + return this->getOption(helpOptionName).getArgumentByName("module").getValueAsString(); + } + + bool GeneralSettings::isVerboseSet() const { + return this->getOption(verboseOptionName).getHasOptionBeenSet(); + } + + double GeneralSettings::getPrecision() const { + return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); + } + + bool GeneralSettings::isExportDotSet() const { + return this->getOption(exportDotOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getExportDotFilename() const { + return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isConfigSet() const { + return this->getOption(configOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getConfigFilename() const { + return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isExplicitSet() const { + return this->getOption(explicitOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getTransitionFilename() const { + return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); + } + + std::string GeneralSettings::getLabelingFilename() const { + return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); + } + + bool GeneralSettings::isSymbolicSet() const { + return this->getOption(symbolicOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getSymbolicModelFilename() const { + return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isPctlSet() const { + return this->getOption(pctlOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getPctlPropertiesFilename() const { + return this->getOption(pctlOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isCslSet() const { + return this->getOption(cslOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getCslPropertiesFilename() const { + return this->getOption(cslOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isLtlSet() const { + return this->getOption(ltlOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getLtlPropertiesFilename() const { + return this->getOption(ltlOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isTransitionRewardsSet() const { + return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getTransitionRewardsFilename() const { + return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isStateRewardsSet() const { + return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getStateRewardsFilename() const { + return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isCounterexampleSet() const { + return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getCounterexampleFilename() const { + return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GeneralSettings::isFixDeadlocksSet() const { + return this->getOption(fixDeadlockOptionName).getHasOptionBeenSet(); + } + + bool GeneralSettings::isTimeoutSet() const { + return this->getOption(timeoutOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t GeneralSettings::getTimeoutInSeconds() const { + return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); + } + + GeneralSettings::EquationSolver GeneralSettings::getEquationSolver() const { + std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); + if (equationSolverName == "gmm++") { + return GeneralSettings::EquationSolver::Gmmxx; + } else if (equationSolverName == "native") { + return GeneralSettings::EquationSolver::Native; + } + LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); + } + + GeneralSettings::LpSolver GeneralSettings::getLpSolver() const { + std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); + if (lpSolverName == "gurobi") { + return GeneralSettings::LpSolver::Gurobi; + } else if (lpSolverName == "glpk") { + return GeneralSettings::LpSolver::glpk; + } + LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << equationSolverName << "'."); + } + + bool GeneralSettings::isConstantsSet() const { + return this->getOption(constantsOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getConstantDefinitionString() const { + return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); + } + } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp index f1fa8ddb6..782a58fa7 100644 --- a/src/settings/modules/ModuleSettings.cpp +++ b/src/settings/modules/ModuleSettings.cpp @@ -35,6 +35,18 @@ namespace storm { return result; } + Option const& ModuleSettings::getOption(std::string const& longName) const { + auto optionIterator = this->options.find(longName); + LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'."); + return *optionIterator->second; + } + + Option& ModuleSettings::getOption(std::string const& longName) { + auto optionIterator = this->options.find(longName); + LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'."); + return *optionIterator->second; + } + } // 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 f97bbf776..ec3c1231b 100644 --- a/src/settings/modules/ModuleSettings.h +++ b/src/settings/modules/ModuleSettings.h @@ -78,6 +78,14 @@ namespace storm { */ Option& getOption(std::string const& longName); + /*! + * Retrieves the option with the given long name. If no such option exists, an exception is thrown. + * + * @param longName The long name of the option to retrieve. + * @return The option associated with the given option name. + */ + Option const& getOption(std::string const& longName) const; + /*! * Retrieves whether the option with the given name was set. *