diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h
index 40391be2b..d5ae374c5 100644
--- a/src/storm/api/bisimulation.h
+++ b/src/storm/api/bisimulation.h
@@ -56,7 +56,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
- typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
+ typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const& quotientFormat = storm::dd::bisimulation::QuotientFormat::Dd) {
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs, CTMCs, MDPs and MAs.");
STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported.");
@@ -66,11 +66,11 @@ namespace storm {
storm::dd::BisimulationDecomposition<DdType, ValueType, ExportValueType> decomposition(*model, formulas, bisimulationType);
decomposition.compute(mode);
- return decomposition.getQuotient();
+ return decomposition.getQuotient(quotientFormat);
}
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
- typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
+ typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const& quotientFormat = storm::dd::bisimulation::QuotientFormat::Dd) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is not supported for this combination of DD library and value type.");
return nullptr;
}
diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
index b41ddaca5..d574de24d 100644
--- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
@@ -60,7 +60,7 @@ namespace storm {
template<typename ModelType>
std::shared_ptr<storm::models::Model<typename BisimulationAbstractionRefinementModelChecker<ModelType>::ValueType>> BisimulationAbstractionRefinementModelChecker<ModelType>::getAbstractModel() {
- lastAbstractModel = this->bisimulation->getQuotient();
+ lastAbstractModel = this->bisimulation->getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
return lastAbstractModel;
}
diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp
index 8f797a40f..05f70678f 100644
--- a/src/storm/settings/modules/BisimulationSettings.cpp
+++ b/src/storm/settings/modules/BisimulationSettings.cpp
@@ -70,12 +70,13 @@ namespace storm {
return false;
}
- BisimulationSettings::QuotientFormat BisimulationSettings::getQuotientFormat() const {
+ storm::dd::bisimulation::QuotientFormat BisimulationSettings::getQuotientFormat() const {
std::string quotientFormatAsString = this->getOption(quotientFormatOptionName).getArgumentByName("format").getValueAsString();
if (quotientFormatAsString == "sparse") {
- return BisimulationSettings::QuotientFormat::Sparse;
+ return storm::dd::bisimulation::QuotientFormat::Sparse;
}
- return BisimulationSettings::QuotientFormat::Dd;
+ STORM_LOG_ASSERT(quotientFormatAsString == "dd", "Invalid bisimulation quotient format: " << quotientFormatAsString << ".");
+ return storm::dd::bisimulation::QuotientFormat::Dd;
}
bool BisimulationSettings::isUseRepresentativesSet() const {
diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h
index c06713a8a..ff372de01 100644
--- a/src/storm/settings/modules/BisimulationSettings.h
+++ b/src/storm/settings/modules/BisimulationSettings.h
@@ -4,6 +4,7 @@
#include "storm/settings/modules/ModuleSettings.h"
#include "storm/storage/dd/bisimulation/SignatureMode.h"
+#include "storm/storage/dd/bisimulation/QuotientFormat.h"
namespace storm {
namespace settings {
@@ -17,8 +18,6 @@ namespace storm {
// An enumeration of all available bisimulation types.
enum class BisimulationType { Strong, Weak };
- enum class QuotientFormat { Sparse, Dd };
-
enum class ReuseMode { None, BlockNumbers };
enum class InitialPartitionMode { Regular, Finer };
@@ -48,7 +47,7 @@ namespace storm {
* Retrieves the format in which the quotient is to be extracted.
* NOTE: only applies to DD-based bisimulation.
*/
- QuotientFormat getQuotientFormat() const;
+ storm::dd::bisimulation::QuotientFormat getQuotientFormat() const;
/*!
* Retrieves whether representatives for blocks are to be used instead of the block numbers.
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index d43dd9c65..a0eeae5e4 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -129,18 +129,18 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
- std::shared_ptr<storm::models::Model<ExportValueType>> BisimulationDecomposition<DdType, ValueType, ExportValueType>::getQuotient() const {
+ std::shared_ptr<storm::models::Model<ExportValueType>> BisimulationDecomposition<DdType, ValueType, ExportValueType>::getQuotient(storm::dd::bisimulation::QuotientFormat const& quotientFormat) const {
std::shared_ptr<storm::models::Model<ExportValueType>> quotient;
if (this->refiner->getStatus() == Status::FixedPoint) {
STORM_LOG_INFO("Starting full quotient extraction.");
- QuotientExtractor<DdType, ValueType, ExportValueType> extractor;
+ QuotientExtractor<DdType, ValueType, ExportValueType> extractor(quotientFormat);
quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
} else {
STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
STORM_LOG_INFO("Starting partial quotient extraction.");
if (!partialQuotientExtractor) {
- partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>>(model);
+ partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>>(model, quotientFormat);
}
quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h
index 1a552c497..36cee976b 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.h
+++ b/src/storm/storage/dd/BisimulationDecomposition.h
@@ -7,6 +7,7 @@
#include "storm/storage/bisimulation/BisimulationType.h"
#include "storm/storage/dd/bisimulation/SignatureMode.h"
#include "storm/storage/dd/bisimulation/PreservationInformation.h"
+#include "storm/storage/dd/bisimulation/QuotientFormat.h"
#include "storm/logic/Formula.h"
@@ -64,7 +65,7 @@ namespace storm {
/*!
* Retrieves the quotient model after the bisimulation decomposition was computed.
*/
- std::shared_ptr<storm::models::Model<ExportValueType>> getQuotient() const;
+ std::shared_ptr<storm::models::Model<ExportValueType>> getQuotient(storm::dd::bisimulation::QuotientFormat const& quotientFormat) const;
private:
void initialize();
diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
index fea92c755..06c387781 100644
--- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
@@ -16,11 +16,11 @@ namespace storm {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
- PartialQuotientExtractor<DdType, ValueType, ExportValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
- auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
- this->quotientFormat = settings.getQuotientFormat();
-
- STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
+ PartialQuotientExtractor<DdType, ValueType, ExportValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::bisimulation::QuotientFormat const& quotientFormat) : model(model), quotientFormat(quotientFormat) {
+ if (this->quotientFormat != storm::dd::bisimulation::QuotientFormat::Dd) {
+ STORM_LOG_ERROR("Only DD-based partial quotient extraction is currently supported. Switching to DD-based extraction.");
+ this->quotientFormat = storm::dd::bisimulation::QuotientFormat::Dd;
+ }
}
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
@@ -28,7 +28,7 @@ namespace storm {
auto start = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::Model<ExportValueType>> result;
- STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
+ STORM_LOG_THROW(this->quotientFormat == storm::dd::bisimulation::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
result = extractDdQuotient(partition, preservationInformation);
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
index d5c638c2a..df38bf696 100644
--- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
+++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
@@ -19,7 +19,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class PartialQuotientExtractor {
public:
- PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model);
+ PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::bisimulation::QuotientFormat const& quotientFormat);
std::shared_ptr<storm::models::Model<ExportValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
@@ -29,7 +29,7 @@ namespace storm {
// The model for which to compute the partial quotient.
storm::models::symbolic::Model<DdType, ValueType> const& model;
- storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat;
+ storm::dd::bisimulation::QuotientFormat quotientFormat;
};
}
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index 36f7f1fe3..ed94fbff8 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -818,18 +818,17 @@ namespace storm {
};
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
- QuotientExtractor<DdType, ValueType, ExportValueType>::QuotientExtractor() : useRepresentatives(false) {
+ QuotientExtractor<DdType, ValueType, ExportValueType>::QuotientExtractor(storm::dd::bisimulation::QuotientFormat const& quotientFormat) : useRepresentatives(false), quotientFormat(quotientFormat) {
auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
this->useRepresentatives = settings.isUseRepresentativesSet();
this->useOriginalVariables = settings.isUseOriginalVariablesSet();
- this->quotientFormat = settings.getQuotientFormat();
}
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::Model<ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto start = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::Model<ExportValueType>> result;
- if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) {
+ if (quotientFormat == storm::dd::bisimulation::QuotientFormat::Sparse) {
result = extractSparseQuotient(model, partition, preservationInformation);
} else {
result = extractDdQuotient(model, partition, preservationInformation);
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
index 422453bf7..2ecfe41a3 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
@@ -19,7 +19,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class QuotientExtractor {
public:
- QuotientExtractor();
+ QuotientExtractor(storm::dd::bisimulation::QuotientFormat const& quotientFormat);
std::shared_ptr<storm::models::Model<ExportValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
@@ -32,7 +32,7 @@ namespace storm {
bool useRepresentatives;
bool useOriginalVariables;
- storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat;
+ storm::dd::bisimulation::QuotientFormat quotientFormat;
};
}
diff --git a/src/storm/storage/dd/bisimulation/QuotientFormat.h b/src/storm/storage/dd/bisimulation/QuotientFormat.h
new file mode 100644
index 000000000..5ce91bd07
--- /dev/null
+++ b/src/storm/storage/dd/bisimulation/QuotientFormat.h
@@ -0,0 +1,9 @@
+#pragma once
+
+namespace storm {
+ namespace dd {
+ namespace bisimulation {
+ enum class QuotientFormat { Sparse, Dd };
+ }
+ }
+}
diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
index 26e7f684c..e7a1a8e45 100644
--- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
+++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
@@ -35,7 +35,7 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(11ul, quotient->getNumberOfStates());
EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
@@ -50,7 +50,7 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(5ul, quotient->getNumberOfStates());
EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
@@ -65,7 +65,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
@@ -92,7 +92,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
// Perform only one step.
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>();
@@ -112,7 +112,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
// Perform only one step.
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>();
@@ -132,7 +132,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>();
@@ -155,7 +155,7 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(11ul, quotient->getNumberOfStates());
EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
@@ -170,7 +170,7 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(5ul, quotient->getNumberOfStates());
EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
@@ -185,7 +185,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
@@ -212,7 +212,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) {
// Perform only one step.
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>();
@@ -232,7 +232,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) {
// Perform only one step.
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>();
@@ -252,7 +252,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) {
decomposition.compute(1);
- quotient = decomposition.getQuotient();
+ quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
ASSERT_TRUE(quotient->isSymbolicModel());
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>();
@@ -278,7 +278,7 @@ TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(2007ul, quotient->getNumberOfStates());
EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
@@ -293,7 +293,7 @@ TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(65ul, quotient->getNumberOfStates());
EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
@@ -311,7 +311,7 @@ TEST(SymbolicModelBisimulationDecomposition, Crowds_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(2007ul, quotient->getNumberOfStates());
EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
@@ -326,7 +326,7 @@ TEST(SymbolicModelBisimulationDecomposition, Crowds_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(65ul, quotient->getNumberOfStates());
EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
@@ -341,7 +341,7 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(77ul, quotient->getNumberOfStates());
EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
@@ -357,7 +357,7 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(11ul, quotient->getNumberOfStates());
EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
@@ -373,7 +373,7 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(77ul, quotient->getNumberOfStates());
EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
@@ -389,7 +389,7 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(11ul, quotient->getNumberOfStates());
EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
@@ -411,7 +411,7 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(252ul, quotient->getNumberOfStates());
EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
@@ -424,7 +424,7 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(1107ul, quotient->getNumberOfStates());
EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
@@ -446,7 +446,7 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
decomposition.compute();
- std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+ std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(252ul, quotient->getNumberOfStates());
EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
@@ -459,7 +459,7 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Sylvan) {
storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
decomposition2.compute();
- quotient = decomposition2.getQuotient();
+ quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
EXPECT_EQ(1107ul, quotient->getNumberOfStates());
EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());