diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
index 20acf5854..6f63f7a70 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
@@ -503,6 +503,9 @@ typedef void (*DD_TOHFP)(DdManager *, void *);
extern "C" {
#endif
+// Make this visible to the outside.
+extern DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E);
+
extern DdNode * Cudd_addNewVar(DdManager *dd);
extern DdNode * Cudd_addNewVarAtLevel(DdManager *dd, int level);
extern DdNode * Cudd_bddNewVar(DdManager *dd);
diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp
index c74cb60cb..5e25b5530 100644
--- a/src/storm/abstraction/AbstractionInformation.cpp
+++ b/src/storm/abstraction/AbstractionInformation.cpp
@@ -499,7 +499,7 @@ namespace storm {
allSuccessorLocationVariables.insert(newMetaVariable.second);
successorVariables.insert(newMetaVariable.second);
extendedPredicateDdVariables.emplace_back(newMetaVariable);
- allLocationIdentities &= ddManager->template getIdentity<uint64_t>(newMetaVariable.first).equals(ddManager->template getIdentity<uint64_t>(newMetaVariable.second)) && ddManager->getRange(newMetaVariable.first) && ddManager->getRange(newMetaVariable.second);
+ allLocationIdentities &= ddManager->getIdentity(newMetaVariable.first, newMetaVariable.second);
return std::make_pair(locationVariablePairs.back(), locationVariablePairs.size() - 1);
}
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index f019b2505..6f1e67252 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -368,8 +368,8 @@ namespace storm {
// Add the identity and ranges of the location variables to the ones of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
- storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
- identity &= variableIdentity.toBdd();
+ storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(locationVariables.first, locationVariables.second);
+ identity &= variableIdentity;
range &= result.manager->getRange(locationVariables.first);
// Then create variables for the variables of the automaton.
@@ -420,8 +420,8 @@ namespace storm {
result.columnMetaVariables.insert(variablePair.second);
result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
- storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
- result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+ storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second);
+ result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
result.rowColumnMetaVariablePairs.push_back(variablePair);
result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
@@ -440,8 +440,8 @@ namespace storm {
result.columnMetaVariables.insert(variablePair.second);
result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
- storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
- result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+ storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second);
+ result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
index 4bd31733a..149fc8936 100644
--- a/src/storm/builder/DdPrismModelBuilder.cpp
+++ b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -189,8 +189,8 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
- storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
- variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
+ storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
+ variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
rowColumnMetaVariablePairs.push_back(variablePair);
allGlobalVariables.insert(integerVariable.getExpressionVariable());
@@ -206,8 +206,8 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
- storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
- variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
+ storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
+ variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
rowColumnMetaVariablePairs.push_back(variablePair);
allGlobalVariables.insert(booleanVariable.getExpressionVariable());
@@ -230,7 +230,7 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
- storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+ storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
@@ -247,7 +247,7 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
- storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+ storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 61f9932f4..686a1e9e5 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -208,7 +208,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> Model<Type, ValueType>::getRowColumnIdentity() const {
- return storm::utility::dd::getRowColumnDiagonal<Type, ValueType>(this->getManager(), this->getRowColumnMetaVariablePairs());
+ return (storm::utility::dd::getRowColumnDiagonal<Type>(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates()).template toAdd<ValueType>();
}
template<storm::dd::DdType Type, typename ValueType>
diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp
index 58d6f20f6..dbba10a29 100644
--- a/src/storm/storage/dd/DdManager.cpp
+++ b/src/storm/storage/dd/DdManager.cpp
@@ -122,15 +122,20 @@ namespace storm {
template<DdType LibraryType>
Bdd<LibraryType> DdManager<LibraryType>::getRange(storm::expressions::Variable const& variable) const {
storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
- STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create range for meta variable.");
-
- Bdd<LibraryType> result = this->getBddZero();
-
- for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
- result |= this->getEncoding(variable, value);
+
+ if (metaVariable.hasHigh()) {
+ return Bdd<LibraryType>(*this, internalDdManager.getBddEncodingLessOrEqualThan(static_cast<uint64_t>(metaVariable.getHigh() - metaVariable.getLow()), metaVariable.getCube().getInternalBdd(), metaVariable.getNumberOfDdVariables()), {variable});
+// Bdd<LibraryType> result = this->getBddZero();
+// for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
+// result |= this->getEncoding(variable, value);
+// }
+// return result;
+ } else {
+ // If there is no upper bound on this variable, the whole range is valid.
+ Bdd<LibraryType> result = this->getBddOne();
+ result.addMetaVariable(variable);
+ return result;
}
-
- return result;
}
template<DdType LibraryType>
@@ -146,6 +151,33 @@ namespace storm {
return result;
}
+ template<DdType LibraryType>
+ Bdd<LibraryType> DdManager<LibraryType>::getIdentity(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& variablePairs, bool restrictToFirstRange) const {
+ auto result = this->getBddOne();
+ for (auto const& pair : variablePairs) {
+ result &= this->getIdentity(pair.first, pair.second, restrictToFirstRange);
+ }
+ return result;
+ }
+
+ template<DdType LibraryType>
+ Bdd<LibraryType> DdManager<LibraryType>::getIdentity(storm::expressions::Variable const& first, storm::expressions::Variable const& second, bool restrictToFirstRange) const {
+ auto const& firstMetaVariable = this->getMetaVariable(first);
+ auto const& secondMetaVariable = this->getMetaVariable(second);
+
+ STORM_LOG_THROW(firstMetaVariable.getNumberOfDdVariables() == secondMetaVariable.getNumberOfDdVariables(), storm::exceptions::InvalidOperationException, "Mismatching sizes of meta variables.");
+
+ auto const& firstDdVariables = firstMetaVariable.getDdVariables();
+ auto const& secondDdVariables = secondMetaVariable.getDdVariables();
+
+ auto result = restrictToFirstRange ? this->getRange(first) : this->getBddOne();
+ for (auto it1 = firstDdVariables.begin(), it2 = secondDdVariables.begin(), ite1 = firstDdVariables.end(); it1 != ite1; ++it1, ++it2) {
+ result &= it1->iff(*it2);
+ }
+
+ return result;
+ }
+
template<DdType LibraryType>
Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const {
return getCube({variable});
diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h
index 3332d1b88..055bbfb1a 100644
--- a/src/storm/storage/dd/DdManager.h
+++ b/src/storm/storage/dd/DdManager.h
@@ -131,6 +131,23 @@ namespace storm {
template<typename ValueType>
Add<LibraryType, ValueType> getIdentity(storm::expressions::Variable const& variable) const;
+ /*!
+ * Retrieves a BDD in which an encoding is mapped to true iff the meta variables of each pair encode the same value.
+ *
+ * @param variablePairs The variable pairs for which to compute the identity.
+ * @param restrictToFirstRange If set, the identity will be restricted to the legal range of the first variable.
+ */
+ Bdd<LibraryType> getIdentity(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& variablePairs, bool restrictToFirstRange = true) const;
+
+ /*!
+ * Retrieves a BDD in which an encoding is mapped to true iff the two meta variables encode the same value.
+ *
+ * @param first The first meta variable in the identity.
+ * @param second The second meta variable in the identity.
+ * @param restrictToFirstRange If set, the identity will be restricted to the legal range of the first variable.
+ */
+ Bdd<LibraryType> getIdentity(storm::expressions::Variable const& first, storm::expressions::Variable const& second, bool restrictToFirstRange = true) const;
+
/*!
* Retrieves a BDD that is the cube of the variables representing the given meta variable.
*
diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
index 73db85e4a..5e5e3a3c8 100644
--- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
@@ -198,18 +198,13 @@ namespace storm {
result = thenResult;
} else {
// Get the node to connect the subresults.
- DdNode* var = Cudd_addIthVar(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset);
- Cudd_Ref(var);
- result = Cudd_addIte(ddman, var, thenResult, elseResult);
- Cudd_Ref(result);
- Cudd_RecursiveDeref(ddman, var);
+ result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, thenResult, elseResult);
Cudd_Deref(thenResult);
Cudd_Deref(elseResult);
}
// Store the result in the cache.
signatureCache[nodePair] = result;
- Cudd_Deref(result);
return result;
}
diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp
index 952c7199c..58223d739 100644
--- a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp
+++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp
@@ -57,6 +57,42 @@ namespace storm {
return InternalBdd<DdType::CUDD>(this, cuddManager.bddZero());
}
+ InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const {
+ DdNodePtr node = this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getCuddDdNode(), numberOfDdVariables);
+ STORM_LOG_ASSERT(node != nullptr, "Wut?");
+ FILE* fp = fopen("range.dot", "w");
+ Cudd_DumpDot(cuddManager.getManager(), 1, &node, nullptr, nullptr, fp);
+ fclose(fp);
+
+ auto tmp = cudd::BDD(cuddManager, node);
+ return InternalBdd<DdType::CUDD>(this, tmp);
+ }
+
+ DdNodePtr InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const {
+ std::cout << minimalValue << " / " << maximalValue << " -> " << bound << std::endl;
+ if (maximalValue <= bound) {
+ return Cudd_ReadOne(cuddManager.getManager());
+ } else if (minimalValue > bound) {
+ return Cudd_ReadLogicZero(cuddManager.getManager());
+ }
+
+ STORM_LOG_ASSERT(remainingDdVariables > 0, "Expected more remaining DD variables.");
+ STORM_LOG_ASSERT(!Cudd_IsConstant(cube), "Expected non-constant cube.");
+ uint64_t newRemainingDdVariables = remainingDdVariables - 1;
+ DdNodePtr elseResult = getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, Cudd_T(cube), newRemainingDdVariables);
+ Cudd_Ref(elseResult);
+ DdNodePtr thenResult = getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, Cudd_T(cube), newRemainingDdVariables);
+ Cudd_Ref(thenResult);
+ STORM_LOG_ASSERT(thenResult != elseResult, "Expected different results.");
+
+ std::cout << "creating " << Cudd_NodeReadIndex(cube) << " -> " << thenResult << " / " << elseResult << std::endl;
+ DdNodePtr result = cuddUniqueInter(cuddManager.getManager(), Cudd_NodeReadIndex(cube), thenResult, elseResult);
+ std::cout << "result " << result << std::endl;
+ Cudd_Deref(thenResult);
+ Cudd_Deref(elseResult);
+ return result;
+ }
+
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddZero() const {
return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addZero());
diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.h b/src/storm/storage/dd/cudd/InternalCuddDdManager.h
index 44efef0c5..3b1c74e16 100644
--- a/src/storm/storage/dd/cudd/InternalCuddDdManager.h
+++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.h
@@ -59,6 +59,13 @@ namespace storm {
*/
InternalBdd<DdType::CUDD> getBddZero() const;
+ /*!
+ * Retrieves a BDD that maps to true iff the encoding is less or equal than the given bound.
+ *
+ * @return A BDD with encodings corresponding to values less or equal than the bound.
+ */
+ InternalBdd<DdType::CUDD> getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const;
+
/*!
* Retrieves an ADD representing the constant zero function.
*
@@ -146,6 +153,9 @@ namespace storm {
cudd::Cudd const& getCuddManager() const;
private:
+ // Helper function to create the BDD whose encodings are below a given bound.
+ DdNodePtr getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const;
+
// The manager responsible for the DDs created/modified with this DdManager.
cudd::Cudd cuddManager;
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
index 4586e9890..29f9a3208 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -129,6 +129,28 @@ namespace storm {
return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
}
+ InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::Sylvan> const& cube, uint64_t numberOfDdVariables) const {
+ return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd(this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getSylvanBdd().GetBDD(), numberOfDdVariables)));
+ }
+
+ BDD InternalDdManager<DdType::Sylvan>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const {
+ if (maximalValue <= bound) {
+ return sylvan_true;
+ } else if (minimalValue > bound) {
+ return sylvan_false;
+ }
+
+ STORM_LOG_ASSERT(remainingDdVariables > 0, "Expected more remaining DD variables.");
+ uint64_t newRemainingDdVariables = remainingDdVariables - 1;
+ BDD elseResult = getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, sylvan_high(cube), newRemainingDdVariables);
+ bdd_refs_push(elseResult);
+ BDD thenResult = getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, sylvan_high(cube), newRemainingDdVariables);
+ bdd_refs_push(elseResult);
+ BDD result = sylvan_makenode(sylvan_var(cube), elseResult, thenResult);
+ bdd_refs_pop(2);
+ return result;
+ }
+
template<>
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h
index c10915145..408817965 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h
+++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h
@@ -60,6 +60,13 @@ namespace storm {
*/
InternalBdd<DdType::Sylvan> getBddZero() const;
+ /*!
+ * Retrieves a BDD that maps to true iff the encoding is less or equal than the given bound.
+ *
+ * @return A BDD with encodings corresponding to values less or equal than the bound.
+ */
+ InternalBdd<DdType::Sylvan> getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::Sylvan> const& cube, uint64_t numberOfDdVariables) const;
+
/*!
* Retrieves an ADD representing the constant zero function.
*
@@ -133,6 +140,9 @@ namespace storm {
uint_fast64_t getNumberOfDdVariables() const;
private:
+ // Helper function to create the BDD whose encodings are below a given bound.
+ BDD getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const;
+
// A counter for the number of instances of this class. This is used to determine when to initialize and
// quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
// 'global' manager.
diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp
index b4b74a19a..47d15347e 100644
--- a/src/storm/utility/dd.cpp
+++ b/src/storm/utility/dd.cpp
@@ -45,38 +45,17 @@ namespace storm {
return reachableStates;
}
- template <storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
- storm::dd::Add<Type, ValueType> result = ddManager.template getAddOne<ValueType>();
- for (auto const& pair : rowColumnMetaVariablePairs) {
- result *= ddManager.template getIdentity<ValueType>(pair.first).equals(ddManager.template getIdentity<ValueType>(pair.second)).template toAdd<ValueType>();
- result *= ddManager.getRange(pair.first).template toAdd<ValueType>() * ddManager.getRange(pair.second).template toAdd<ValueType>();
- }
- return result;
- }
-
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
- storm::dd::Bdd<Type> diagonal = ddManager.getBddOne();
- for (auto const& pair : rowColumnMetaVariablePairs) {
- diagonal &= ddManager.template getIdentity<uint64_t>(pair.first).equals(ddManager.template getIdentity<uint64_t>(pair.second));
- diagonal &= ddManager.getRange(pair.first) && ddManager.getRange(pair.second);
- }
- return diagonal;
+ return ddManager.getIdentity(rowColumnMetaVariablePairs);
}
template storm::dd::Bdd<storm::dd::DdType::CUDD> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template storm::dd::Bdd<storm::dd::DdType::Sylvan> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
- template storm::dd::Add<storm::dd::DdType::CUDD, double> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
- template storm::dd::Add<storm::dd::DdType::Sylvan, double> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-
template storm::dd::Bdd<storm::dd::DdType::CUDD> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
template storm::dd::Bdd<storm::dd::DdType::Sylvan> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
- template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
- template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-
}
}
}
diff --git a/src/test/storm/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp
index 7cfac18a5..499be2a12 100644
--- a/src/test/storm/storage/CuddDdTest.cpp
+++ b/src/test/storm/storage/CuddDdTest.cpp
@@ -414,7 +414,7 @@ TEST(CuddDd, RangeTest) {
storm::dd::Bdd<storm::dd::DdType::CUDD> range;
ASSERT_NO_THROW(range = manager->getRange(x.first));
-
+
EXPECT_EQ(9ul, range.getNonZeroCount());
EXPECT_EQ(1ul, range.getLeafCount());
EXPECT_EQ(5ul, range.getNodeCount());