From 8f12b3b8c4883f1007bcbbbaf0491e973cb21eed Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 20 Jun 2016 20:07:39 +0200
Subject: [PATCH] added option 'exact' (in addition to parametric)
Former-commit-id: ccc026a44d31fab3c286fbfc844657b228b2ad4c
---
src/cli/cli.cpp | 6 ++----
src/settings/modules/GeneralSettings.cpp | 16 +++++++---------
src/settings/modules/GeneralSettings.h | 15 +++++++++------
src/storm.cpp | 8 ++++----
4 files changed, 22 insertions(+), 23 deletions(-)
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 8fd9120cb..b8566af22 100644
--- a/src/cli/cli.cpp
+++ b/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);
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 91620e09e..a83265541 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/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() {
}
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 1f7bf3445..ad37bda72 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/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
diff --git a/src/storm.cpp b/src/storm.cpp
index 464dda56f..d12dce50e 100644
--- a/src/storm.cpp
+++ b/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());
}
}