From b6a5fcfd842a5803496a09f5d03c68c34e919f1e Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 May 2019 10:12:01 +0200 Subject: [PATCH 1/5] Settings: Do not hard-code executable name in help message. --- src/storm-cli-utilities/cli.cpp | 2 +- src/storm-conv-cli/storm-conv.cpp | 1 + src/storm/settings/SettingsManager.cpp | 25 ++++++++++++++++--------- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 90b198fa9..c7b18fb7a 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -177,7 +177,7 @@ namespace storm { try { storm::settings::mutableManager().setFromCommandLine(argc, argv); } catch (storm::exceptions::OptionParserException& e) { - STORM_LOG_ERROR("Unable to parse command line options. Type 'storm --help' or 'storm --help all' for help."); + STORM_LOG_ERROR("Unable to parse command line options. Type '" + std::string(argv[0]) + " --help' or '" + std::string(argv[0]) + " --help all' for help."); return false; } diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 1ef0823ea..1c333f93c 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -275,6 +275,7 @@ bool parseOptions(const int argc, const char* argv[]) { try { storm::settings::mutableManager().setFromCommandLine(argc, argv); } catch (storm::exceptions::OptionParserException& e) { + STORM_LOG_ERROR("Unable to parse command line options. Type '" + std::string(argv[0]) + " --help' or '" + std::string(argv[0]) + " --help all' for help."); return false; } diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 099a77f46..04cb48621 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -240,15 +240,22 @@ namespace storm { } } } - if (numHidden > 0) { - STORM_PRINT(numHidden << " hidden options." << std::endl); - } - if (!invisibleModules.empty()) { - STORM_PRINT(invisibleModules.size() << " hidden modules (" << boost::join(invisibleModules, ", ") << ")." << std::endl); - } - if (numHidden > 0 || !invisibleModules.empty()) { - STORM_PRINT(std::endl << "Type 'storm --help modulename' to display all options of a specific module or 'storm --help all' for a complete list of options." << std::endl); - } + if (!includeAdvanced) { + if (numHidden == 1) { + STORM_PRINT(numHidden << " hidden option." << std::endl); + } else { + STORM_PRINT(numHidden << " hidden options." << std::endl); + } + if (!invisibleModules.empty()) { + if (invisibleModules.size() == 1) { + STORM_PRINT(invisibleModules.size() << " hidden module (" << boost::join(invisibleModules, ", ") << ")." << std::endl); + } else { + STORM_PRINT(invisibleModules.size() << " hidden modules (" << boost::join(invisibleModules, ", ") << ")." << std::endl); + } + } + STORM_PRINT(std::endl << "Type '" + executableName + " --help modulename' to display all options of a specific module." << std::endl); + STORM_PRINT("Type '" + executableName + " --help all' to display a complete list of options." << std::endl); + } } else { // Create a regular expression from the input hint. std::regex hintRegex(filter, std::regex_constants::ECMAScript | std::regex_constants::icase); From 5d4088088357baa042f75ad8d09d586e94c2d234 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 May 2019 10:47:52 +0200 Subject: [PATCH 2/5] Flagging a few more options as advanced. --- src/storm/settings/modules/GmmxxEquationSolverSettings.cpp | 4 ++-- .../settings/modules/TopologicalEquationSolverSettings.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp b/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp index 9783081d3..d1dd1cadd 100644 --- a/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp @@ -34,9 +34,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); } bool GmmxxEquationSolverSettings::isLinearEquationSystemMethodSet() const { diff --git a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp index 6445a871e..2a9630a98 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp @@ -27,10 +27,10 @@ namespace storm { TopologicalEquationSolverSettings::TopologicalEquationSolverSettings() : ModuleSettings(moduleName) { std::vector linearEquationSolver = {"gmm++", "native", "eigen", "elimination"}; - this->addOption(storm::settings::OptionBuilder(moduleName, underlyingEquationSolverOptionName, true, "Sets which solver is considered for solving the underlying equation systems.") + this->addOption(storm::settings::OptionBuilder(moduleName, underlyingEquationSolverOptionName, true, "Sets which solver is considered for solving the underlying equation systems.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "vi-to-pi"}; - this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true, "Sets which minmax method is considered for solving the underlying minmax equation systems.") + this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true, "Sets which minmax method is considered for solving the underlying minmax equation systems.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("value-iteration").build()).build()); } From 208854bf02ccc7b204653461abd96e7a302147b9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 May 2019 10:48:43 +0200 Subject: [PATCH 3/5] settings: Detect whether an option was set with or without the module prefix. --- src/storm/settings/Option.cpp | 10 +++++++++- src/storm/settings/Option.h | 17 +++++++++++++++++ src/storm/settings/SettingsManager.cpp | 3 +++ src/storm/settings/modules/ModuleSettings.cpp | 1 + 4 files changed, 30 insertions(+), 1 deletion(-) diff --git a/src/storm/settings/Option.cpp b/src/storm/settings/Option.cpp index 1ab2aa23a..99d03aede 100644 --- a/src/storm/settings/Option.cpp +++ b/src/storm/settings/Option.cpp @@ -117,8 +117,12 @@ namespace storm { bool Option::getHasOptionBeenSet() const { return this->hasBeenSet; } + + bool Option::getHasOptionBeenSetWithModulePrefix() const { + return this->hasBeenSetWithModulePrefix; + } - Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), hasBeenSet(false), arguments(optionArguments), argumentNameMap() { + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), hasBeenSet(false), hasBeenSetWithModulePrefix(false), arguments(optionArguments), argumentNameMap() { // First, do some sanity checks. STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); @@ -138,6 +142,10 @@ namespace storm { void Option::setHasOptionBeenSet(bool newValue) { this->hasBeenSet = newValue; } + + void Option::setHasOptionBeenSetWithModulePrefix(bool newValue) { + this->hasBeenSetWithModulePrefix = newValue; + } uint_fast64_t Option::getPrintLength() const { uint_fast64_t length = 2; diff --git a/src/storm/settings/Option.h b/src/storm/settings/Option.h index 0ff675d21..926dad8d9 100644 --- a/src/storm/settings/Option.h +++ b/src/storm/settings/Option.h @@ -161,6 +161,13 @@ namespace storm { * @return True iff the option has been set. */ bool getHasOptionBeenSet() const; + + /*! + * Retrieves whether the option has been set by including the module prefix. + * + * @return True iff the option has been set by including the module prefix. + */ + bool getHasOptionBeenSetWithModulePrefix() const; /*! * Retrieves whether the option is only displayed in the advanced help. @@ -210,6 +217,9 @@ namespace storm { // A flag that indicates whether this option has been set. bool hasBeenSet; + + // A flag that indicates whether this option has been set. + bool hasBeenSetWithModulePrefix; // The arguments of this option (possibly empty). std::vector> arguments; @@ -239,6 +249,13 @@ namespace storm { * @param newValue The new status of the flag. */ void setHasOptionBeenSet(bool newValue = true); + + /*! + * Sets the flag that marks the option as being (un)set by including the module prefix. + * + * @param newValue The new status of the flag. + */ + void setHasOptionBeenSetWithModulePrefix(bool newValue = true); }; } } diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 04cb48621..f3b9009b2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -494,6 +494,9 @@ namespace storm { } option->setHasOptionBeenSet(); + if (optionName != option->getLongName() && optionName != option->getShortName() && boost::starts_with(optionName, option->getModuleName())) { + option->setHasOptionBeenSetWithModulePrefix(); + } } void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map>> const& optionMap, std::vector const& argumentCache) { diff --git a/src/storm/settings/modules/ModuleSettings.cpp b/src/storm/settings/modules/ModuleSettings.cpp index 528535ec2..b9dde8b08 100644 --- a/src/storm/settings/modules/ModuleSettings.cpp +++ b/src/storm/settings/modules/ModuleSettings.cpp @@ -26,6 +26,7 @@ namespace storm { void ModuleSettings::unset(std::string const& name) { return this->getOption(name).setHasOptionBeenSet(false); + return this->getOption(name).setHasOptionBeenSetWithModulePrefix(false); } std::vector> const& ModuleSettings::getOptions() const { From 5e3506a0e183c9765414b66aec52b11116072c57 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 May 2019 10:50:19 +0200 Subject: [PATCH 4/5] GeneralSettings: Issue a warning when precision is set via --general:precision and not --precision. --- src/storm/settings/modules/GeneralSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index 2db8a22cd..05fe6c542 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/src/storm/settings/modules/GeneralSettings.cpp @@ -81,7 +81,6 @@ namespace storm { return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString(); } - bool GeneralSettings::isBisimulationSet() const { return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); } @@ -103,6 +102,7 @@ namespace storm { } bool GeneralSettings::check() const { + STORM_LOG_WARN_COND(!this->getOption(precisionOptionName).getHasOptionBeenSetWithModulePrefix(), "Setting the precision option with module prefix does not effect all solvers. Consider setting --" << precisionOptionName << " instead of --" << moduleName << ":" << precisionOptionName << "."); return true; } From 511c2d79870ebda3bab37982af0bf88da0dde29b Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 May 2019 10:56:28 +0200 Subject: [PATCH 5/5] Changelog: Update. --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5610f8171..add4eeb9a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,8 @@ Version 1.3.x - Added support for multi-dimensional quantile queries - Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the --qvbs option. - Added script resources/examples/download_qvbs.sh to download the QVBS. -- If an option is unknown, Storm now prints a hint to similar option names. +- If an option is unknown, Storm now suggests similar option names. +- Flagged several options as 'advanced' to clean up the `--help`-message. Use `--help all` to display a complete list of options. - Support for the new `round` operator in the PRISM language - Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]` - JANI: Allow bounded types for constants