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(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.