From d23547d99ffb29bca21e39291384b44d1c6cfa20 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 15 Aug 2017 13:38:15 +0200 Subject: [PATCH] started optimizing some DdManager methods --- resources/3rdparty/cudd-3.0.0/cudd/cudd.h | 3 ++ .../abstraction/AbstractionInformation.cpp | 2 +- src/storm/builder/DdJaniModelBuilder.cpp | 12 ++--- src/storm/builder/DdPrismModelBuilder.cpp | 12 ++--- src/storm/models/symbolic/Model.cpp | 2 +- src/storm/storage/dd/DdManager.cpp | 48 +++++++++++++++---- src/storm/storage/dd/DdManager.h | 17 +++++++ .../dd/bisimulation/SignatureRefiner.cpp | 7 +-- .../storage/dd/cudd/InternalCuddDdManager.cpp | 36 ++++++++++++++ .../storage/dd/cudd/InternalCuddDdManager.h | 10 ++++ .../dd/sylvan/InternalSylvanDdManager.cpp | 22 +++++++++ .../dd/sylvan/InternalSylvanDdManager.h | 10 ++++ src/storm/utility/dd.cpp | 23 +-------- src/test/storm/storage/CuddDdTest.cpp | 2 +- 14 files changed, 155 insertions(+), 51 deletions(-) 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(newMetaVariable.first).equals(ddManager->template getIdentity(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 const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()]; - storm::dd::Add variableIdentity = result.manager->template getIdentity(locationVariables.first).equals(result.manager->template getIdentity(locationVariables.second)).template toAdd() * result.manager->getRange(locationVariables.first).template toAdd() * result.manager->getRange(locationVariables.second).template toAdd(); - identity &= variableIdentity.toBdd(); + storm::dd::Bdd 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 variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd() * result.manager->getRange(variablePair.first).template toAdd() * result.manager->getRange(variablePair.second).template toAdd(); - result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); + storm::dd::Bdd variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second); + result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd()); 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 variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd(); - result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); + storm::dd::Bdd variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second); + result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd()); 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 variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + storm::dd::Bdd variableIdentity = manager->getIdentity(variablePair.first, variablePair.second); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); 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 variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + storm::dd::Bdd variableIdentity = manager->getIdentity(variablePair.first, variablePair.second); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); 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 variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + storm::dd::Bdd variableIdentity = manager->getIdentity(variablePair.first, variablePair.second); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); 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 variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + storm::dd::Bdd variableIdentity = manager->getIdentity(variablePair.first, variablePair.second); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); 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::Add Model::getRowColumnIdentity() const { - return storm::utility::dd::getRowColumnDiagonal(this->getManager(), this->getRowColumnMetaVariablePairs()); + return (storm::utility::dd::getRowColumnDiagonal(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates()).template toAdd(); } template 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 Bdd DdManager::getRange(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create range for meta variable."); - - Bdd result = this->getBddZero(); - - for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result |= this->getEncoding(variable, value); + + if (metaVariable.hasHigh()) { + return Bdd(*this, internalDdManager.getBddEncodingLessOrEqualThan(static_cast(metaVariable.getHigh() - metaVariable.getLow()), metaVariable.getCube().getInternalBdd(), metaVariable.getNumberOfDdVariables()), {variable}); +// Bdd 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 result = this->getBddOne(); + result.addMetaVariable(variable); + return result; } - - return result; } template @@ -146,6 +151,33 @@ namespace storm { return result; } + template + Bdd DdManager::getIdentity(std::vector> 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 + Bdd DdManager::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 Bdd DdManager::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 Add 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 getIdentity(std::vector> 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 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(this, cuddManager.bddZero()); } + InternalBdd InternalDdManager::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd 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(this, tmp); + } + + DdNodePtr InternalDdManager::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 InternalAdd InternalDdManager::getAddZero() const { return InternalAdd(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 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 getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd 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(this, sylvan::Bdd::bddZero()); } + InternalBdd InternalDdManager::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd const& cube, uint64_t numberOfDdVariables) const { + return InternalBdd(this, sylvan::Bdd(this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getSylvanBdd().GetBDD(), numberOfDdVariables))); + } + + BDD InternalDdManager::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 InternalDdManager::getAddZero() const { return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero())); 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 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 getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd 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::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs) { - storm::dd::Add result = ddManager.template getAddOne(); - for (auto const& pair : rowColumnMetaVariablePairs) { - result *= ddManager.template getIdentity(pair.first).equals(ddManager.template getIdentity(pair.second)).template toAdd(); - result *= ddManager.getRange(pair.first).template toAdd() * ddManager.getRange(pair.second).template toAdd(); - } - return result; - } - template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs) { - storm::dd::Bdd diagonal = ddManager.getBddOne(); - for (auto const& pair : rowColumnMetaVariablePairs) { - diagonal &= ddManager.template getIdentity(pair.first).equals(ddManager.template getIdentity(pair.second)); - diagonal &= ddManager.getRange(pair.first) && ddManager.getRange(pair.second); - } - return diagonal; + return ddManager.getIdentity(rowColumnMetaVariablePairs); } template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); - template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); - template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); - template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); - template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); - template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> 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 range; ASSERT_NO_THROW(range = manager->getRange(x.first)); - + EXPECT_EQ(9ul, range.getNonZeroCount()); EXPECT_EQ(1ul, range.getLeafCount()); EXPECT_EQ(5ul, range.getNodeCount());