From 5d53c6efa5d091c7054d1f79befc7129489af9e5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 15 Jun 2014 17:56:46 +0200 Subject: [PATCH] Added ODD-concept to easily convert between DD-based and explicit formats. Former-commit-id: f2a2a002b77727d81d348c133348944d4b71b2b9 --- src/storage/dd/CuddDd.cpp | 50 ++++++++++ src/storage/dd/CuddDd.h | 48 +++++++++- src/storage/dd/CuddDdManager.h | 1 + src/storage/dd/CuddDdMetaVariable.h | 4 +- src/storage/dd/CuddOdd.cpp | 97 +++++++++++++++++++ src/storage/dd/CuddOdd.h | 123 +++++++++++++++++++++++++ src/storage/dd/Odd.h | 13 +++ test/functional/storage/CuddDdTest.cpp | 17 ++++ 8 files changed, 351 insertions(+), 2 deletions(-) create mode 100644 src/storage/dd/CuddOdd.cpp create mode 100644 src/storage/dd/CuddOdd.h create mode 100644 src/storage/dd/Odd.h diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index f02e0d7a1..a7d9df2d1 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -2,6 +2,7 @@ #include #include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h" @@ -425,6 +426,55 @@ namespace storm { return Cudd_IsConstant(this->cuddAdd.getNode()); } + uint_fast64_t Dd::getIndex() const { + return static_cast(this->getCuddAdd().NodeReadIndex()); + } + + std::vector Dd::toDoubleVector() const { + return this->toDoubleVector(Odd(*this)); + } + + std::vector Dd::toDoubleVector(Odd const& odd) const { + std::vector result(odd.getTotalOffset()); + std::vector ddVariableIndices = this->getSortedVariableIndices(); + toDoubleVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices); + return result; + } + + void Dd::toDoubleVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const { + if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentLevel == maxLevel) { + result[currentOffset] = Cudd_V(dd); + } else if (ddVariableIndices[currentLevel] < dd->index) { + // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set + // and for the one in which it is not set. + toDoubleVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices); + toDoubleVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices); + } else { + // Otherwise, we simply recursively call the function for both (different) cases. + toDoubleVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices); + toDoubleVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices); + } + } + + std::vector Dd::getSortedVariableIndices() const { + std::vector ddVariableIndices; + for (auto const& metaVariableName : this->getContainedMetaVariableNames()) { + auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Next, we need to sort them, since they may be arbitrarily ordered otherwise. + std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); + return ddVariableIndices; + } + bool Dd::containsMetaVariable(std::string const& metaVariableName) const { auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); return metaVariable != containedMetaVariableNames.end(); diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index b269c4dfd..a7951cfb3 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -16,8 +16,9 @@ namespace storm { namespace dd { - // Forward-declare the DdManager class. + // Forward-declare some classes. template class DdManager; + template class Odd; template<> class Dd { @@ -25,6 +26,7 @@ namespace storm { // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; friend class DdForwardIterator; + friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; @@ -447,6 +449,28 @@ namespace storm { */ bool isConstant() const; + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + uint_fast64_t getIndex() const; + + /*! + * Converts the DD to a double vector. + * + * @return The double vector that is represented by this DD. + */ + std::vector toDoubleVector() const; + + /*! + * Converts the DD to a double vector using the given ODD (that needs to be constructed for the DD). + * + * @param odd The ODD for the DD. + * @return The double vector that is represented by this DD. + */ + std::vector toDoubleVector(Odd const& odd) const; + /*! * Retrieves whether the given meta variable is contained in the DD. * @@ -587,6 +611,28 @@ namespace storm { */ Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames = std::set()); + /*! + * Helper function to convert the DD into a double vector. + * + * @param dd The DD to convert. + * @param result The resulting vector whose entries are to be set appropriately. This vector needs to be + * preallocated. + * @param odd The ODD used for the translation. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentOffset The current offset. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + */ + void toDoubleVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const; + + /*! + * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, + * because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access. + * + * @return The (sorted) indices of all DD variables that are contained in this DD. + */ + std::vector getSortedVariableIndices() const; + // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index a570224c3..75c6a23de 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -16,6 +16,7 @@ namespace storm { class DdManager : public std::enable_shared_from_this> { public: friend class Dd; + friend class Odd; friend class DdForwardIterator; /*! diff --git a/src/storage/dd/CuddDdMetaVariable.h b/src/storage/dd/CuddDdMetaVariable.h index b54ca1939..25375dc4d 100644 --- a/src/storage/dd/CuddDdMetaVariable.h +++ b/src/storage/dd/CuddDdMetaVariable.h @@ -13,8 +13,9 @@ namespace storm { namespace dd { - // Forward-declare the DdManager class. + // Forward-declare some classes. template class DdManager; + template class Odd; template<> class DdMetaVariable { @@ -22,6 +23,7 @@ namespace storm { // Declare the DdManager class as friend so it can access the internals of a meta variable. friend class DdManager; friend class Dd; + friend class Odd; friend class DdForwardIterator; // An enumeration for all legal types of meta variables. diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp new file mode 100644 index 000000000..3f97dc861 --- /dev/null +++ b/src/storage/dd/CuddOdd.cpp @@ -0,0 +1,97 @@ +#include "src/storage/dd/CuddOdd.h" + +#include + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddDdMetaVariable.h" + +namespace storm { + namespace dd { + Odd::Odd(Dd const& dd) { + std::shared_ptr> manager = dd.getDdManager(); + + // First, we need to determine the involved DD variables indices. + std::vector ddVariableIndices = dd.getSortedVariableIndices(); + + // Prepare a unique table for each level that keeps the constructed ODD nodes unique. + std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); + + // Now construct the ODD structure. + std::shared_ptr> rootOdd = buildOddRec(dd.getCuddAdd().getNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + + // Finally, move the children of the root ODD into this ODD. + this->dd = rootOdd->dd; + this->elseNode = std::move(rootOdd->elseNode); + this->thenNode = std::move(rootOdd->thenNode); + this->elseOffset = rootOdd->elseOffset; + this->thenOffset = rootOdd->thenOffset; + } + + Odd::Odd(ADD dd, std::shared_ptr>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr>&& thenNode, uint_fast64_t thenOffset) : dd(dd), elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { + // Intentionally left empty. + } + + Odd const& Odd::getThenSuccessor() const { + return *this->thenNode; + } + + Odd const& Odd::getElseSuccessor() const { + return *this->elseNode; + } + + uint_fast64_t Odd::getElseOffset() const { + return this->elseOffset; + } + + void Odd::setElseOffset(uint_fast64_t newOffset) { + this->elseOffset = newOffset; + } + + uint_fast64_t Odd::getThenOffset() const { + return this->thenOffset; + } + + void Odd::setThenOffset(uint_fast64_t newOffset) { + this->thenOffset = newOffset; + } + + uint_fast64_t Odd::getTotalOffset() const { + return this->elseOffset + this->thenOffset; + } + + std::shared_ptr> Odd::buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels) { + // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. + auto const& iterator = uniqueTableForLevels[currentLevel].find(dd); + if (iterator != uniqueTableForLevels[currentLevel].end()) { + return iterator->second; + } else { + // Otherwise, we need to recursively compute the ODD. + + // If we are already past the maximal level that is to be considered, we can simply create a Odd without + // successors + if (currentLevel == maxLevel) { + uint_fast64_t elseOffset = 0; + uint_fast64_t thenOffset = 0; + + // If the DD is not the zero leaf, then the then-offset is 1. + if (dd != Cudd_ReadZero(manager.getManager())) { + thenOffset = 1; + } + + return std::shared_ptr>(new Odd(ADD(manager, dd), nullptr, elseOffset, nullptr, thenOffset)); + } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { + // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same + // node for the then-successor as well. + std::shared_ptr> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> thenNode = elseNode; + return std::shared_ptr>(new Odd(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset())); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + std::shared_ptr> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + return std::shared_ptr>(new Odd(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset())); + } + } + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h new file mode 100644 index 000000000..2927bfde6 --- /dev/null +++ b/src/storage/dd/CuddOdd.h @@ -0,0 +1,123 @@ +#ifndef STORM_STORAGE_DD_CUDDODD_H_ +#define STORM_STORAGE_DD_CUDDODD_H_ + +#include + +#include "src/storage/dd/Odd.h" +#include "src/storage/dd/CuddDd.h" +#include "src/utility/OsDetection.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + template<> + class Odd { + public: + /*! + * Constructs an offset-labeled DD from the given DD. + * + * @param dd The DD for which to build the offset-labeled DD. + */ + Odd(Dd const& dd); + + // Instantiate all copy/move constructors/assignments with the default implementation. + Odd() = default; + Odd(Odd const& other) = default; + Odd& operator=(Odd const& other) = default; +#ifndef WINDOWS + Odd(Odd&& other) = default; + Odd& operator=(Odd&& other) = default; +#endif + + /*! + * Retrieves the then-successor of this ODD node. + * + * @return The then-successor of this ODD node. + */ + Odd const& getThenSuccessor() const; + + /*! + * Retrieves the else-successor of this ODD node. + * + * @return The else-successor of this ODD node. + */ + Odd const& getElseSuccessor() const; + + /*! + * Retrieves the else-offset of this ODD node. + * + * @return The else-offset of this ODD node. + */ + uint_fast64_t getElseOffset() const; + + /*! + * Sets the else-offset of this ODD node. + * + * @param newOffset The new else-offset of this ODD node. + */ + void setElseOffset(uint_fast64_t newOffset); + + /*! + * Retrieves the then-offset of this ODD node. + * + * @return The then-offset of this ODD node. + */ + uint_fast64_t getThenOffset() const; + + /*! + * Sets the then-offset of this ODD node. + * + * @param newOffset The new then-offset of this ODD node. + */ + void setThenOffset(uint_fast64_t newOffset); + + /*! + * Retrieves the total offset, i.e., the sum of the then- and else-offset. + * + * @return The total offset of this ODD. + */ + uint_fast64_t getTotalOffset() const; + + private: + /*! + * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor. + * + * @param dd The DD associated with this ODD node. + * @param elseNode The else-successor of thie ODD node. + * @param elseOffset The offset of the else-successor. + * @param thenNode The then-successor of thie ODD node. + * @param thenOffset The offset of the then-successor. + */ + Odd(ADD dd, std::shared_ptr>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr>&& thenNode, uint_fast64_t thenOffset); + + /*! + * Recursively builds the ODD. + * + * @param dd The DD for which to build the ODD. + * @param manager The manager responsible for the DD. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps + * ODD nodes for the same DD and level unique. + * @return A pointer to the constructed ODD for the given arguments. + */ + static std::shared_ptr> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); + + // The DD associated with this ODD node. + ADD dd; + + // The then- and else-nodes. + std::shared_ptr> elseNode; + std::shared_ptr> thenNode; + + // The offsets that need to be added if the then- or else-successor is taken, respectively. + uint_fast64_t elseOffset; + uint_fast64_t thenOffset; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDODD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/Odd.h b/src/storage/dd/Odd.h new file mode 100644 index 000000000..6a7231300 --- /dev/null +++ b/src/storage/dd/Odd.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_ODD_H_ +#define STORM_STORAGE_DD_ODD_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare Odd class so we can then specialize it for the different DD types. + template class Odd; + } +} + +#endif /* STORM_STORAGE_DD_ODD_H_ */ \ No newline at end of file diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 391f8c96d..7f8a3f299 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -3,6 +3,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/DdMetaVariable.h" TEST(CuddDdManager, Constants) { @@ -375,4 +376,20 @@ TEST(CuddDd, ToExpressionTest) { // same value as the current value obtained from the DD. EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation)); } +} + +TEST(CuddDd, OddTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + manager->addMetaVariable("x", 1, 9); + + storm::dd::Dd dd = manager->getIdentity("x"); + storm::dd::Odd odd; + ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); + EXPECT_EQ(9, odd.getTotalOffset()); + std::vector ddAsVector; + ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector()); + EXPECT_EQ(9, ddAsVector.size()); + for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { + EXPECT_TRUE(i+1 == ddAsVector[i]); + } } \ No newline at end of file