From 8711b32c995800b7b3a0eb6d8a577d3fd87d1562 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Feb 2020 09:06:16 +0100
Subject: [PATCH] When using bisimulation with the dd-to-sparse engine, the
quotient is automatically extracted in a sparse way.
---
src/storm-cli-utilities/model-handling.h | 5 ++++-
src/storm/settings/modules/BisimulationSettings.cpp | 4 ++++
src/storm/settings/modules/BisimulationSettings.h | 7 +++++++
3 files changed, 15 insertions(+), 1 deletion(-)
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index c83c39e93..010698ac7 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -510,7 +510,10 @@ namespace storm {
STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
auto quotientFormat = bisimulationSettings.getQuotientFormat();
-
+ if (mpi.engine == storm::utility::Engine::DdSparse && quotientFormat != storm::dd::bisimulation::QuotientFormat::Sparse && bisimulationSettings.isQuotientFormatSetFromDefaultValue()) {
+ STORM_LOG_INFO("Setting bisimulation quotient format to 'sparse'.");
+ quotientFormat = storm::dd::bisimulation::QuotientFormat::Sparse;
+ }
STORM_LOG_INFO("Performing bisimulation minimization...");
return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode(), quotientFormat);
}
diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp
index 05f70678f..1b5606bf5 100644
--- a/src/storm/settings/modules/BisimulationSettings.cpp
+++ b/src/storm/settings/modules/BisimulationSettings.cpp
@@ -70,6 +70,10 @@ namespace storm {
return false;
}
+ bool BisimulationSettings::isQuotientFormatSetFromDefaultValue() const {
+ return !this->getOption(quotientFormatOptionName).getHasOptionBeenSet() || this->getOption(quotientFormatOptionName).getArgumentByName("format").wasSetFromDefaultValue();
+ }
+
storm::dd::bisimulation::QuotientFormat BisimulationSettings::getQuotientFormat() const {
std::string quotientFormatAsString = this->getOption(quotientFormatOptionName).getArgumentByName("format").getValueAsString();
if (quotientFormatAsString == "sparse") {
diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h
index ff372de01..acf6ac424 100644
--- a/src/storm/settings/modules/BisimulationSettings.h
+++ b/src/storm/settings/modules/BisimulationSettings.h
@@ -43,6 +43,13 @@ namespace storm {
*/
bool isWeakBisimulationSet() const;
+ /*!
+ * Retrieves whether the format in which the quotient is to be extracted has been set from its default value.
+ *
+ * @return True iff it has been set from its default value.
+ */
+ bool isQuotientFormatSetFromDefaultValue() const;
+
/*!
* Retrieves the format in which the quotient is to be extracted.
* NOTE: only applies to DD-based bisimulation.