Merge branch 'master' into deterministicScheds

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

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;
             }
             

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;
     }
     

src/storm/settings/Option.cpp

@@ -118,7 +118,11 @@ namespace storm {
 				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, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
+			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<std::shared_ptr<ArgumentBase>> 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.");
@@ -139,6 +143,10 @@ namespace storm {
                 this->hasBeenSet = newValue;
             }
             
+            void  Option::setHasOptionBeenSetWithModulePrefix(bool newValue) {
+                this->hasBeenSetWithModulePrefix = newValue;
+            }
+        
             uint_fast64_t Option::getPrintLength() const {
                 uint_fast64_t length = 2;
                 if (!this->getRequiresModulePrefix()) {

src/storm/settings/Option.h

@@ -162,6 +162,13 @@ namespace storm {
              */
             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.
              */
@@ -211,6 +218,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<std::shared_ptr<ArgumentBase>> 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);
 		};
 	}
 }

src/storm/settings/SettingsManager.cpp

@@ -240,14 +240,21 @@ namespace storm {
                         }
                     }
                 }
-                if (numHidden > 0) {
+                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);
                         }
-                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);
+                    }
+                        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.
@@ -487,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<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {

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;
             }
             

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 {

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<std::shared_ptr<Option>> const& ModuleSettings::getOptions() const {

src/storm/settings/modules/TopologicalEquationSolverSettings.cpp

@@ -27,10 +27,10 @@ namespace storm {
             
             TopologicalEquationSolverSettings::TopologicalEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> 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<std::string> 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());
             }