If an option is unknown, Storm now prints a hint to similar option names.

CHANGELOG.md

@@ -11,6 +11,7 @@ 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.
 - Allow bounded types for constants in JANI.
 - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
 

src/storm/settings/SettingsManager.cpp

@@ -39,6 +39,7 @@
 #include "storm/settings/modules/MultiplierSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
+#include "storm/utility/string.h"
 #include "storm/settings/Option.h"
 
 namespace storm {
@@ -82,6 +83,18 @@ namespace storm {
             }
         }
         
+        void SettingsManager::handleUnknownOption(std::string const& optionName, bool isShort) const {
+            std::string optionNameWithDashes = (isShort ? "-" : "--") + optionName;
+            storm::utility::string::SimilarStrings similarStrings(optionNameWithDashes, 0.6, false);
+            for (auto const& longOption : longNameToOptions) {
+                similarStrings.add("--" + longOption.first);
+            }
+            for (auto const& shortOption : shortNameToOptions) {
+                similarStrings.add("-" + shortOption.first);
+            }
+            STORM_LOG_THROW(false, storm::exceptions::OptionParserException, "Unknown option '" << optionNameWithDashes << "'. " << similarStrings.toDidYouMeanString());
+        }
+        
         void SettingsManager::setFromExplodedString(std::vector<std::string> const& commandLineArguments) {
             // In order to assign the parsed arguments to an option, we need to keep track of the "active" option's name.
             bool optionActive = false;
@@ -111,7 +124,9 @@ namespace storm {
                         // match the long name.
                         std::string optionName = currentArgument.substr(2);
                         auto optionIterator = this->longNameToOptions.find(optionName);
-                        STORM_LOG_THROW(optionIterator != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
+                        if (optionIterator == this->longNameToOptions.end()) {
+                            handleUnknownOption(optionName, false);
+                        }
                         activeOptionIsShortName = false;
                         activeOptionName = optionName;
                     } else {
@@ -119,7 +134,9 @@ namespace storm {
                         // match the short name.
                         std::string optionName = currentArgument.substr(1);
                         auto optionIterator = this->shortNameToOptions.find(optionName);
-                        STORM_LOG_THROW(optionIterator != this->shortNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
+                        if (optionIterator == this->shortNameToOptions.end()) {
+                            handleUnknownOption(optionName, true);
+                        }
                         activeOptionIsShortName = true;
                         activeOptionName = optionName;
                     }

src/storm/settings/SettingsManager.h

@@ -64,6 +64,11 @@ namespace storm {
              */
             void setFromConfigurationFile(std::string const& configFilename);
             
+            /*!
+             * Throws an exception with a nice error message indicating similar valid option names.
+             */
+            void handleUnknownOption(std::string const& optionName, bool isShort) const;
+            
             /*!
              * This function prints a help message to the standard output. Optionally, a string can be given as a hint.
              * If it is 'all', the complete help is shown. Otherwise, the string is interpreted as a regular expression