added option 'exact' (in addition to parametric)

Former-commit-id: ccc026a44d

src/cli/cli.cpp

@@ -229,15 +229,13 @@ namespace storm {
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas(parsedFormulas.begin(), parsedFormulas.end());
                 
                 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) {
-#ifdef STORM_HAVE_CARL
                     if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
                         buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas, true);
+                    } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+                        buildAndCheckSymbolicModel<storm::RationalNumber>(program.get(), formulas, true);
                     } else {
-#endif
                         buildAndCheckSymbolicModel<double>(program.get(), formulas, true);
-#ifdef STORM_HAVE_CARL
                     }
-#endif
                 } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
                     STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine.");
                     buildAndCheckExplicitModel<double>(formulas, true);

src/settings/modules/GeneralSettings.cpp

@@ -32,10 +32,8 @@ namespace storm {
             const std::string GeneralSettings::timeoutOptionShortName = "t";
             const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
             const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
-            
-#ifdef STORM_HAVE_CARL
             const std::string GeneralSettings::parametricOptionName = "parametric";
-#endif
+            const std::string GeneralSettings::exactOptionName = "exact";
 
             GeneralSettings::GeneralSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -52,10 +50,8 @@ namespace storm {
                 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());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
-                
-#ifdef STORM_HAVE_CARL
-                this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build());
-#endif
+                this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exactOptionName, false, "Sets whether to enable exact model checking.").build());
             }
             
             bool GeneralSettings::isHelpSet() const {
@@ -106,12 +102,14 @@ namespace storm {
                 return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
             }
             
-#ifdef STORM_HAVE_CARL
             bool GeneralSettings::isParametricSet() const {
                 return this->getOption(parametricOptionName).getHasOptionBeenSet();
             }
-#endif
 
+            bool GeneralSettings::isExactSet() const {
+                return this->getOption(exactOptionName).getHasOptionBeenSet();
+            }
+            
             void GeneralSettings::finalize() {
             }
 

src/settings/modules/GeneralSettings.h

@@ -106,15 +106,20 @@ namespace storm {
                  */
                 bool isBisimulationSet() const;
 
-#ifdef STORM_HAVE_CARL
                 /*!
                  * Retrieves whether the option enabling parametric model checking is set.
                  *
                  * @return True iff the option was set.
                  */
                 bool isParametricSet() const;
-#endif
-                
+
+                /*!
+                 * Retrieves whether the option enabling exact model checking is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isExactSet() const;
+
                 bool check() const override;
                 void finalize() override;
 
@@ -138,10 +143,8 @@ namespace storm {
                 static const std::string timeoutOptionShortName;
                 static const std::string bisimulationOptionName;
                 static const std::string bisimulationOptionShortName;
-
-#ifdef STORM_HAVE_CARL
                 static const std::string parametricOptionName;
-#endif
+                static const std::string exactOptionName;
             };
 
         } // namespace modules

src/storm.cpp

@@ -13,8 +13,8 @@ int main(const int argc, const char** argv) {
 
     try {
         storm::utility::setUp();
-        storm::cli::printHeader("SToRM", argc, argv);
-        storm::settings::initializeAll("SToRM", "storm");
+        storm::cli::printHeader("Storm", argc, argv);
+        storm::settings::initializeAll("Storm", "storm");
         bool optionsCorrect = storm::cli::parseOptions(argc, argv);
         if (!optionsCorrect) {
             return -1;
@@ -27,8 +27,8 @@ int main(const int argc, const char** argv) {
         storm::utility::cleanUp();
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what());
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what());
     }
 }