diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index bdba45a30..7618fd9e3 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -277,8 +277,6 @@ namespace storm {
model = model.preprocess(constantDefinitions);
-
-
if (ioSettings.isNoBuildModelSet()) {
return;
}
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index d75065299..81ecad8a4 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -20,7 +20,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
- : ModelBase(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling),
+ : storm::models::Model<ValueType>(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling),
rewardModels(rewardModels), choiceLabeling(optionalChoiceLabeling) {
for (auto const& rewardModel : this->getRewardModels()) {
STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -33,7 +33,7 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
- : ModelBase(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)),
+ : storm::models::Model<ValueType>(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)),
rewardModels(std::move(rewardModels)), choiceLabeling(std::move(optionalChoiceLabeling)) {
for (auto const& rewardModel : this->getRewardModels()) {
STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h
index a545ae3ce..57382a1c9 100644
--- a/src/storm/models/sparse/Model.h
+++ b/src/storm/models/sparse/Model.h
@@ -6,7 +6,7 @@
#include <boost/container/flat_set.hpp>
#include <boost/optional.hpp>
-#include "storm/models/ModelBase.h"
+#include "storm/models/Model.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/SparseMatrix.h"
@@ -35,7 +35,7 @@ namespace storm {
* Base class for all sparse models.
*/
template<class CValueType, class CRewardModelType = StandardRewardModel<CValueType>>
- class Model : public storm::models::ModelBase {
+ class Model : public storm::models::Model<CValueType> {
template<typename ParametricModelType, typename ConstantModelType>
friend class storm::utility::ModelInstantiator;
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 1ec8ef7d9..2a6804618 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -35,7 +35,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
- : ModelBase(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) {
+ : storm::models::Model<ValueType>(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) {
this->labelToBddMap.emplace("init", initialStates);
this->labelToBddMap.emplace("deadlock", deadlockStates);
}
@@ -52,7 +52,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
- : ModelBase(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(nullptr), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToBddMap(labelToBddMap), rewardModels(rewardModels) {
+ : storm::models::Model<ValueType>(modelType), manager(manager), reachableStates(reachableStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(nullptr), columnVariables(columnVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToBddMap(labelToBddMap), rewardModels(rewardModels) {
STORM_LOG_THROW(this->labelToBddMap.find("init") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException, "Illegal custom label 'init'.");
STORM_LOG_THROW(this->labelToBddMap.find("deadlock") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException, "Illegal custom label 'deadlock'.");
this->labelToBddMap.emplace("init", initialStates);
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index cae2e3c85..f12a7ad26 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -10,7 +10,7 @@
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/Bdd.h"
-#include "storm/models/ModelBase.h"
+#include "storm/models/Model.h"
#include "storm/utility/OsDetection.h"
#include "storm-config.h"
@@ -45,7 +45,7 @@ namespace storm {
* Base class for all symbolic models.
*/
template<storm::dd::DdType Type, typename CValueType = double>
- class Model : public storm::models::ModelBase {
+ class Model : public storm::models::Model<CValueType> {
public:
typedef CValueType ValueType;
diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp
index fdef27093..2c1db8a39 100644
--- a/src/storm/settings/modules/BisimulationSettings.cpp
+++ b/src/storm/settings/modules/BisimulationSettings.cpp
@@ -22,7 +22,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build());
std::vector<std::string> quotTypes = { "sparse", "dd" };
- this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
}
@@ -42,7 +42,7 @@ namespace storm {
}
BisimulationSettings::QuotientFormat BisimulationSettings::getQuotientFormat() const {
- std::string quotientFormatAsString = this->getOption(typeOptionName).getArgumentByName("format").getValueAsString();
+ std::string quotientFormatAsString = this->getOption(quotientFormatOptionName).getArgumentByName("format").getValueAsString();
if (quotientFormatAsString == "sparse") {
return BisimulationSettings::QuotientFormat::Sparse;
}
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index d71fa7ba4..11878f0d2 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -125,41 +125,47 @@ namespace storm {
// the insertion.
bool fixCurrentRow = row == lastRow && column < lastColumn;
- // If we switched to another row, we have to adjust the missing entries in the row indices vector.
- if (row != lastRow) {
- // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
- for (index_type i = lastRow + 1; i <= row; ++i) {
- rowIndications.push_back(currentEntryCount);
+ // If the element is in the same row and column as the previous entry, we add them up.
+ if (row == lastRow && column == lastColumn) {
+ columnsAndValues.back().setColumn(column);
+ columnsAndValues.back().setValue(value);
+ } else {
+ // If we switched to another row, we have to adjust the missing entries in the row indices vector.
+ if (row != lastRow) {
+ // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
+ for (index_type i = lastRow + 1; i <= row; ++i) {
+ rowIndications.push_back(currentEntryCount);
+ }
+
+ lastRow = row;
}
- lastRow = row;
- }
-
- lastColumn = column;
-
- // Finally, set the element and increase the current size.
- columnsAndValues.emplace_back(column, value);
- highestColumn = std::max(highestColumn, column);
- ++currentEntryCount;
-
- // If we need to fix the row, do so now.
- if (fixCurrentRow) {
- // First, we sort according to columns.
- std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
- return a.getColumn() < b.getColumn();
- });
+ lastColumn = column;
- // Then, we eliminate possible duplicate entries.
- auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
- return a.getColumn() == b.getColumn();
- });
+ // Finally, set the element and increase the current size.
+ columnsAndValues.emplace_back(column, value);
+ highestColumn = std::max(highestColumn, column);
+ ++currentEntryCount;
- // Finally, remove the superfluous elements.
- std::size_t elementsToRemove = std::distance(it, columnsAndValues.end());
- if (elementsToRemove > 0) {
- STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries.");
- currentEntryCount -= elementsToRemove;
- columnsAndValues.resize(columnsAndValues.size() - elementsToRemove);
+ // If we need to fix the row, do so now.
+ if (fixCurrentRow) {
+ // First, we sort according to columns.
+ std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+ return a.getColumn() < b.getColumn();
+ });
+
+ // Then, we eliminate possible duplicate entries.
+ auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+ return a.getColumn() == b.getColumn();
+ });
+
+ // Finally, remove the superfluous elements.
+ std::size_t elementsToRemove = std::distance(it, columnsAndValues.end());
+ if (elementsToRemove > 0) {
+ STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries.");
+ currentEntryCount -= elementsToRemove;
+ columnsAndValues.resize(columnsAndValues.size() - elementsToRemove);
+ }
}
}
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index a1698404a..81ad026af 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -82,12 +82,12 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
+ std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
STORM_LOG_THROW(this->status == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed.");
STORM_LOG_TRACE("Starting quotient extraction.");
QuotientExtractor<DdType, ValueType> extractor;
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> quotient = extractor.extract(model, currentPartition);
+ std::shared_ptr<storm::models::Model<ValueType>> quotient = extractor.extract(model, currentPartition);
STORM_LOG_TRACE("Quotient extraction done.");
return quotient;
diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h
index e0ec00d27..d13d6a114 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.h
+++ b/src/storm/storage/dd/BisimulationDecomposition.h
@@ -33,7 +33,7 @@ namespace storm {
/*!
* Retrieves the quotient model after the bisimulation decomposition was computed.
*/
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> getQuotient() const;
+ std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
private:
// The status of the computation.
diff --git a/src/storm/storage/dd/DdMetaVariable.cpp b/src/storm/storage/dd/DdMetaVariable.cpp
index 440612d7c..fda284391 100644
--- a/src/storm/storage/dd/DdMetaVariable.cpp
+++ b/src/storm/storage/dd/DdMetaVariable.cpp
@@ -49,6 +49,28 @@ namespace storm {
return this->cube;
}
+ template<DdType LibraryType>
+ std::vector<uint64_t> DdMetaVariable<LibraryType>::getIndices() const {
+ std::vector<std::pair<uint64_t, uint64_t>> indicesAndLevels = this->getIndicesAndLevels();
+ std::sort(indicesAndLevels.begin(), indicesAndLevels.end(), [] (std::pair<uint64_t, uint64_t> const& a, std::pair<uint64_t, uint64_t> const& b) { return a.second < b.second; });
+
+ std::vector<uint64_t> indices;
+ for (auto const& e : indicesAndLevels) {
+ indices.emplace_back(e.first);
+ }
+
+ return indices;
+ }
+
+ template<DdType LibraryType>
+ std::vector<std::pair<uint64_t, uint64_t>> DdMetaVariable<LibraryType>::getIndicesAndLevels() const {
+ std::vector<std::pair<uint64_t, uint64_t>> indicesAndLevels;
+ for (auto const& v : ddVariables) {
+ indicesAndLevels.emplace_back(v.getIndex(), v.getLevel());
+ }
+ return indicesAndLevels;
+ }
+
template<DdType LibraryType>
uint64_t DdMetaVariable<LibraryType>::getHighestLevel() const {
uint64_t result = 0;
diff --git a/src/storm/storage/dd/DdMetaVariable.h b/src/storm/storage/dd/DdMetaVariable.h
index 9b9b736ed..c18f9fa44 100644
--- a/src/storm/storage/dd/DdMetaVariable.h
+++ b/src/storm/storage/dd/DdMetaVariable.h
@@ -78,6 +78,16 @@ namespace storm {
*/
uint64_t getHighestLevel() const;
+ /*!
+ * Retrieves the indices of the DD variables associated with this meta variable sorted by level.
+ */
+ std::vector<uint64_t> getIndices() const;
+
+ /*!
+ * Retrieves the indices and levels of the DD variables associated with this meta variable.
+ */
+ std::vector<std::pair<uint64_t, uint64_t>> getIndicesAndLevels() const;
+
private:
/*!
* Creates an integer meta variable with the given name and range bounds.
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index bef5d3fc3..a59eed3bd 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -6,6 +6,10 @@
#include "storm/models/symbolic/Ctmc.h"
#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+
#include "storm/storage/dd/bisimulation/PreservationInformation.h"
#include "storm/settings/SettingsManager.h"
@@ -13,10 +17,452 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/BitVector.h"
+
+#include <sparsepp/spp.h>
+
namespace storm {
namespace dd {
namespace bisimulation {
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ class InternalSparseQuotientExtractor;
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ class InternalSparseQuotientExtractorBase {
+ public:
+ InternalSparseQuotientExtractorBase(storm::dd::DdManager<DdType> const& manager, std::set<storm::expressions::Variable> const& stateVariables) : manager(manager) {
+ for (auto const& variable : stateVariables) {
+ auto const& ddMetaVariable = manager.getMetaVariable(variable);
+ std::vector<std::pair<uint64_t, uint64_t>> indicesAndLevels = ddMetaVariable.getIndicesAndLevels();
+ stateVariablesIndicesAndLevels.insert(stateVariablesIndicesAndLevels.end(), indicesAndLevels.begin(), indicesAndLevels.end());
+ }
+
+ // Sort the indices by their levels.
+ std::sort(stateVariablesIndicesAndLevels.begin(), stateVariablesIndicesAndLevels.end(), [] (std::pair<uint64_t, uint64_t> const& a, std::pair<uint64_t, uint64_t> const& b) { return a.second < b.second; } );
+ }
+
+ protected:
+ storm::storage::SparseMatrix<ValueType> createMatrixFromEntries(Partition<DdType, ValueType> const& partition) {
+ for (auto& row : entries) {
+ std::sort(row.begin(), row.end(), [] (storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& a, storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& b) { return a.getColumn() < b.getColumn(); } );
+ }
+
+ storm::storage::SparseMatrixBuilder<ValueType> builder(partition.getNumberOfBlocks(), partition.getNumberOfBlocks());
+ uint64_t rowCounter = 0;
+ for (auto& row : entries) {
+ for (auto const& entry : row) {
+ builder.addNextValue(rowCounter, entry.getColumn(), entry.getValue());
+ }
+
+ // Free storage for row.
+ row.clear();
+ row.shrink_to_fit();
+
+ ++rowCounter;
+ }
+
+ return builder.build();
+ }
+
+ storm::dd::DdManager<DdType> const& manager;
+ std::vector<std::pair<uint64_t, uint64_t>> stateVariablesIndicesAndLevels;
+ std::vector<std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>> entries;
+ };
+ template<typename ValueType>
+ class InternalSparseQuotientExtractor<storm::dd::DdType::CUDD, ValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::CUDD, ValueType> {
+ public:
+ InternalSparseQuotientExtractor(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, std::set<storm::expressions::Variable> const& stateVariables) : InternalSparseQuotientExtractorBase<storm::dd::DdType::CUDD, ValueType>(manager, stateVariables), ddman(this->manager.getInternalDdManager().getCuddManager().getManager()) {
+ // Intentionally left empty.
+ }
+
+ storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& transitionMatrix, Partition<storm::dd::DdType::CUDD, ValueType> const& partition) {
+ STORM_LOG_ASSERT(partition.storedAsAdd(), "Expected partition stored as ADD.");
+
+ // Create the number of rows necessary for the matrix.
+ this->entries.resize(partition.getNumberOfBlocks());
+
+ storm::storage::BitVector encoding(this->stateVariablesIndicesAndLevels.size());
+ extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), 0, encoding);
+
+ return this->createMatrixFromEntries(partition);
+ }
+
+ storm::storage::BitVector extractStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& states, Partition<storm::dd::DdType::CUDD, ValueType> const& partition) {
+ STORM_LOG_ASSERT(partition.storedAsAdd(), "Expected partition stored as ADD.");
+
+ storm::storage::BitVector result(partition.getNumberOfBlocks());
+ extractStatesRec(states.getInternalBdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), 0, result);
+
+ return result;
+ }
+
+ private:
+ uint64_t decodeBlockIndex(DdNode* blockEncoding) {
+ std::unique_ptr<uint64_t>& blockCacheEntry = blockDecodeCache[blockEncoding];
+ if (blockCacheEntry) {
+ return *blockCacheEntry;
+ }
+
+ uint64_t result = 0;
+ uint64_t offset = 0;
+ while (blockEncoding != Cudd_ReadOne(ddman)) {
+ if (Cudd_T(blockEncoding) != Cudd_ReadZero(ddman)) {
+ blockEncoding = Cudd_T(blockEncoding);
+ result |= 1ull << offset;
+ } else {
+ blockEncoding = Cudd_E(blockEncoding);
+ }
+ ++offset;
+ }
+
+ blockCacheEntry.reset(new uint64_t(result));
+
+ return result;
+ }
+
+ void extractStatesRec(DdNode* statesNode, DdNode* partitionNode, uint64_t offset, storm::storage::BitVector& result) {
+ if (statesNode == Cudd_ReadLogicZero(ddman)) {
+ return;
+ }
+
+ // Determine the levels in the DDs.
+ uint64_t statesVariable = Cudd_NodeReadIndex(statesNode);
+ uint64_t partitionVariable = Cudd_NodeReadIndex(partitionNode) - 1;
+
+ // See how many variables we skipped.
+ while (offset < this->stateVariablesIndicesAndLevels.size() && statesVariable != this->stateVariablesIndicesAndLevels[offset].first && partitionVariable != this->stateVariablesIndicesAndLevels[offset].first) {
+ ++offset;
+ }
+
+ if (offset == this->stateVariablesIndicesAndLevels.size()) {
+ result.set(decodeBlockIndex(partitionNode));
+ return;
+ }
+
+ uint64_t topVariable;
+ if (statesVariable == this->stateVariablesIndicesAndLevels[offset].first) {
+ topVariable = statesVariable;
+ } else {
+ topVariable = partitionVariable;
+ }
+
+ DdNode* tStates = statesNode;
+ DdNode* eStates = statesNode;
+ bool negate = false;
+ if (topVariable == statesVariable) {
+ tStates = Cudd_T(statesNode);
+ eStates = Cudd_E(statesNode);
+ negate = Cudd_IsComplement(statesNode);
+ }
+
+ DdNode* tPartition = partitionNode;
+ DdNode* ePartition = partitionNode;
+ if (topVariable == partitionVariable) {
+ tPartition = Cudd_T(partitionNode);
+ ePartition = Cudd_E(partitionNode);
+ }
+
+ extractStatesRec(negate ? Cudd_Not(tStates) : tStates, tPartition, offset, result);
+ extractStatesRec(negate ? Cudd_Not(eStates) : eStates, ePartition, offset, result);
+ }
+
+ void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState) {
+ // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero
+ // as all states of the model have to be contained.
+ if (transitionMatrixNode == Cudd_ReadZero(ddman)) {
+ return;
+ }
+
+ // If we have moved through all source variables, we must have arrived at a constant.
+ if (currentIndex == sourceState.size()) {
+ // Decode the source block.
+ uint64_t sourceBlockIndex = decodeBlockIndex(sourcePartitionNode);
+
+ std::unique_ptr<storm::storage::BitVector>& sourceRepresentative = uniqueSourceRepresentative[sourceBlockIndex];
+ if (sourceRepresentative && *sourceRepresentative != sourceState) {
+ // In this case, we have picked a different representative and must not record any entries now.
+ return;
+ }
+
+ // Otherwise, we record the new representative.
+ sourceRepresentative.reset(new storm::storage::BitVector(sourceState));
+
+ // Decode the target block.
+ uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode);
+
+ this->entries[sourceBlockIndex].emplace_back(targetBlockIndex, Cudd_V(transitionMatrixNode));
+ } else {
+ // Determine the levels in the DDs.
+ uint64_t transitionMatrixVariable = Cudd_NodeReadIndex(transitionMatrixNode);
+ uint64_t sourcePartitionVariable = Cudd_NodeReadIndex(sourcePartitionNode) - 1;
+ uint64_t targetPartitionVariable = Cudd_NodeReadIndex(targetPartitionNode) - 1;
+
+ // Move through transition matrix.
+ DdNode* tt = transitionMatrixNode;
+ DdNode* te = transitionMatrixNode;
+ DdNode* et = transitionMatrixNode;
+ DdNode* ee = transitionMatrixNode;
+ if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ DdNode* t = Cudd_T(transitionMatrixNode);
+ DdNode* e = Cudd_E(transitionMatrixNode);
+
+ uint64_t tVariable = Cudd_NodeReadIndex(t);
+ if (tVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ tt = Cudd_T(t);
+ te = Cudd_E(t);
+ } else {
+ tt = te = t;
+ }
+
+ uint64_t eVariable = Cudd_NodeReadIndex(e);
+ if (eVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ et = Cudd_T(e);
+ ee = Cudd_E(e);
+ } else {
+ et = ee = e;
+ }
+ } else {
+ if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ tt = Cudd_T(transitionMatrixNode);
+ te = Cudd_E(transitionMatrixNode);
+ } else {
+ tt = te = transitionMatrixNode;
+ }
+ }
+
+ // Move through partition (for source state).
+ DdNode* sourceT;
+ DdNode* sourceE;
+ if (sourcePartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ sourceT = Cudd_T(sourcePartitionNode);
+ sourceE = Cudd_E(sourcePartitionNode);
+ } else {
+ sourceT = sourceE = sourcePartitionNode;
+ }
+
+ // Move through partition (for target state).
+ DdNode* targetT;
+ DdNode* targetE;
+ if (targetPartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ targetT = Cudd_T(targetPartitionNode);
+ targetE = Cudd_E(targetPartitionNode);
+ } else {
+ targetT = targetE = targetPartitionNode;
+ }
+
+ sourceState.set(currentIndex, true);
+ extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState);
+ extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState);
+
+ sourceState.set(currentIndex, false);
+ extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState);
+ extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState);
+ }
+ }
+
+ ::DdManager* ddman;
+
+ spp::sparse_hash_map<uint64_t, std::unique_ptr<storm::storage::BitVector>> uniqueSourceRepresentative;
+ spp::sparse_hash_map<DdNode const*, std::unique_ptr<uint64_t>> blockDecodeCache;
+ };
+
+ template<typename ValueType>
+ class InternalSparseQuotientExtractor<storm::dd::DdType::Sylvan, ValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType> {
+ public:
+ InternalSparseQuotientExtractor(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, std::set<storm::expressions::Variable> const& stateVariables) : InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType>(manager, stateVariables) {
+ // Intentionally left empty.
+ }
+
+ storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& transitionMatrix, Partition<storm::dd::DdType::Sylvan, ValueType> const& partition) {
+ STORM_LOG_ASSERT(partition.storedAsBdd(), "Expected partition stored as BDD.");
+
+ // Create the number of rows necessary for the matrix.
+ this->entries.resize(partition.getNumberOfBlocks());
+
+ storm::storage::BitVector encoding(this->stateVariablesIndicesAndLevels.size());
+ extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), 0, encoding);
+
+ return this->createMatrixFromEntries(partition);
+ }
+
+ storm::storage::BitVector extractStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& states, Partition<storm::dd::DdType::Sylvan, ValueType> const& partition) {
+ STORM_LOG_ASSERT(partition.storedAsBdd(), "Expected partition stored as BDD.");
+
+ storm::storage::BitVector result(partition.getNumberOfBlocks());
+ extractStatesRec(states.getInternalBdd().getSylvanBdd().GetBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), 0, result);
+
+ return result;
+ }
+
+ private:
+ uint64_t decodeBlockIndex(BDD blockEncoding) {
+ std::unique_ptr<uint64_t>& blockCacheEntry = blockDecodeCache[blockEncoding];
+ if (blockCacheEntry) {
+ return *blockCacheEntry;
+ }
+
+ uint64_t result = 0;
+ uint64_t offset = 0;
+ while (blockEncoding != sylvan_true) {
+ if (sylvan_high(blockEncoding) != sylvan_false) {
+ blockEncoding = sylvan_high(blockEncoding);
+ result |= 1ull << offset;
+ } else {
+ blockEncoding = sylvan_low(blockEncoding);
+ }
+ ++offset;
+ }
+
+ blockCacheEntry.reset(new uint64_t(result));
+
+ return result;
+ }
+
+ void extractStatesRec(BDD statesNode, BDD partitionNode, uint64_t offset, storm::storage::BitVector& result) {
+ if (statesNode == sylvan_false) {
+ return;
+ }
+
+ // Determine the levels in the DDs.
+ uint64_t statesVariable = sylvan_isconst(statesNode) ? 0xffffffff : sylvan_var(statesNode);
+ uint64_t partitionVariable = sylvan_var(partitionNode) - 1;
+
+ // See how many variables we skipped.
+ while (offset < this->stateVariablesIndicesAndLevels.size() && statesVariable != this->stateVariablesIndicesAndLevels[offset].first && partitionVariable != this->stateVariablesIndicesAndLevels[offset].first) {
+ ++offset;
+ }
+
+ if (offset == this->stateVariablesIndicesAndLevels.size()) {
+ result.set(decodeBlockIndex(partitionNode));
+ return;
+ }
+
+ uint64_t topVariable;
+ if (statesVariable == this->stateVariablesIndicesAndLevels[offset].first) {
+ topVariable = statesVariable;
+ } else {
+ topVariable = partitionVariable;
+ }
+
+ BDD tStates = statesNode;
+ BDD eStates = statesNode;
+ if (topVariable == statesVariable) {
+ tStates = sylvan_high(statesNode);
+ eStates = sylvan_low(statesNode);
+ }
+
+ BDD tPartition = partitionNode;
+ BDD ePartition = partitionNode;
+ if (topVariable == partitionVariable) {
+ tPartition = sylvan_high(partitionNode);
+ ePartition = sylvan_low(partitionNode);
+ }
+
+ extractStatesRec(tStates, tPartition, offset, result);
+ extractStatesRec(eStates, ePartition, offset, result);
+ }
+
+ void extractTransitionMatrixRec(MTBDD transitionMatrixNode, BDD sourcePartitionNode, BDD targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState) {
+ // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero
+ // as all states of the model have to be contained.
+ if (mtbdd_iszero(transitionMatrixNode)) {
+ return;
+ }
+
+ // If we have moved through all source variables, we must have arrived at a constant.
+ if (currentIndex == sourceState.size()) {
+ // Decode the source block.
+ uint64_t sourceBlockIndex = decodeBlockIndex(sourcePartitionNode);
+
+ std::unique_ptr<storm::storage::BitVector>& sourceRepresentative = uniqueSourceRepresentative[sourceBlockIndex];
+ if (sourceRepresentative && *sourceRepresentative != sourceState) {
+ // In this case, we have picked a different representative and must not record any entries now.
+ return;
+ }
+
+ // Otherwise, we record the new representative.
+ sourceRepresentative.reset(new storm::storage::BitVector(sourceState));
+
+ // Decode the target block.
+ uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode);
+
+ this->entries[sourceBlockIndex].emplace_back(targetBlockIndex, storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode));
+ } else {
+ // Determine the levels in the DDs.
+ uint64_t transitionMatrixVariable = sylvan_isconst(transitionMatrixNode) ? 0xffffffff : sylvan_var(transitionMatrixNode);
+ uint64_t sourcePartitionVariable = sylvan_var(sourcePartitionNode) - 1;
+ uint64_t targetPartitionVariable = sylvan_var(targetPartitionNode) - 1;
+
+ // Move through transition matrix.
+ MTBDD tt = transitionMatrixNode;
+ MTBDD te = transitionMatrixNode;
+ MTBDD et = transitionMatrixNode;
+ MTBDD ee = transitionMatrixNode;
+ if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ MTBDD t = sylvan_high(transitionMatrixNode);
+ MTBDD e = sylvan_low(transitionMatrixNode);
+
+ uint64_t tVariable = sylvan_isconst(t) ? 0xffffffff : sylvan_var(t);
+ if (tVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ tt = sylvan_high(t);
+ te = sylvan_low(t);
+ } else {
+ tt = te = t;
+ }
+
+ uint64_t eVariable = sylvan_isconst(e) ? 0xffffffff : sylvan_var(e);
+ if (eVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ et = sylvan_high(e);
+ ee = sylvan_low(e);
+ } else {
+ et = ee = e;
+ }
+ } else {
+ if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
+ tt = sylvan_high(transitionMatrixNode);
+ te = sylvan_low(transitionMatrixNode);
+ } else {
+ tt = te = transitionMatrixNode;
+ }
+ }
+
+ // Move through partition (for source state).
+ MTBDD sourceT;
+ MTBDD sourceE;
+ if (sourcePartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ sourceT = sylvan_high(sourcePartitionNode);
+ sourceE = sylvan_low(sourcePartitionNode);
+ } else {
+ sourceT = sourceE = sourcePartitionNode;
+ }
+
+ // Move through partition (for target state).
+ MTBDD targetT;
+ MTBDD targetE;
+ if (targetPartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
+ targetT = sylvan_high(targetPartitionNode);
+ targetE = sylvan_low(targetPartitionNode);
+ } else {
+ targetT = targetE = targetPartitionNode;
+ }
+
+ sourceState.set(currentIndex, true);
+ extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState);
+ extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState);
+
+ sourceState.set(currentIndex, false);
+ extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState);
+ extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState);
+ }
+ }
+
+ spp::sparse_hash_map<uint64_t, std::unique_ptr<storm::storage::BitVector>> uniqueSourceRepresentative;
+ spp::sparse_hash_map<BDD, std::unique_ptr<uint64_t>> blockDecodeCache;
+ };
+
template<storm::dd::DdType DdType, typename ValueType>
QuotientExtractor<DdType, ValueType>::QuotientExtractor() : useRepresentatives(false) {
auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
@@ -25,9 +471,9 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition) {
+ std::shared_ptr<storm::models::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition) {
auto start = std::chrono::high_resolution_clock::now();
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
+ std::shared_ptr<storm::models::Model<ValueType>> result;
if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) {
result = extractSparseQuotient(model, partition);
} else {
@@ -35,12 +481,51 @@ namespace storm {
}
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.");
+
+ STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted.");
+
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition) {
- return nullptr;
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition) {
+ InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model.getManager(), model.getRowVariables());
+ storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix(), partition);
+
+ std::cout << "Matrix has " << quotientTransitionMatrix.getEntryCount() << " entries" << std::endl;
+
+ storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks());
+ quotientStateLabeling.addLabel("init", sparseExtractor.extractStates(model.getInitialStates(), partition));
+ std::cout << "init: " << quotientStateLabeling.getStates("init").getNumberOfSetBits() << std::endl;
+ quotientStateLabeling.addLabel("deadlock", sparseExtractor.extractStates(model.getDeadlockStates(), partition));
+ std::cout << "deadlock: " << quotientStateLabeling.getStates("init").getNumberOfSetBits() << std::endl;
+
+ for (auto const& label : partition.getPreservationInformation().getLabels()) {
+ quotientStateLabeling.addLabel(label, sparseExtractor.extractStates(model.getStates(label), partition));
+ std::cout << label << ": " << quotientStateLabeling.getStates(label).getNumberOfSetBits() << std::endl;
+ }
+ for (auto const& expression : partition.getPreservationInformation().getExpressions()) {
+ std::stringstream stream;
+ stream << expression;
+ std::string expressionAsString = stream.str();
+
+ if (quotientStateLabeling.containsLabel(expressionAsString)) {
+ STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition.");
+ } else {
+ quotientStateLabeling.addLabel(stream.str(), sparseExtractor.extractStates(model.getStates(expression), partition));
+ std::cout << stream.str() << ": " << quotientStateLabeling.getStates(stream.str()).getNumberOfSetBits() << std::endl;
+ }
+ }
+
+
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
+ if (model.getType() == storm::models::ModelType::Dtmc) {
+ result = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling));
+ } else if (model.getType() == storm::models::ModelType::Ctmc) {
+ result = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling));
+ }
+
+ return result;
}
template<storm::dd::DdType DdType, typename ValueType>
@@ -65,10 +550,14 @@ namespace storm {
}
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
+ auto start = std::chrono::high_resolution_clock::now();
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables());
quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables());
+ auto end = std::chrono::high_resolution_clock::now();
+ STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
+ start = std::chrono::high_resolution_clock::now();
storm::dd::Bdd<DdType> partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables());
@@ -90,7 +579,9 @@ namespace storm {
preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()));
}
}
-
+ end = std::chrono::high_resolution_clock::now();
+ STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
} else {
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
index eb6cbef4b..14b518016 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
@@ -5,6 +5,7 @@
#include "storm/storage/dd/DdType.h"
#include "storm/models/symbolic/Model.h"
+#include "storm/models/sparse/Model.h"
#include "storm/storage/dd/bisimulation/Partition.h"
@@ -19,10 +20,10 @@ namespace storm {
public:
QuotientExtractor();
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
+ std::shared_ptr<storm::models::Model<ValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
private:
- std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition);
diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h
index 8e7c1a34f..b37499898 100644
--- a/src/storm/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h
@@ -595,7 +595,6 @@ namespace storm {
InternalDdManager<DdType::CUDD> const& getInternalDdManager() const;
- private:
/*!
* Retrieves the CUDD ADD object associated with this ADD.
*
@@ -610,6 +609,7 @@ namespace storm {
*/
DdNode* getCuddDdNode() const;
+ private:
/*!
* Performs a recursive step to perform the given function between the given DD-based vector and the given
* explicit vector.
diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h
index 3ca4f47d7..005404e8e 100644
--- a/src/storm/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h
@@ -387,7 +387,6 @@ namespace storm {
friend struct std::hash<storm::dd::InternalBdd<storm::dd::DdType::CUDD>>;
- private:
/*!
* Retrieves the CUDD BDD object associated with this DD.
*
@@ -402,6 +401,7 @@ namespace storm {
*/
DdNode* getCuddDdNode() const;
+ private:
/*!
* Builds a BDD representing the values that make the given filter function evaluate to true.
*
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
index 86f76ed3f..8ecc880e5 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
+++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
@@ -605,6 +605,13 @@ namespace storm {
*/
sylvan::Mtbdd getSylvanMtbdd() const;
+ /*!
+ * Retrieves the value of the given node (that must be a leaf).
+ *
+ * @return The value of the leaf.
+ */
+ static ValueType getValue(MTBDD const& node);
+
private:
/*!
* Recursively builds the ODD from an ADD.
@@ -733,13 +740,6 @@ namespace storm {
static MTBDD getLeaf(storm::RationalFunction const& value);
#endif
- /*!
- * Retrieves the value of the given node (that must be a leaf).
- *
- * @return The value of the leaf.
- */
- static ValueType getValue(MTBDD const& node);
-
// The manager responsible for this MTBDD.
InternalDdManager<DdType::Sylvan> const* ddManager;
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index ec026968f..448bbcd39 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -29,6 +29,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
+
this->odd = symbolicDtmc.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(this->odd, this->odd);
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index a913917be..614759395 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -194,7 +194,7 @@ namespace storm {
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
storm::dd::BisimulationDecomposition<LibraryType, ValueType> decomposition(*result, formulas);
decomposition.compute();
- result = decomposition.getQuotient();
+ result = std::dynamic_pointer_cast<storm::models::symbolic::Model<LibraryType, ValueType>>(decomposition.getQuotient());
}
return result;