From 70fc3ec29a76958717b36b341cfb80d3673442c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 20 Mar 2014 18:50:30 +0100 Subject: [PATCH] Further work on abstraction layer for DDs. Former-commit-id: 245986076bca9c24016c8d6f6ab487438f3ed008 --- src/storage/dd/CuddDd.cpp | 90 +++++++++++++++ src/storage/dd/CuddDd.h | 178 ++++++++++++++++++++++++++++-- src/storage/dd/CuddDdManager.cpp | 68 ++++++++++++ src/storage/dd/CuddDdManager.h | 42 ++++--- src/storage/dd/DdMetaVariable.cpp | 13 ++- src/storage/dd/DdMetaVariable.h | 6 +- src/storage/dd/DdType.h | 12 ++ 7 files changed, 378 insertions(+), 31 deletions(-) create mode 100644 src/storage/dd/CuddDd.cpp create mode 100644 src/storage/dd/DdType.h diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp new file mode 100644 index 000000000..d3ad10493 --- /dev/null +++ b/src/storage/dd/CuddDd.cpp @@ -0,0 +1,90 @@ +#include "src/storage/dd/CuddDd.h" + +namespace storm { + namespace dd { + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + // Intentionally left empty. + } + + Dd Dd::operator+(Dd const& other) const { + Dd result(*this); + result += other; + return result; + } + + Dd& Dd::operator+=(Dd const& other) { + cuddAdd += other; + + // Join the variable sets of the two participating DDs. + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + + return *this; + } + + Dd Dd::operator*(Dd const& other) const { + Dd result(*this); + result *= other; + return result; + } + + Dd& Dd::operator*=(Dd const& other) { + cuddAdd *= other; + + // Join the variable sets of the two participating DDs. + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + + return *this; + } + + Dd Dd::operator-(Dd const& other) const { + Dd result(*this); + result -= other; + return result; + } + + Dd& Dd::operator-=(Dd const& other) { + cuddAdd -= other; + + // Join the variable sets of the two participating DDs. + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + + return *this; + } + + Dd Dd::operator/(Dd const& other) const { + Dd result(*this); + result /= other; + return result; + } + + Dd& Dd::operator/=(Dd const& other) { + cuddAdd.Divide(other); + + // Join the variable sets of the two participating DDs. + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + + return *this; + } + + Dd Dd::operator~() const { + Dd result(*this); + result.complement(); + return result; + } + + Dd& Dd::complement() { + cuddAdd = ~cuddAdd; + return *this; + } + + void Dd::exportToDot(std::string const& filename) const { + FILE* filePointer = fopen(filename.c_str() , "w"); + this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer); + fclose(filePointer); + } + + std::shared_ptr> Dd::getDdManager() const { + return this->ddManager; + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index d608b07e5..eff759bd3 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -12,13 +12,10 @@ namespace storm { template<> class Dd { - /*! - * Creates a DD that encapsulates the given CUDD ADD. - * - * @param cuddAdd The CUDD ADD to store. - */ - Dd(ADD cuddAdd); - + public: + // Declare the DdManager class as friend so it can access the internals of a DD. + friend class DdManager; + // Instantiate all copy/move constructors/assignments with the default implementation. Dd(Dd const& other) = default; Dd(Dd&& other) = default; @@ -89,6 +86,13 @@ namespace storm { */ Dd& operator/=(Dd const& other); + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd minus() const; + /*! * Retrieves the logical complement of the current DD. The result will map all encodings with a value * unequal to zero to false and all others to true. @@ -100,8 +104,157 @@ namespace storm { /*! * Logically complements the current DD. The result will map all encodings with a value * unequal to zero to false and all others to true. + * + * @return A reference to the current DD after the operation. + */ + Dd& complement(); + + /*! + * Retrieves the function that maps all evaluations to one that have an identical function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd equals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd notEquals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd less(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or + * equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd lessOrEqual(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. */ - void complement(); + Dd greater(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * or equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd greaterOrEqual(Dd const& other) const; + + /*! + * Existentially abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void existsAbstract(std::unordered_set const& metaVariableNames); + + /*! + * Sum-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void sumAbstract(std::unordered_set const& metaVariableNames); + + /*! + * Min-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void minAbstract(std::unordered_set const& metaVariableNames); + + /*! + * Max-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void maxAbstract(std::unordered_set const& metaVariableNames); + + /*! + * Sets the function values of all encodings that have the given value of the meta variable to the given + * target value. + * + * @param metaVariableName The name of the meta variable that has to be equal to the given value. + * @param variableValue The value that the meta variable is supposed to have. This must be within the range + * of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the two meta variables to the + * given target value. + * + * @param metaVariableName1 The name of the first meta variable that has to be equal to the first given + * value. + * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the + * range of the meta variable. + * @param metaVariableName2 The name of the first meta variable that has to be equal to the second given + * value. + * @param variableValue2 The value that the second meta variable is supposed to have. This must be within + * the range of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the given meta variables to the + * given target value. + * + * @param metaVariableNameToValueMap A mapping of meta variable names to the values they are supposed to + * have. All values must be within the range of the respective meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue); + + /*! + * Retrieves whether the given meta variable is contained in the DD. + * + * @param metaVariableName The name of the meta variable for which to query membership. + * @return True iff the meta variable is contained in the DD. + */ + bool containsMetaVariable(std::string const& metaVariableName) const; + + /*! + * Retrieves whether the given meta variables are all contained in the DD. + * + * @param metaVariableNames The names of the meta variable for which to query membership. + * @return True iff all meta variables are contained in the DD. + */ + bool containsMetaVariables(std::unordered_set metaVariableNames) const; + + /*! + * Retrieves the set of all names of meta variables contained in the DD. + * + * @return The set of names of all meta variables contained in the DD. + */ + std::unordered_set const& getContainedMetaVariableNames() const; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToDot(std::string const& filename) const; /*! * Retrieves the manager that is responsible for this DD. @@ -111,6 +264,15 @@ namespace storm { std::shared_ptr> getDdManager() const; private: + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddAdd The CUDD ADD to store. + * @param + */ + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept; + // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index af75ca402..580c6c9a6 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,7 +1,75 @@ #include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace dd { + DdManager::DdManager() noexcept : metaVariableMap(), cuddManager() { + // Intentionally left empty. + } + Dd DdManager::getOne() { + return Dd(this->shared_from_this(), cuddManager.addOne(), {""}); + } + + Dd DdManager::getZero() { + return Dd(this->shared_from_this(), cuddManager.addZero(), {""}); + } + + Dd DdManager::getConstant(double value) { + return Dd(this->shared_from_this(), cuddManager.constant(value), {""}); + } + + void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + std::size_t numberOfBits = std::log2(high - low); + + std::vector> variables; + for (std::size_t i = 0; i < numberOfBits; ++i) { + variables.emplace_back(cuddManager.addVar()); + } + + metaVariableMap.emplace(name, low, high, variables, this->shared_from_this()); + } + + void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { + if (names.size() == 0) { + throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables."; + } + + // Add the variables in interleaved order. + std::size_t numberOfBits = std::log2(high - low); + std::vector>> variables; + for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) { + for (uint_fast64_t i = 0; i < names.size(); ++i) { + variables[i].emplace_back(cuddManager.addVar()); + } + } + + // Now add the meta variables. + for (uint_fast64_t i = 0; i < names.size(); ++i) { + metaVariableMap.emplace(names[i], low, high, variables[i], this->shared_from_this()); + } + } + + DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { + auto const& nameVariablePair = metaVariableMap.find(metaVariableName); + + if (nameVariablePair == metaVariableMap.end()) { + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name."; + } + + return nameVariablePair->second; + } + + std::unordered_set DdManager::getAllMetaVariableNames() const { + std::unordered_set result; + for (auto const& nameValuePair : metaVariableMap) { + result.insert(nameValuePair.first); + } + return result; + } + + Cudd& DdManager::getCuddManager() { + return this->cuddManager; + } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 8c47b4b2d..72f2aea0c 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -5,22 +5,24 @@ #include #include "src/storage/dd/DdManager.h" +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/CuddDd.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" namespace storm { namespace dd { - // To break the cylic dependencies, we need to forward-declare the other DD-related classes. - template class DdMetaVariable; - template class Dd; - template<> class DdManager : std::enable_shared_from_this> { + // To break the cylic dependencies, we need to forward-declare the other DD-related classes. + friend class DdMetaVariable; + friend class Dd; + /*! * Creates an empty manager without any meta variables. */ - DdManager(); + DdManager() noexcept; // Explictly forbid copying a DdManager, but allow moving it. DdManager(DdManager const& other) = delete; @@ -55,12 +57,17 @@ namespace storm { * @param name The name of the meta variable. * @param low The lowest value of the range of the variable. * @param high The highest value of the range of the variable. - * @param addSuccessorVariable If set, a second meta variable is added. This can then be used, for example, - * to encode the value of the meta variable in a successor state. - * @param useInterleavedVariableOrdering If set, the variables used for the successor meta variable are - * interleaved with the ones for the added meta variable. */ - void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, bool addSuccessorVariable = false, bool useInterleavedVariableOrdering = true); + void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high); + + /*! + * Adds meta variables with the given names and (equal) range and arranges the DD variables in an interleaved order. + * + * @param names The names of the variables. + * @param low The lowest value of the ranges of the variables. + * @param high The highest value of the ranges of the variables. + */ + void addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high); /*! * Retrieves the meta variable with the given name if it exists. @@ -71,21 +78,20 @@ namespace storm { DdMetaVariable const& getMetaVariable(std::string const& metaVariableName) const; /*! - * Retrieves the successor meta variable of the one with the given name if it exists. + * Retrieves the names of all meta variables that have been added to the manager. * - * @param metaVariableName The name of the meta variable whose successor meta variable to retrieve. - * @return The successor meta variable of the one with the given name. + * @return The set of all meta variable names of the manager. */ - DdMetaVariable const& getSuccessorMetaVariable(std::string const& metaVariableName) const; + std::unordered_set getAllMetaVariableNames() const; + private: /*! - * Retrieves the names of all meta variables that have been added to the manager. + * Retrieves the underlying CUDD manager. * - * @return The set of all meta variable names of the manager. + * @return The underlying CUDD manager. */ - std::unordered_set getAllMetaVariableNames(); + Cudd& getCuddManager(); - private: // A mapping from variable names to the meta variable information. std::unordered_map> metaVariableMap; diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 72c2be15f..c2795562b 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -3,8 +3,12 @@ namespace storm { namespace dd { template - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) { - // Intentionally left empty. + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) { + // Create the cube of all variables of this meta variable. + this->cube = this->getDdManager()->getOne(); + for (auto const& ddVariable : this->ddVariables) { + this->cube *= ddVariable; + } } template @@ -21,6 +25,11 @@ namespace storm { int_fast64_t DdMetaVariable::getHigh() const { return this->high; } + + template + std::shared_ptr> DdMetaVariable::getDdManager() const { + return this->manager; + } template std::vector> const& DdMetaVariable::getDdVariables() const { diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 2631143f2..f784fda2c 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -14,8 +14,8 @@ namespace storm { template class DdMetaVariable { - // Declare the other DD-related classes as friends so they can access the internals of a meta variable. - friend class Dd; + // Declare the DdManager class as friend so it can access the internals of a meta variable. + friend class DdManager; /*! * Creates a meta variable with the given name, range bounds. @@ -26,7 +26,7 @@ namespace storm { * @param ddVariables The vector of variables used to encode this variable. * @param manager A pointer to the manager that is responsible for this meta variable. */ - DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) noexcept; // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; diff --git a/src/storage/dd/DdType.h b/src/storage/dd/DdType.h new file mode 100644 index 000000000..327832ec5 --- /dev/null +++ b/src/storage/dd/DdType.h @@ -0,0 +1,12 @@ +#ifndef STORM_STORAGE_DD_DDTYPE_H_ +#define STORM_STORAGE_DD_DDTYPE_H_ + +namespace storm { + namespace dd { + enum DdType { + CUDD + }; + } +} + +#endif /* STORM_STORAGE_DD_DDTYPE_H_ */