diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index e4a929445..90b198fa9 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -177,8 +177,7 @@ namespace storm { try { storm::settings::mutableManager().setFromCommandLine(argc, argv); } catch (storm::exceptions::OptionParserException& e) { - storm::settings::manager().printHelp(); - throw e; + STORM_LOG_ERROR("Unable to parse command line options. Type 'storm --help' or 'storm --help all' for help."); return false; } @@ -186,7 +185,7 @@ namespace storm { bool result = true; if (general.isHelpSet()) { - storm::settings::manager().printHelp(storm::settings::getModule().getHelpModuleName()); + storm::settings::manager().printHelp(storm::settings::getModule().getHelpFilterExpression()); result = false; } diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index d60895eff..1ef0823ea 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -275,8 +275,6 @@ bool parseOptions(const int argc, const char* argv[]) { try { storm::settings::mutableManager().setFromCommandLine(argc, argv); } catch (storm::exceptions::OptionParserException& e) { - storm::settings::manager().printHelp(); - throw e; return false; } @@ -289,7 +287,7 @@ bool parseOptions(const int argc, const char* argv[]) { bool result = true; if (general.isHelpSet()) { - storm::settings::manager().printHelp(general.getHelpModuleName()); + storm::settings::manager().printHelp(general.getHelpFilterExpression()); result = false; } diff --git a/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp b/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp index 4f1c65e74..19ab31765 100644 --- a/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp +++ b/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp @@ -22,8 +22,8 @@ namespace storm { const std::string ConversionGeneralSettings::configOptionShortName = "c"; ConversionGeneralSettings::ConversionGeneralSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows available options, arguments and descriptions.").setShortName(helpOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "'frequent' for frequently used options, 'all' for the complete help, or a regular expression to show help for all matching entities.").setDefaultValueString("frequent").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Enables verbose and debug output.").build()); @@ -40,8 +40,8 @@ namespace storm { return this->getOption(versionOptionName).getHasOptionBeenSet(); } - std::string ConversionGeneralSettings::getHelpModuleName() const { - return this->getOption(helpOptionName).getArgumentByName("hint").getValueAsString(); + std::string ConversionGeneralSettings::getHelpFilterExpression() const { + return this->getOption(helpOptionName).getArgumentByName("filter").getValueAsString(); } bool ConversionGeneralSettings::isVerboseSet() const { diff --git a/src/storm-conv/settings/modules/ConversionGeneralSettings.h b/src/storm-conv/settings/modules/ConversionGeneralSettings.h index dc7e79f27..343035382 100644 --- a/src/storm-conv/settings/modules/ConversionGeneralSettings.h +++ b/src/storm-conv/settings/modules/ConversionGeneralSettings.h @@ -30,7 +30,7 @@ namespace storm { * * @return The name of the module for which to show the help or "all". */ - std::string getHelpModuleName() const; + std::string getHelpFilterExpression() const; /*! * Retrieves whether the verbose option was set. diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index 5b2142ee3..27a2c1120 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp @@ -20,11 +20,11 @@ namespace storm { CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) { std::vector techniques = {"maxsat", "milp"}; - this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command/edge 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/edge set. Note that this requires the model to be given in a symbolic format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").setIsAdvanced().build()); } bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const { diff --git a/src/storm/settings/Option.cpp b/src/storm/settings/Option.cpp index 338289fe6..1ab2aa23a 100644 --- a/src/storm/settings/Option.cpp +++ b/src/storm/settings/Option.cpp @@ -14,11 +14,11 @@ namespace storm { namespace settings { - Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, isAdvanced, optionArguments) { // Intentionally left empty. } - Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, isAdvanced, optionArguments) { // Intentionally left empty. } @@ -85,13 +85,11 @@ namespace storm { std::string const& Option::getLongName() const { return this->longName; } - bool Option::getHasShortName() const { return this->hasShortName; } - std::string const& Option::getShortName() const { return this->shortName; } @@ -108,16 +106,19 @@ namespace storm { return this->isRequired; } - bool Option::getRequiresModulePrefix() const { return this->requireModulePrefix; } + bool Option::getIsAdvanced() const { + return this->isAdvanced; + } + bool Option::getHasOptionBeenSet() const { return this->hasBeenSet; } - Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), 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), 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."); diff --git a/src/storm/settings/Option.h b/src/storm/settings/Option.h index 1adf8ddff..0ff675d21 100644 --- a/src/storm/settings/Option.h +++ b/src/storm/settings/Option.h @@ -40,9 +40,10 @@ namespace storm { * @param isOptionRequired Sets whether the option is required to appear. * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the * module name. + * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); + Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments = std::vector>()); /*! * Creates an option with the given parameters. @@ -53,10 +54,10 @@ namespace storm { * @param optionDescription The description of the option. * @param isOptionRequired Sets whether the option is required to appear. * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the - * module name. + * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); + Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector> const& optionArguments = std::vector>()); /*! * Checks whether the given option is compatible with the current one. If not, an exception is thrown. @@ -161,6 +162,11 @@ namespace storm { */ bool getHasOptionBeenSet() const; + /*! + * Retrieves whether the option is only displayed in the advanced help. + */ + bool getIsAdvanced() const; + /*! * Retrieves the arguments of the option. * @@ -199,6 +205,9 @@ namespace storm { // A flag that indicates whether this option is required to be prefixed with the module name. bool requireModulePrefix; + // A flag that indicates whether this option is only displayed in the advanced help. + bool isAdvanced; + // A flag that indicates whether this option has been set. bool hasBeenSet; @@ -219,9 +228,10 @@ namespace storm { * @param isOptionRequired Sets whether the option is required to appear. * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the * module name. + * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); + 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 = std::vector>()); /*! * Sets the flag that marks the option as being (un)set. diff --git a/src/storm/settings/OptionBuilder.h b/src/storm/settings/OptionBuilder.h index f6b2bfea1..643b13b3b 100644 --- a/src/storm/settings/OptionBuilder.h +++ b/src/storm/settings/OptionBuilder.h @@ -33,7 +33,7 @@ namespace storm { * @param requireModulePrefix Sets whether this option can only be set by specifying the module name as its prefix. * @param description A description that explains the purpose of this option. */ - OptionBuilder(std::string const& moduleName, std::string const& longName, bool requireModulePrefix, std::string const& description) : longName(longName), shortName(""), hasShortName(false), description(description), moduleName(moduleName), requireModulePrefix(requireModulePrefix), isRequired(false), isBuild(false), arguments(), argumentNameSet() { + OptionBuilder(std::string const& moduleName, std::string const& longName, bool requireModulePrefix, std::string const& description) : longName(longName), shortName(""), hasShortName(false), description(description), moduleName(moduleName), requireModulePrefix(requireModulePrefix), isRequired(false), isAdvanced(false), isBuild(false), arguments(), argumentNameSet() { // Intentionally left empty. } @@ -60,6 +60,14 @@ namespace storm { return *this; } + /*! + * Sets whether the option is only displayed in the advanced help. + */ + OptionBuilder& setIsAdvanced(bool isAdvanced = true) { + this->isAdvanced = isAdvanced; + return *this; + } + /*! * Adds the given argument to the arguments of this option. * @@ -89,9 +97,9 @@ namespace storm { this->isBuild = true; if (this->hasShortName) { - return std::shared_ptr