From de44a1562ce9f82302cdba7fa5c96c901d919e4b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 19 Mar 2014 23:24:55 +0100 Subject: [PATCH 01/20] Started writing the DD abstraction layer. Former-commit-id: 8720a38b17b919f2e7ea33f57bb2e513edf8d210 --- CMakeLists.txt | 4 +- CPackConfig.cmake | 27 ---- .../MILPMinimalLabelSetGenerator.h | 2 +- src/storage/dd/CuddDd.h | 126 ++++++++++++++++++ src/storage/dd/CuddDdManager.cpp | 7 + src/storage/dd/CuddDdManager.h | 98 ++++++++++++++ src/storage/dd/Dd.h | 13 ++ src/storage/dd/DdManager.h | 13 ++ src/storage/dd/DdMetaVariable.cpp | 38 ++++++ src/storage/dd/DdMetaVariable.h | 101 ++++++++++++++ 10 files changed, 400 insertions(+), 29 deletions(-) delete mode 100644 CPackConfig.cmake create mode 100644 src/storage/dd/CuddDd.h create mode 100644 src/storage/dd/CuddDdManager.cpp create mode 100644 src/storage/dd/CuddDdManager.h create mode 100644 src/storage/dd/Dd.h create mode 100644 src/storage/dd/DdManager.h create mode 100644 src/storage/dd/DdMetaVariable.cpp create mode 100644 src/storage/dd/DdMetaVariable.h diff --git a/CMakeLists.txt b/CMakeLists.txt index aa1e269c0..8942c984f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -242,7 +242,8 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB_RECURSE STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) +file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp) @@ -275,6 +276,7 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) source_group(solver FILES ${STORM_SOLVER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) +source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) diff --git a/CPackConfig.cmake b/CPackConfig.cmake deleted file mode 100644 index 5ce6c0f53..000000000 --- a/CPackConfig.cmake +++ /dev/null @@ -1,27 +0,0 @@ -include(InstallRequiredSystemLibraries) - -# For help take a look at: -# http://www.cmake.org/Wiki/CMake:CPackConfiguration - -### general settings -set(CPACK_PACKAGE_NAME "StoRM") -set(CPACK_PACKAGE_VENDOR "i2 RWTH Aachen University") -set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Stochastic Reward Model Checker - An extensible model checker written in C++.") - -set(CPACK_RESOURCE_FILE_LICENSE "${CMAKE_SOURCE_DIR}/LICENSE") - -### versions -set(CPACK_PACKAGE_VERSION_MAJOR "${STORM_CPP_VERSION_MAJOR}") -set(CPACK_PACKAGE_VERSION_MINOR "${STORM_CPP_VERSION_MINOR}") -set(CPACK_PACKAGE_VERSION_PATCH "${STORM_CPP_VERSION_PATCH}") -set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION_MAJOR}.${CPACK_PACKAGE_VERSION_MINOR}.${CPACK_PACKAGE_VERSION_PATCH}-${STORM_CPP_VERSION_HASH}") - -set(CPACK_GENERATOR "ZIP") -set(CPACK_PACKAGE_INSTALL_DIRECTORY "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}") - -### source package settings -set(CPACK_SOURCE_GENERATOR "ZIP") -set(CPACK_SOURCE_IGNORE_FILES "~$;[.]swp$;/[.]svn/;/[.]git/;.gitignore;/build/;tags;cscope.*") -set(CPACK_SOURCE_PACKAGE_FILE_NAME "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}-src") - -include(CPack) \ No newline at end of file diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 3ec8256ed..027369182 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1021,7 +1021,7 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; } - bool strictBound = !probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS; + bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS); // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. double bound = probBoundFormula->getBound(); diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h new file mode 100644 index 000000000..d608b07e5 --- /dev/null +++ b/src/storage/dd/CuddDd.h @@ -0,0 +1,126 @@ +#ifndef STORM_STORAGE_DD_CUDDDD_H_ +#define STORM_STORAGE_DD_CUDDDD_H_ + +#include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddDdManager.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + + template<> + class Dd { + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param cuddAdd The CUDD ADD to store. + */ + Dd(ADD cuddAdd); + + // Instantiate all copy/move constructors/assignments with the default implementation. + Dd(Dd const& other) = default; + Dd(Dd&& other) = default; + Dd& operator=(Dd const& other) = default; + Dd& operator=(Dd&& other) = default; + + /*! + * Adds the two DDs. + * + * @param other The DD to add to the current one. + * @return The result of the addition. + */ + Dd operator+(Dd const& other) const; + + /*! + * Adds the given DD to the current one. + * + * @param other The DD to add to the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator+=(Dd const& other); + + /*! + * Multiplies the two DDs. + * + * @param other The DD to multiply with the current one. + * @return The result of the multiplication. + */ + Dd operator*(Dd const& other) const; + + /*! + * Multiplies the given DD with the current one and assigns the result to the current DD. + * + * @param other The DD to multiply with the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator*=(Dd const& other); + + /*! + * Subtracts the given DD from the current one. + * + * @param other The DD to subtract from the current one. + * @return The result of the subtraction. + */ + Dd operator-(Dd const& other) const; + + /*! + * Subtracts the given DD from the current one and assigns the result to the current DD. + * + * @param other The DD to subtract from the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator-=(Dd const& other); + + /*! + * Divides the current DD by the given one. + * + * @param other The DD by which to divide the current one. + * @return The result of the division. + */ + Dd operator/(Dd const& other) const; + + /*! + * Divides the current DD by the given one and assigns the result to the current DD. + * + * @param other The DD by which to divide the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator/=(Dd const& other); + + /*! + * 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. + * + * @return The logical complement of the current DD. + */ + Dd operator~() const; + + /*! + * Logically complements the current DD. The result will map all encodings with a value + * unequal to zero to false and all others to true. + */ + void complement(); + + /*! + * Retrieves the manager that is responsible for this DD. + * + * A pointer to the manager that is responsible for this DD. + */ + std::shared_ptr> getDdManager() const; + + private: + // A pointer to the manager responsible for this DD. + std::shared_ptr> ddManager; + + // The ADD created by CUDD. + ADD cuddAdd; + + // The names of all meta variables that appear in this DD. + std::unordered_set containedMetaVariableNames; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp new file mode 100644 index 000000000..af75ca402 --- /dev/null +++ b/src/storage/dd/CuddDdManager.cpp @@ -0,0 +1,7 @@ +#include "src/storage/dd/CuddDdManager.h" + +namespace storm { + namespace dd { + + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h new file mode 100644 index 000000000..8c47b4b2d --- /dev/null +++ b/src/storage/dd/CuddDdManager.h @@ -0,0 +1,98 @@ +#ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ +#define STORM_STORAGE_DD_CUDDDDMANAGER_H_ + +#include +#include + +#include "src/storage/dd/DdManager.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> { + /*! + * Creates an empty manager without any meta variables. + */ + DdManager(); + + // Explictly forbid copying a DdManager, but allow moving it. + DdManager(DdManager const& other) = delete; + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager const& other) = delete; + DdManager& operator=(DdManager&& other) = default; + + /*! + * Retrieves a DD representing the constant one function. + * + * @return A DD representing the constant one function. + */ + Dd getOne(); + + /*! + * Retrieves a DD representing the constant zero function. + * + * @return A DD representing the constant zero function. + */ + Dd getZero(); + + /*! + * Retrieves a DD representing the constant function with the given value. + * + * @return A DD representing the constant function with the given value. + */ + Dd getConstant(double value); + + /*! + * Adds a meta variable with the given name and range. + * + * @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); + + /*! + * Retrieves the meta variable with the given name if it exists. + * + * @param metaVariableName The name of the meta variable to retrieve. + * @return The meta variable with the given name. + */ + DdMetaVariable const& getMetaVariable(std::string const& metaVariableName) const; + + /*! + * Retrieves the successor meta variable of the one with the given name if it exists. + * + * @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. + */ + DdMetaVariable const& getSuccessorMetaVariable(std::string const& metaVariableName) const; + + /*! + * Retrieves the names of all meta variables that have been added to the manager. + * + * @return The set of all meta variable names of the manager. + */ + std::unordered_set getAllMetaVariableNames(); + + private: + // A mapping from variable names to the meta variable information. + std::unordered_map> metaVariableMap; + + // The manager responsible for the DDs created/modified with this DdManager. + Cudd cuddManager; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h new file mode 100644 index 000000000..bc7075f46 --- /dev/null +++ b/src/storage/dd/Dd.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DD_H_ +#define STORM_STORAGE_DD_DD_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare Dd class so we can then specialize it for the different DD types. + template class Dd; + } +} + +#endif /* STORM_STORAGE_DD_DD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h new file mode 100644 index 000000000..53fde64bb --- /dev/null +++ b/src/storage/dd/DdManager.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DDMANAGER_H_ +#define STORM_STORAGE_DD_DDMANAGER_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare DdManager class so we can then specialize it for the different DD types. + template class DdManager; + } +} + +#endif /* STORM_STORAGE_DD_DDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp new file mode 100644 index 000000000..72c2be15f --- /dev/null +++ b/src/storage/dd/DdMetaVariable.cpp @@ -0,0 +1,38 @@ +#include "src/storage/dd/DdMetaVariable.h" + +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. + } + + template + std::string const& DdMetaVariable::getName() const { + return this->name; + } + + template + int_fast64_t DdMetaVariable::getLow() const { + return this->low; + } + + template + int_fast64_t DdMetaVariable::getHigh() const { + return this->high; + } + + template + std::vector> const& DdMetaVariable::getDdVariables() const { + return this->ddVariables; + } + + template + Dd const& DdMetaVariable::getCube() const { + return this->cube; + } + + // Explicitly instantiate DdMetaVariable. + template<> class DdMetaVariable; + } +} \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h new file mode 100644 index 000000000..2631143f2 --- /dev/null +++ b/src/storage/dd/DdMetaVariable.h @@ -0,0 +1,101 @@ +#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_ +#define STORM_STORAGE_DD_DDMETAVARIABLE_H_ + +#include +#include +#include +#include + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddDd.h" + +namespace storm { + namespace dd { + + template + class DdMetaVariable { + // Declare the other DD-related classes as friends so they can access the internals of a meta variable. + friend class Dd; + + /*! + * Creates a meta variable with the given name, range bounds. + * + * @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 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); + + // Explictly generate all default versions of copy/move constructors/assignments. + DdMetaVariable(DdMetaVariable const& other) = default; + DdMetaVariable(DdMetaVariable&& other) = default; + DdMetaVariable& operator=(DdMetaVariable const& other) = default; + DdMetaVariable& operator=(DdMetaVariable&& other) = default; + + /*! + * Retrieves the name of the meta variable. + * + * @return The name of the variable. + */ + std::string const& getName() const; + + /*! + * Retrieves the lowest value of the range of the variable. + * + * @return The lowest value of the range of the variable. + */ + int_fast64_t getLow() const; + + /*! + * Retrieves the highest value of the range of the variable. + * + * @return The highest value of the range of the variable. + */ + int_fast64_t getHigh() const; + + /*! + * Retrieves the manager that is responsible for this meta variable. + * + * A pointer to the manager that is responsible for this meta variable. + */ + std::shared_ptr> getDdManager() const; + + private: + /*! + * Retrieves the variables used to encode the meta variable. + * + * @return A vector of variables used to encode the meta variable. + */ + std::vector> const& getDdVariables() const; + + /*! + * Retrieves the cube of all variables that encode this meta variable. + * + * @return The cube of all variables that encode this meta variable. + */ + Dd const& getCube() const; + + // The name of the meta variable. + std::string name; + + // The lowest value of the range of the variable. + int_fast64_t low; + + // The highest value of the range of the variable. + int_fast64_t high; + + // The vector of variables that are used to encode the meta variable. + std::vector> ddVariables; + + // The cube consisting of all variables that encode the meta variable. + Dd cube; + + // A pointer to the manager responsible for this meta variable. + std::shared_ptr> manager; + }; + } +} + +#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */ \ No newline at end of file From 70fc3ec29a76958717b36b341cfb80d3673442c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 20 Mar 2014 18:50:30 +0100 Subject: [PATCH 02/20] 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_ */ From 97e4e0125047740c334edea576e84fb82c445690 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 21 Mar 2014 19:08:26 +0100 Subject: [PATCH 03/20] Further step towards finalizing the abstraction layer for DDs. Former-commit-id: efd5822b677716cfa87e19010c3198ea993e637b --- src/storage/dd/CuddDd.cpp | 144 ++++++++++++++++++++++++++++-- src/storage/dd/CuddDd.h | 20 ++++- src/storage/dd/CuddDdManager.cpp | 8 +- src/storage/dd/CuddDdManager.h | 1 - src/storage/dd/DdMetaVariable.cpp | 1 + src/storage/dd/DdMetaVariable.h | 5 +- 6 files changed, 163 insertions(+), 16 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index d3ad10493..23f148da0 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,8 +1,9 @@ #include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddDdManager.h" namespace storm { namespace dd { - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } @@ -13,10 +14,10 @@ namespace storm { } Dd& Dd::operator+=(Dd const& other) { - cuddAdd += other; + cuddAdd += other.getCuddAdd(); // 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())); + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); return *this; } @@ -28,10 +29,10 @@ namespace storm { } Dd& Dd::operator*=(Dd const& other) { - cuddAdd *= other; + cuddAdd *= other.getCuddAdd(); // 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())); + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); return *this; } @@ -43,10 +44,10 @@ namespace storm { } Dd& Dd::operator-=(Dd const& other) { - cuddAdd -= other; + cuddAdd -= other.getCuddAdd(); // 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())); + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); return *this; } @@ -58,10 +59,10 @@ namespace storm { } Dd& Dd::operator/=(Dd const& other) { - cuddAdd.Divide(other); + cuddAdd.Divide(other.getCuddAdd()); // 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())); + std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); return *this; } @@ -77,12 +78,137 @@ namespace storm { return *this; } + Dd Dd::equals(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().Equals(other.getCuddAdd()); + return result; + } + + Dd Dd::notEquals(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().NotEquals(other.getCuddAdd()); + return result; + } + + Dd Dd::less(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().LessThan(other.getCuddAdd()); + return result; + } + + Dd Dd::lessOrEqual(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().LessThanOrEqual(other.getCuddAdd()); + return result; + } + + Dd Dd::greater(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().GreaterThan(other.getCuddAdd()); + return result; + } + + Dd Dd::greaterOrEqual(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()); + return result; + } + + void Dd::existsAbstract(std::unordered_set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); + } + + void Dd::sumAbstract(std::unordered_set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); + } + + void Dd::minAbstract(std::unordered_set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); + } + + void Dd::maxAbstract(std::unordered_set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); + } + + void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { + std::unordered_map metaVariableNameToValueMap; + metaVariableNameToValueMap.emplace(metaVariableName, variableValue); + this->setValue(metaVariableNameToValueMap, targetValue); + } + + void Dd::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) { + std::unordered_map metaVariableNameToValueMap; + metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1); + metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2); + this->setValue(metaVariableNameToValueMap, targetValue); + } + + void Dd::setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue) { + // TODO: Fill this + } + + bool Dd::containsMetaVariable(std::string const& metaVariableName) const { + auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); + return metaVariable != containedMetaVariableNames.end(); + } + + bool Dd::containsMetaVariables(std::unordered_set metaVariableNames) const { + for (auto const& metaVariableName : metaVariableNames) { + auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); + + if (metaVariable == containedMetaVariableNames.end()) { + return false; + } + } + return true; + } + + std::unordered_set const& Dd::getContainedMetaVariableNames() const { + return containedMetaVariableNames; + } + 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); } + ADD Dd::getCuddAdd() { + return this->cuddAdd; + } + + ADD const& Dd::getCuddAdd() const { + return this->cuddAdd; + } + std::shared_ptr> Dd::getDdManager() const { return this->ddManager; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index eff759bd3..b0a3e33eb 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -1,14 +1,18 @@ #ifndef STORM_STORAGE_DD_CUDDDD_H_ #define STORM_STORAGE_DD_CUDDDD_H_ +#include +#include + #include "src/storage/dd/Dd.h" -#include "src/storage/dd/CuddDdManager.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" namespace storm { namespace dd { + // Forward-declare the DdManager class. + template class DdManager; template<> class Dd { @@ -264,6 +268,20 @@ namespace storm { std::shared_ptr> getDdManager() const; private: + /*! + * Retrieves the CUDD ADD object associated with this DD. + * + * @return The CUDD ADD object assoicated with this DD. + */ + ADD getCuddAdd(); + + /*! + * Retrieves the CUDD ADD object associated with this DD. + * + * @return The CUDD ADD object assoicated with this DD. + */ + ADD const& getCuddAdd() const; + /*! * Creates a DD that encapsulates the given CUDD ADD. * diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 580c6c9a6..40c11fbaa 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -24,10 +24,10 @@ namespace storm { std::vector> variables; for (std::size_t i = 0; i < numberOfBits; ++i) { - variables.emplace_back(cuddManager.addVar()); + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); } - metaVariableMap.emplace(name, low, high, variables, this->shared_from_this()); + metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); } void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { @@ -40,13 +40,13 @@ namespace storm { 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()); + variables[i].emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {names[i]})); } } // 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()); + metaVariableMap.emplace(names[i], DdMetaVariable(names[i], low, high, variables[i], this->shared_from_this())); } } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 72f2aea0c..ede42104d 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -16,7 +16,6 @@ namespace storm { 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; /*! diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index c2795562b..d5cae858c 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -1,4 +1,5 @@ #include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/CuddDdManager.h" namespace storm { namespace dd { diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index f784fda2c..6bf5f6c3c 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -6,16 +6,19 @@ #include #include -#include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddDd.h" namespace storm { namespace dd { + // Forward-declare the DdManager class. + template class DdManager; template class DdMetaVariable { + public: // Declare the DdManager class as friend so it can access the internals of a meta variable. friend class DdManager; + friend class Dd; /*! * Creates a meta variable with the given name, range bounds. From 874fc8a864876ec7456e294386c4ace06bf92217 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Mar 2014 12:58:18 +0100 Subject: [PATCH 04/20] Alpha version of DD abstraction layer. Former-commit-id: 98cc5f3aa7a6a836c86388e39a9af1579abbbf5a --- src/storage/dd/CuddDd.cpp | 7 ++++++- src/storage/dd/CuddDd.h | 3 ++- src/storage/dd/CuddDdManager.cpp | 29 +++++++++++++++++++++++++++-- src/storage/dd/CuddDdManager.h | 14 +++++++++++++- src/storage/dd/DdMetaVariable.cpp | 10 +++++++--- src/storage/dd/DdMetaVariable.h | 7 +++++++ 6 files changed, 62 insertions(+), 8 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 23f148da0..648db72a4 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -172,7 +172,12 @@ namespace storm { } void Dd::setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue) { - // TODO: Fill this + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableNameToValueMap) { + valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + } + + this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); } bool Dd::containsMetaVariable(std::string const& metaVariableName) const { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index b0a3e33eb..215e7e6a7 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -19,8 +19,9 @@ namespace storm { 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() = default; Dd(Dd const& other) = default; Dd(Dd&& other) = default; Dd& operator=(Dd const& other) = default; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 40c11fbaa..cce1edbfe 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -18,9 +18,34 @@ namespace storm { Dd DdManager::getConstant(double value) { return Dd(this->shared_from_this(), cuddManager.constant(value), {""}); } + + Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { + std::vector> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); + + Dd result; + if (value & (1ull << (ddVariables.size() - 1))) { + result = ddVariables[0]; + } else { + result = ddVariables[0]; + } + + for (std::size_t i = 1; i < ddVariables.size(); ++i) { + if (value & (1ull << (ddVariables.size() - i - 1))) { + result *= ddVariables[i]; + } else { + result *= ~ddVariables[i]; + } + } + + return result; + } void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { - std::size_t numberOfBits = std::log2(high - low); + if (high == low) { + throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; + } + + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); std::vector> variables; for (std::size_t i = 0; i < numberOfBits; ++i) { @@ -36,7 +61,7 @@ namespace storm { } // Add the variables in interleaved order. - std::size_t numberOfBits = std::log2(high - low); + std::size_t numberOfBits = static_cast(std::ceil(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) { diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index ede42104d..1d061b504 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -14,7 +14,8 @@ namespace storm { namespace dd { template<> - class DdManager : std::enable_shared_from_this> { + class DdManager : public std::enable_shared_from_this> { + public: // To break the cylic dependencies, we need to forward-declare the other DD-related classes. friend class Dd; @@ -50,6 +51,17 @@ namespace storm { */ Dd getConstant(double value); + /*! + * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + * + * @param metaVariableName The meta variable that is supposed to have the given value. + * @param value The value the meta variable is supposed to have. + * @return The DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + */ + Dd getEncoding(std::string const& metaVariableName, int_fast64_t value); + /*! * Adds a meta variable with the given name and range. * diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index d5cae858c..72e7baba5 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,9 +4,8 @@ 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) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) { + 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), cube(manager->getOne()), 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; } @@ -27,6 +26,11 @@ namespace storm { return this->high; } + template + std::size_t DdMetaVariable::getNumberOfDdVariables() const { + return this->ddVariables.size(); + } + template std::shared_ptr> DdMetaVariable::getDdManager() const { return this->manager; @@ -43,6 +47,6 @@ namespace storm { } // Explicitly instantiate DdMetaVariable. - template<> class DdMetaVariable; + template class DdMetaVariable; } } \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 6bf5f6c3c..c5e7c00cf 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -65,6 +65,13 @@ namespace storm { */ std::shared_ptr> getDdManager() const; + + /*! + * Retrieves the number of DD variables for this meta variable. + * + * @return The number of DD variables for this meta variable. + */ + std::size_t getNumberOfDdVariables() const; private: /*! * Retrieves the variables used to encode the meta variable. From a63cda69f56f4586e5b7ec10ce3599d85a14042a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Mar 2014 13:09:36 +0100 Subject: [PATCH 05/20] Added function to retrieve range DD for meta variable. Former-commit-id: 32ef6715f429172331027fd8b9919e0934a0fa1e --- src/storage/dd/CuddDdManager.cpp | 10 ++++++++++ src/storage/dd/CuddDdManager.h | 9 +++++++++ 2 files changed, 19 insertions(+) diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index cce1edbfe..15f51a3b7 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -39,6 +39,16 @@ namespace storm { return result; } + + Dd DdManager::getRange(std::string const metaVariableName) { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + + Dd result = this->getZero(); + for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { + result.setValue(metaVariableName, value - metaVariable.getLow(), static_cast(value)); + } + return result; + } void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { if (high == low) { diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 1d061b504..b826cce35 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -62,6 +62,15 @@ namespace storm { */ Dd getEncoding(std::string const& metaVariableName, int_fast64_t value); + /*! + * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values + * of the range of the meta variable to one. + * + * @param metaVariableName The name of the meta variable whose range to retrieve. + * @return The range of the meta variable + */ + Dd getRange(std::string const metaVariableName); + /*! * Adds a meta variable with the given name and range. * From c2c353f6b9e929966ac4c86b6c758561900df05e Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Mar 2014 16:17:43 +0100 Subject: [PATCH 06/20] Readded missing file. Former-commit-id: acc68213d496fce4c7332093e0c5f2a182c639bd --- CPackConfig.cmake | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 CPackConfig.cmake diff --git a/CPackConfig.cmake b/CPackConfig.cmake new file mode 100644 index 000000000..5ce6c0f53 --- /dev/null +++ b/CPackConfig.cmake @@ -0,0 +1,27 @@ +include(InstallRequiredSystemLibraries) + +# For help take a look at: +# http://www.cmake.org/Wiki/CMake:CPackConfiguration + +### general settings +set(CPACK_PACKAGE_NAME "StoRM") +set(CPACK_PACKAGE_VENDOR "i2 RWTH Aachen University") +set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Stochastic Reward Model Checker - An extensible model checker written in C++.") + +set(CPACK_RESOURCE_FILE_LICENSE "${CMAKE_SOURCE_DIR}/LICENSE") + +### versions +set(CPACK_PACKAGE_VERSION_MAJOR "${STORM_CPP_VERSION_MAJOR}") +set(CPACK_PACKAGE_VERSION_MINOR "${STORM_CPP_VERSION_MINOR}") +set(CPACK_PACKAGE_VERSION_PATCH "${STORM_CPP_VERSION_PATCH}") +set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION_MAJOR}.${CPACK_PACKAGE_VERSION_MINOR}.${CPACK_PACKAGE_VERSION_PATCH}-${STORM_CPP_VERSION_HASH}") + +set(CPACK_GENERATOR "ZIP") +set(CPACK_PACKAGE_INSTALL_DIRECTORY "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}") + +### source package settings +set(CPACK_SOURCE_GENERATOR "ZIP") +set(CPACK_SOURCE_IGNORE_FILES "~$;[.]swp$;/[.]svn/;/[.]git/;.gitignore;/build/;tags;cscope.*") +set(CPACK_SOURCE_PACKAGE_FILE_NAME "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}-src") + +include(CPack) \ No newline at end of file From 52cd48c247d174febad28c979d99fb8127998efd Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Mar 2014 17:19:39 +0100 Subject: [PATCH 07/20] Fixed bug in restriction of a program to certain commands. Also, modules may now have an action without actually having a command labeled with the action and the explicit model adapter now handles this correctly. Former-commit-id: 6bbb4b807cbe6ed7f005a0b645c5a3b094854d20 --- src/adapters/ExplicitModelAdapter.h | 7 +++++++ src/ir/Module.cpp | 17 +++++++++++++++++ src/ir/Module.h | 6 +----- 3 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a2932b9c9..f1ef50396 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -233,6 +233,13 @@ namespace storm { } std::set const& commandIndices = module.getCommandsByAction(action); + + // If the module contains the action, but there is no command in the module that is labeled with + // this action, we don't have any feasible command combinations. + if (commandIndices.empty()) { + return boost::optional>>(); + } + std::list commands; // Look up commands by their indices and add them if the guard evaluates to true in the given state. diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 6b67ee579..5724db8df 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -169,11 +169,16 @@ namespace storm { if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { return actionsCommandSetPair->second; } + LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module."); throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module."; } void Module::collectActions() { + // Clear the current mapping. + this->actionsToCommandIndexMap.clear(); + + // Add the mapping for all commands. for (unsigned int id = 0; id < this->commands.size(); id++) { std::string const& action = this->commands[id].getActionName(); if (action != "") { @@ -184,9 +189,18 @@ namespace storm { this->actions.insert(action); } } + + // For all actions that are "in the module", but for which no command exists, we add the mapping to an empty + // set of commands. + for (auto const& action : this->actions) { + if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { + this->actionsToCommandIndexMap[action] = std::set(); + } + } } void Module::restrictCommands(boost::container::flat_set const& indexSet) { + // First construct the new vector of commands. std::vector newCommands; for (auto const& command : commands) { if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { @@ -194,6 +208,9 @@ namespace storm { } } commands = std::move(newCommands); + + // Then refresh the internal mappings. + this->collectActions(); } } // namespace ir diff --git a/src/ir/Module.h b/src/ir/Module.h index e6762bb8d..d9570c652 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -188,8 +188,8 @@ namespace storm { * @param indexSet The set of indices for which to keep the commands. */ void restrictCommands(boost::container::flat_set const& indexSet); - private: + private: /*! * Computes the locally maintained mappings for fast data retrieval. */ @@ -217,11 +217,7 @@ namespace storm { std::set actions; // A map of actions to the set of commands labeled with this action. -#ifdef LINUX - boost::container::map> actionsToCommandIndexMap; -#else std::map> actionsToCommandIndexMap; -#endif }; } // namespace ir From dea56e1bd407984b00b63ef974744e47c7af37e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 00:08:23 +0100 Subject: [PATCH 08/20] Added some missing includes and some stubs for additional functionality of DD abstraction layer. Former-commit-id: d90d525993228f8d5255c6cbd1950e6f781e4f10 --- src/storage/dd/CuddDd.cpp | 80 +++++++++++++++++++++++++++++--- src/storage/dd/CuddDd.h | 57 +++++++++++++++++++++++ src/storage/dd/CuddDdManager.cpp | 2 + 3 files changed, 132 insertions(+), 7 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 648db72a4..2b1648a8c 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,12 +1,18 @@ #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } + bool Dd::operator==(Dd const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); + } + Dd Dd::operator+(Dd const& other) const { Dd result(*this); result += other; @@ -14,7 +20,7 @@ namespace storm { } Dd& Dd::operator+=(Dd const& other) { - cuddAdd += other.getCuddAdd(); + this->getCuddAdd() += other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -29,7 +35,7 @@ namespace storm { } Dd& Dd::operator*=(Dd const& other) { - cuddAdd *= other.getCuddAdd(); + this->getCuddAdd() *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -44,7 +50,7 @@ namespace storm { } Dd& Dd::operator-=(Dd const& other) { - cuddAdd -= other.getCuddAdd(); + this->getCuddAdd() -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -59,7 +65,7 @@ namespace storm { } Dd& Dd::operator/=(Dd const& other) { - cuddAdd.Divide(other.getCuddAdd()); + this->getCuddAdd().Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -74,7 +80,7 @@ namespace storm { } Dd& Dd::complement() { - cuddAdd = ~cuddAdd; + this->getCuddAdd() = ~this->getCuddAdd(); return *this; } @@ -118,6 +124,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -129,6 +141,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -140,6 +158,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -151,6 +175,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -158,6 +188,30 @@ namespace storm { this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); } + uint_fast64_t Dd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariableName : this->containedMetaVariableNames) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); + } + return static_cast(this->cuddAdd.CountMinterm(static_cast(numberOfDdVariables))); + } + + uint_fast64_t Dd::getLeafCount() const { + return static_cast(this->cuddAdd.CountLeaves()); + } + + double Dd::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); + // FIXME + return 0; + } + + double Dd::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); + // FIXME + return 0; + } + void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { std::unordered_map metaVariableNameToValueMap; metaVariableNameToValueMap.emplace(metaVariableName, variableValue); @@ -177,7 +231,15 @@ namespace storm { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); } - this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + } + + bool Dd::isOne() const { + return *this == this->getDdManager()->getOne(); + } + + bool Dd::isZero() const { + return *this == this->getDdManager()->getZero(); } bool Dd::containsMetaVariable(std::string const& metaVariableName) const { @@ -197,7 +259,11 @@ namespace storm { } std::unordered_set const& Dd::getContainedMetaVariableNames() const { - return containedMetaVariableNames; + return this->containedMetaVariableNames; + } + + std::unordered_set& Dd::getContainedMetaVariableNames() { + return this->containedMetaVariableNames; } void Dd::exportToDot(std::string const& filename) const { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 215e7e6a7..ffb82f400 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/dd/Dd.h" @@ -27,6 +28,13 @@ namespace storm { Dd& operator=(Dd const& other) = default; Dd& operator=(Dd&& other) = default; + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + */ + bool operator==(Dd const& other) const; + /*! * Adds the two DDs. * @@ -194,6 +202,34 @@ namespace storm { */ void maxAbstract(std::unordered_set const& metaVariableNames); + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + uint_fast64_t getNonZeroCount() const; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + double getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + double getMax() const; + /*! * Sets the function values of all encodings that have the given value of the meta variable to the given * target value. @@ -231,6 +267,20 @@ namespace storm { */ void setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue); + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + /*! * Retrieves whether the given meta variable is contained in the DD. * @@ -254,6 +304,13 @@ namespace storm { */ std::unordered_set const& getContainedMetaVariableNames() 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& getContainedMetaVariableNames(); + /*! * Exports the DD to the given file in the dot format. * diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 15f51a3b7..1c691522d 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h" From 4252a2710c44f159aaa4b460464e5daa767f18ff Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 14:19:06 +0100 Subject: [PATCH 09/20] Renamed CPackConfig.cmake to StormCPackConfig.cmake and adapted reference in CMakeLists.txt accordingly. Also, CPackConfig.cmake is now ignored. Former-commit-id: d24d731950d8c307dcec44ee1c6e2e0614f24f70 --- .gitignore | 1 + CMakeLists.txt | 2 +- CPackConfig.cmake => StormCPackConfig.cmake | 0 3 files changed, 2 insertions(+), 1 deletion(-) rename CPackConfig.cmake => StormCPackConfig.cmake (100%) diff --git a/.gitignore b/.gitignore index 8d18b13b4..aa15c7b9a 100644 --- a/.gitignore +++ b/.gitignore @@ -33,6 +33,7 @@ resources/3rdparty/cudd-2.5.0/ ipch/ obj/ CMakeFiles/ +CPackConfig.cmake # The build Dir build/ build//CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 8942c984f..5831d731f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -519,4 +519,4 @@ INSTALL(TARGETS storm storm-functional-tests storm-performance-tests LIBRARY DESTINATION lib ARCHIVE DESTINATION lib ) -include(CPackConfig.cmake) \ No newline at end of file +include(StormCPackConfig.cmake) \ No newline at end of file diff --git a/CPackConfig.cmake b/StormCPackConfig.cmake similarity index 100% rename from CPackConfig.cmake rename to StormCPackConfig.cmake From ac355a66eb55869675d19eaa057c4b88e10d39f5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 16:04:40 +0100 Subject: [PATCH 10/20] Further work on DD layer. Former-commit-id: 061b428763617ec66c61eed91f0a9f7dd1d9bc56 --- src/storage/dd/CuddDd.cpp | 45 +++++++++++++++++++++++++++++++++++---- src/storage/dd/CuddDd.h | 29 +++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 4 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 2b1648a8c..6276a422b 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -188,6 +188,33 @@ namespace storm { this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); } + void Dd::swapVariables(std::vector> const& metaVariablePairs) { + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { + throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; + } + + // Keep track of the contained meta variables in the DD. + bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); + bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); + if (containsVariable1 && !containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.first); + this->addContainedMetaVariable(metaVariablePair.second); + } else if (!containsVariable1 && containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.second); + this->addContainedMetaVariable(metaVariablePair.first); + } + } + + // FIXME: complete this and add matrix-matrix multiplication. + } + uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariableName : this->containedMetaVariableNames) { @@ -200,16 +227,18 @@ namespace storm { return static_cast(this->cuddAdd.CountLeaves()); } + uint_fast64_t Dd::getNodeCount() const { + return static_cast(this->cuddAdd.nodeCount()); + } + double Dd::getMin() const { ADD constantMinAdd = this->getCuddAdd().FindMin(); - // FIXME - return 0; + return static_cast(Cudd_V(constantMinAdd)); } double Dd::getMax() const { ADD constantMaxAdd = this->getCuddAdd().FindMax(); - // FIXME - return 0; + return static_cast(Cudd_V(constantMaxAdd)); } void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { @@ -280,6 +309,14 @@ namespace storm { return this->cuddAdd; } + void Dd::addContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().insert(metaVariableName); + } + + void Dd::removeContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().erase(metaVariableName); + } + std::shared_ptr> Dd::getDdManager() const { return this->ddManager; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index ffb82f400..a07db98d6 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -202,6 +202,14 @@ namespace storm { */ void maxAbstract(std::unordered_set const& metaVariableNames); + /*! + * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have + * the same number of underlying DD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + */ + void swapVariables(std::vector> const& metaVariablePairs); + /*! * Retrieves the number of encodings that are mapped to a non-zero value. * @@ -216,6 +224,13 @@ namespace storm { */ uint_fast64_t getLeafCount() const; + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + uint_fast64_t getNodeCount() const; + /*! * Retrieves the lowest function value of any encoding. * @@ -340,6 +355,20 @@ namespace storm { */ ADD const& getCuddAdd() const; + /*! + * Adds the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to add. + */ + void addContainedMetaVariable(std::string const& metaVariableName); + + /*! + * Removes the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to remove. + */ + void removeContainedMetaVariable(std::string const& metaVariableName); + /*! * Creates a DD that encapsulates the given CUDD ADD. * From cb35b3315daad61e20ddff3f7aa89104e210787c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 22:32:51 +0100 Subject: [PATCH 11/20] Added matrix-matrix multiplication to DD interface. (This includes matrix-vector multiplication as a special case). Former-commit-id: d5d8fef7386f39402514540143f19b73a147ae68 --- src/storage/dd/CuddDd.cpp | 54 ++++++++++++++++++++++++-------- src/storage/dd/CuddDd.h | 31 ++++++++++++------ src/storage/dd/CuddDdManager.cpp | 4 +-- src/storage/dd/CuddDdManager.h | 3 +- 4 files changed, 65 insertions(+), 27 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 6276a422b..be51d5a98 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -5,7 +5,7 @@ namespace storm { namespace dd { - Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } @@ -23,7 +23,7 @@ namespace storm { this->getCuddAdd() += other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -38,7 +38,7 @@ namespace storm { this->getCuddAdd() *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -53,7 +53,7 @@ namespace storm { this->getCuddAdd() -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -68,7 +68,7 @@ namespace storm { this->getCuddAdd().Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -120,7 +120,7 @@ namespace storm { return result; } - void Dd::existsAbstract(std::unordered_set const& metaVariableNames) { + void Dd::existsAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -137,7 +137,7 @@ namespace storm { this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); } - void Dd::sumAbstract(std::unordered_set const& metaVariableNames) { + void Dd::sumAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -154,7 +154,7 @@ namespace storm { this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); } - void Dd::minAbstract(std::unordered_set const& metaVariableNames) { + void Dd::minAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -171,7 +171,7 @@ namespace storm { this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); } - void Dd::maxAbstract(std::unordered_set const& metaVariableNames) { + void Dd::maxAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -210,11 +210,39 @@ namespace storm { this->removeContainedMetaVariable(metaVariablePair.second); this->addContainedMetaVariable(metaVariablePair.first); } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddAdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddAdd()); + } } - // FIXME: complete this and add matrix-matrix multiplication. + // Finally, call CUDD to swap the variables. + this->getCuddAdd().SwapVariables(from, to); } + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + std::vector summationDdVariables; + + // Create the CUDD summation variables. + for (auto const& metaVariableName : summationMetaVariableNames) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariableName).getDdVariables()) { + summationDdVariables.push_back(ddVariable.getCuddAdd()); + } + } + + std::set unionOfMetaVariableNames; + std::set_union(this->getContainedMetaVariableNames().begin(), this->getContainedMetaVariableNames().end(), otherMatrix.getContainedMetaVariableNames().begin(), otherMatrix.getContainedMetaVariableNames().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); + std::set containedMetaVariableNames; + std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); + + return Dd(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); + } + + uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariableName : this->containedMetaVariableNames) { @@ -276,7 +304,7 @@ namespace storm { return metaVariable != containedMetaVariableNames.end(); } - bool Dd::containsMetaVariables(std::unordered_set metaVariableNames) const { + bool Dd::containsMetaVariables(std::set metaVariableNames) const { for (auto const& metaVariableName : metaVariableNames) { auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); @@ -287,11 +315,11 @@ namespace storm { return true; } - std::unordered_set const& Dd::getContainedMetaVariableNames() const { + std::set const& Dd::getContainedMetaVariableNames() const { return this->containedMetaVariableNames; } - std::unordered_set& Dd::getContainedMetaVariableNames() { + std::set& Dd::getContainedMetaVariableNames() { return this->containedMetaVariableNames; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index a07db98d6..0aa71889e 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -1,8 +1,8 @@ #ifndef STORM_STORAGE_DD_CUDDDD_H_ #define STORM_STORAGE_DD_CUDDDD_H_ -#include #include +#include #include #include "src/storage/dd/Dd.h" @@ -179,28 +179,28 @@ namespace storm { * * @param metaVariableNames The names of all meta variables from which to abstract. */ - void existsAbstract(std::unordered_set const& metaVariableNames); + void existsAbstract(std::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); + void sumAbstract(std::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); + void minAbstract(std::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); + void maxAbstract(std::set const& metaVariableNames); /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have @@ -210,6 +210,17 @@ namespace storm { */ void swapVariables(std::vector> const& metaVariablePairs); + /*! + * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariableNames The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return A DD representing the result of the matrix-matrix multiplication. + */ + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + /*! * Retrieves the number of encodings that are mapped to a non-zero value. * @@ -310,21 +321,21 @@ namespace storm { * @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; + bool containsMetaVariables(std::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; + std::set const& getContainedMetaVariableNames() 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& getContainedMetaVariableNames(); + std::set& getContainedMetaVariableNames(); /*! * Exports the DD to the given file in the dot format. @@ -376,7 +387,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept; + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept; // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; @@ -385,7 +396,7 @@ namespace storm { ADD cuddAdd; // The names of all meta variables that appear in this DD. - std::unordered_set containedMetaVariableNames; + std::set containedMetaVariableNames; }; } } diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 1c691522d..e6ca9e8e7 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -97,8 +97,8 @@ namespace storm { return nameVariablePair->second; } - std::unordered_set DdManager::getAllMetaVariableNames() const { - std::unordered_set result; + std::set DdManager::getAllMetaVariableNames() const { + std::set result; for (auto const& nameValuePair : metaVariableMap) { result.insert(nameValuePair.first); } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index b826cce35..76da42bd5 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -1,7 +1,6 @@ #ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ #define STORM_STORAGE_DD_CUDDDDMANAGER_H_ -#include #include #include "src/storage/dd/DdManager.h" @@ -102,7 +101,7 @@ namespace storm { * * @return The set of all meta variable names of the manager. */ - std::unordered_set getAllMetaVariableNames() const; + std::set getAllMetaVariableNames() const; private: /*! From d6ff967ef04a898476c7864cba562bec7777325e Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Mar 2014 10:20:02 +0100 Subject: [PATCH 12/20] Added missing algorithm header inclusion. Former-commit-id: 32231ecb8d0e8927cbde64c33b8a1cc667b855eb --- src/storage/dd/CuddDd.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index be51d5a98..23db4562d 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" From 386fac39358c28a0848c6162aa995ae7af5d768b Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Mar 2014 10:37:26 +0100 Subject: [PATCH 13/20] Removed faulty deletion of cudd utility (is obsolete now anyway). Former-commit-id: c4dca6c50fa8762fc53ad24fbc2b2c62ff5eafda --- src/storm.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm.cpp b/src/storm.cpp index ef23b9f2f..81e77cf11 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -240,7 +240,7 @@ void setUp() { * Performs some necessary clean-up. */ void cleanUp() { - delete storm::utility::cuddUtilityInstance(); + // Intentionally left empty. } /*! From 7ea7ce93e22852a5593c38bd9bee8d3f14d78535 Mon Sep 17 00:00:00 2001 From: dbohlender Date: Thu, 27 Mar 2014 10:58:41 +0100 Subject: [PATCH 14/20] Fixed MSVC incompabilities Former-commit-id: 67749daab8f6873c66d6b45048db02ebfc8c5f0f --- src/storage/dd/CuddDd.cpp | 4 +++- src/storage/dd/CuddDd.h | 11 +++++++---- src/storage/dd/CuddDdManager.cpp | 2 +- src/storage/dd/CuddDdManager.h | 13 +++++++++---- src/storage/dd/DdMetaVariable.cpp | 2 +- src/storage/dd/DdMetaVariable.h | 13 +++++++++---- 6 files changed, 30 insertions(+), 15 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index be51d5a98..873107d27 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" @@ -5,7 +7,7 @@ namespace storm { namespace dd { - Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 0aa71889e..74a1a6c7f 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -6,6 +6,7 @@ #include #include "src/storage/dd/Dd.h" +#include "utility\OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -24,9 +25,11 @@ namespace storm { // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; Dd(Dd const& other) = default; - Dd(Dd&& other) = default; - Dd& operator=(Dd const& other) = default; - Dd& operator=(Dd&& other) = default; + Dd& operator=(Dd const& other) = default; + #ifndef WINDOWS + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; + #endif /*! * Retrieves whether the two DDs represent the same function. @@ -387,7 +390,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept; + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames); // 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 e6ca9e8e7..931b968d9 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -5,7 +5,7 @@ namespace storm { namespace dd { - DdManager::DdManager() noexcept : metaVariableMap(), cuddManager() { + DdManager::DdManager() : metaVariableMap(), cuddManager() { // Intentionally left empty. } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 76da42bd5..25feb01cf 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -6,6 +6,7 @@ #include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/storage/dd/CuddDd.h" +#include "utility\OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -21,13 +22,17 @@ namespace storm { /*! * Creates an empty manager without any meta variables. */ - DdManager() noexcept; + DdManager(); // Explictly forbid copying a DdManager, but allow moving it. DdManager(DdManager const& other) = delete; - DdManager(DdManager&& other) = default; - DdManager& operator=(DdManager const& other) = delete; - DdManager& operator=(DdManager&& other) = default; + DdManager& operator=(DdManager const& other) = delete; + #ifndef WINDOWS + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager&& other) = default; + #endif + + /*! * Retrieves a DD representing the constant one function. diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 72e7baba5..7671289fc 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,7 +4,7 @@ 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) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + 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), cube(manager->getOne()), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { this->cube *= ddVariable; diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index c5e7c00cf..2212cf265 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -6,6 +6,7 @@ #include #include +#include "utility\OsDetection.h" #include "src/storage/dd/CuddDd.h" namespace storm { @@ -29,13 +30,17 @@ 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) noexcept; + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; - DdMetaVariable(DdMetaVariable&& other) = default; - DdMetaVariable& operator=(DdMetaVariable const& other) = default; - DdMetaVariable& operator=(DdMetaVariable&& other) = default; + DdMetaVariable& operator=(DdMetaVariable const& other) = default; + #ifndef WINDOWS + DdMetaVariable(DdMetaVariable&& other) = default; + DdMetaVariable& operator=(DdMetaVariable&& other) = default; + #endif + + /*! * Retrieves the name of the meta variable. From dd15e6019383e0ca54137628f29d08690e0efa79 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Mar 2014 10:37:26 +0100 Subject: [PATCH 15/20] Removed faulty deletion of cudd utility (is obsolete now anyway). Former-commit-id: 743c59ceca680284a4bb6a23aac1a7e3081d6d31 --- src/storm.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm.cpp b/src/storm.cpp index ef23b9f2f..81e77cf11 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -240,7 +240,7 @@ void setUp() { * Performs some necessary clean-up. */ void cleanUp() { - delete storm::utility::cuddUtilityInstance(); + // Intentionally left empty. } /*! From 2fcb12e8752c5348e1042e5099e0a86341da13a7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Mar 2014 11:18:15 +0100 Subject: [PATCH 16/20] Fixed some backslashes in includes to slashes and changed indentation of some code. Former-commit-id: 0e4828e3685debe90a095d9a6f82298988f7fc87 --- src/storage/dd/CuddDd.h | 24 ++++++++++++------------ src/storage/dd/CuddDdManager.h | 16 +++++++--------- src/storage/dd/DdMetaVariable.h | 18 ++++++++---------- 3 files changed, 27 insertions(+), 31 deletions(-) diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 74a1a6c7f..414190b2e 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -6,7 +6,7 @@ #include #include "src/storage/dd/Dd.h" -#include "utility\OsDetection.h" +#include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -26,10 +26,10 @@ namespace storm { Dd() = default; Dd(Dd const& other) = default; Dd& operator=(Dd const& other) = default; - #ifndef WINDOWS - Dd(Dd&& other) = default; - Dd& operator=(Dd&& other) = default; - #endif +#ifndef WINDOWS + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; +#endif /*! * Retrieves whether the two DDs represent the same function. @@ -45,7 +45,7 @@ namespace storm { * @return The result of the addition. */ Dd operator+(Dd const& other) const; - + /*! * Adds the given DD to the current one. * @@ -61,7 +61,7 @@ namespace storm { * @return The result of the multiplication. */ Dd operator*(Dd const& other) const; - + /*! * Multiplies the given DD with the current one and assigns the result to the current DD. * @@ -183,7 +183,7 @@ namespace storm { * @param metaVariableNames The names of all meta variables from which to abstract. */ void existsAbstract(std::set const& metaVariableNames); - + /*! * Sum-abstracts from the given meta variables. * @@ -204,7 +204,7 @@ namespace storm { * @param metaVariableNames The names of all meta variables from which to abstract. */ void maxAbstract(std::set const& metaVariableNames); - + /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have * the same number of underlying DD variables. @@ -269,7 +269,7 @@ namespace storm { * @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. @@ -382,7 +382,7 @@ namespace storm { * @param metaVariableName The name of the meta variable to remove. */ void removeContainedMetaVariable(std::string const& metaVariableName); - + /*! * Creates a DD that encapsulates the given CUDD ADD. * @@ -394,7 +394,7 @@ namespace storm { // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; - + // The ADD created by CUDD. ADD cuddAdd; diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 25feb01cf..666376719 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -6,7 +6,7 @@ #include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/storage/dd/CuddDd.h" -#include "utility\OsDetection.h" +#include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -18,7 +18,7 @@ namespace storm { public: // To break the cylic dependencies, we need to forward-declare the other DD-related classes. friend class Dd; - + /*! * Creates an empty manager without any meta variables. */ @@ -27,12 +27,10 @@ namespace storm { // Explictly forbid copying a DdManager, but allow moving it. DdManager(DdManager const& other) = delete; DdManager& operator=(DdManager const& other) = delete; - #ifndef WINDOWS - DdManager(DdManager&& other) = default; - DdManager& operator=(DdManager&& other) = default; - #endif - - +#ifndef WINDOWS + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager&& other) = default; +#endif /*! * Retrieves a DD representing the constant one function. @@ -54,7 +52,7 @@ namespace storm { * @return A DD representing the constant function with the given value. */ Dd getConstant(double value); - + /*! * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal * to the given value one. diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 2212cf265..994b0841a 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -6,7 +6,7 @@ #include #include -#include "utility\OsDetection.h" +#include "utility/OsDetection.h" #include "src/storage/dd/CuddDd.h" namespace storm { @@ -35,12 +35,10 @@ namespace storm { // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; DdMetaVariable& operator=(DdMetaVariable const& other) = default; - #ifndef WINDOWS - DdMetaVariable(DdMetaVariable&& other) = default; - DdMetaVariable& operator=(DdMetaVariable&& other) = default; - #endif - - +#ifndef WINDOWS + DdMetaVariable(DdMetaVariable&& other) = default; + DdMetaVariable& operator=(DdMetaVariable&& other) = default; +#endif /*! * Retrieves the name of the meta variable. @@ -55,14 +53,14 @@ namespace storm { * @return The lowest value of the range of the variable. */ int_fast64_t getLow() const; - + /*! * Retrieves the highest value of the range of the variable. * * @return The highest value of the range of the variable. */ int_fast64_t getHigh() const; - + /*! * Retrieves the manager that is responsible for this meta variable. * @@ -91,7 +89,7 @@ namespace storm { * @return The cube of all variables that encode this meta variable. */ Dd const& getCube() const; - + // The name of the meta variable. std::string name; From a4fec9f080320283ee130ff08d8bee0e7b8016ec Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Mar 2014 15:13:38 +0100 Subject: [PATCH 17/20] Started writing functional tests for DD abstraction layer and fixed some bugs on the way. Former-commit-id: 8a2fc118bea53c4f82c1228402971b19631fee2b --- src/storage/dd/CuddDd.cpp | 4 +- src/storage/dd/CuddDd.h | 2 +- src/storage/dd/CuddDdManager.cpp | 47 +++++++++++++++++++--- src/storage/dd/CuddDdManager.h | 15 +++++++ test/functional/storage/CuddDdTest.cpp | 54 ++++++++++++++++++++++++++ 5 files changed, 114 insertions(+), 8 deletions(-) create mode 100644 test/functional/storage/CuddDdTest.cpp diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 873107d27..eba51a557 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -263,12 +263,12 @@ namespace storm { double Dd::getMin() const { ADD constantMinAdd = this->getCuddAdd().FindMin(); - return static_cast(Cudd_V(constantMinAdd)); + return static_cast(Cudd_V(constantMinAdd.getNode())); } double Dd::getMax() const { ADD constantMaxAdd = this->getCuddAdd().FindMax(); - return static_cast(Cudd_V(constantMaxAdd)); + return static_cast(Cudd_V(constantMaxAdd.getNode())); } void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 414190b2e..1f8339fe6 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -390,7 +390,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames); + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames = std::set()); // 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 931b968d9..d8a7096a0 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,8 +1,11 @@ #include +#include #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h" +#include + namespace storm { namespace dd { DdManager::DdManager() : metaVariableMap(), cuddManager() { @@ -10,15 +13,15 @@ namespace storm { } Dd DdManager::getOne() { - return Dd(this->shared_from_this(), cuddManager.addOne(), {""}); + return Dd(this->shared_from_this(), cuddManager.addOne()); } Dd DdManager::getZero() { - return Dd(this->shared_from_this(), cuddManager.addZero(), {""}); + return Dd(this->shared_from_this(), cuddManager.addZero()); } Dd DdManager::getConstant(double value) { - return Dd(this->shared_from_this(), cuddManager.constant(value), {""}); + return Dd(this->shared_from_this(), cuddManager.constant(value)); } Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { @@ -53,6 +56,12 @@ namespace storm { } void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + // Check whether a meta variable already exists. + if (this->containsMetaVariable(name)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; + } + + // Check that the range is legal. if (high == low) { throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; } @@ -68,13 +77,33 @@ namespace storm { } void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { + // Make sure that at least one meta variable is added. if (names.size() == 0) { throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables."; } + // Check that there are no duplicate names in the given name vector. + std::vector nameCopy(names); + std::sort(nameCopy.begin(), nameCopy.end()); + if (std::adjacent_find(nameCopy.begin(), nameCopy.end()) != nameCopy.end()) { + throw storm::exceptions::InvalidArgumentException() << "Cannot add duplicate meta variables."; + } + + // Check that the range is legal. + if (high == low) { + throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; + } + + // Check whether a meta variable already exists. + for (auto const& metaVariableName : names) { + if (this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists."; + } + } + // Add the variables in interleaved order. std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); - std::vector>> variables; + std::vector>> variables(names.size()); for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) { for (uint_fast64_t i = 0; i < names.size(); ++i) { variables[i].emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {names[i]})); @@ -90,7 +119,7 @@ namespace storm { DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { auto const& nameVariablePair = metaVariableMap.find(metaVariableName); - if (nameVariablePair == metaVariableMap.end()) { + if (!this->containsMetaVariable(metaVariableName)) { throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name."; } @@ -105,6 +134,14 @@ namespace storm { return result; } + std::size_t DdManager::getNumberOfMetaVariables() const { + return this->metaVariableMap.size(); + } + + bool DdManager::containsMetaVariable(std::string const& metaVariableName) const { + return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end(); + } + Cudd& DdManager::getCuddManager() { return this->cuddManager; } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 666376719..4e421f9ec 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -106,6 +106,21 @@ namespace storm { */ std::set getAllMetaVariableNames() const; + /*! + * Retrieves the number of meta variables that are contained in this manager. + * + * @return The number of meta variables contained in this manager. + */ + std::size_t getNumberOfMetaVariables() const; + + /*! + * Retrieves whether the given meta variable name is already in use. + * + * @param metaVariableName The meta variable name whose membership to query. + * @return True if the given meta variable name is managed by this manager. + */ + bool containsMetaVariable(std::string const& metaVariableName) const; + private: /*! * Retrieves the underlying CUDD manager. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp new file mode 100644 index 000000000..3a9b1dde9 --- /dev/null +++ b/test/functional/storage/CuddDdTest.cpp @@ -0,0 +1,54 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/DdMetaVariable.h" + +TEST(CuddDdManager, Constants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Dd zero; + ASSERT_NO_THROW(zero = manager->getZero()); + + EXPECT_EQ(0, zero.getNonZeroCount()); + EXPECT_EQ(1, zero.getLeafCount()); + EXPECT_EQ(1, zero.getNodeCount()); + EXPECT_EQ(0, zero.getMin()); + EXPECT_EQ(0, zero.getMax()); + + storm::dd::Dd one; + ASSERT_NO_THROW(one = manager->getOne()); + + EXPECT_EQ(1, one.getNonZeroCount()); + EXPECT_EQ(1, one.getLeafCount()); + EXPECT_EQ(1, one.getNodeCount()); + EXPECT_EQ(1, one.getMin()); + EXPECT_EQ(1, one.getMax()); + + storm::dd::Dd two; + ASSERT_NO_THROW(two = manager->getConstant(2)); + + EXPECT_EQ(1, two.getNonZeroCount()); + EXPECT_EQ(1, two.getLeafCount()); + EXPECT_EQ(1, two.getNodeCount()); + EXPECT_EQ(2, two.getMin()); + EXPECT_EQ(2, two.getMax()); +} + +TEST(CuddDdManager, AddMetaVariableTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + EXPECT_EQ(1, manager->getNumberOfMetaVariables()); + + std::vector names = {"x", "x'"}; + ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + + names = {"y", "y"}; + ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + + names = {"y", "y'"}; + ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3)); + EXPECT_EQ(3, manager->getNumberOfMetaVariables()); +} \ No newline at end of file From 6b07643c9623599800f45a90e528df85380ef0ca Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Mar 2014 16:57:55 +0100 Subject: [PATCH 18/20] Further tests for DD layer and bugfixing. Former-commit-id: 752a8c55ac6b506af523927c135343be9ab2b2c1 --- src/storage/dd/CuddDdManager.cpp | 12 ++++++------ src/storage/dd/CuddDdManager.h | 2 +- src/storage/dd/DdMetaVariable.h | 2 +- test/functional/storage/CuddDdTest.cpp | 21 +++++++++++++++++++-- 4 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index d8a7096a0..dd6ce4f4f 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -57,7 +57,7 @@ namespace storm { void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { // Check whether a meta variable already exists. - if (this->containsMetaVariable(name)) { + if (this->hasMetaVariable(name)) { throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; } @@ -66,7 +66,7 @@ namespace storm { throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; } - std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); std::vector> variables; for (std::size_t i = 0; i < numberOfBits; ++i) { @@ -96,13 +96,13 @@ namespace storm { // Check whether a meta variable already exists. for (auto const& metaVariableName : names) { - if (this->containsMetaVariable(metaVariableName)) { + if (this->hasMetaVariable(metaVariableName)) { throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists."; } } // Add the variables in interleaved order. - std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); std::vector>> variables(names.size()); for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) { for (uint_fast64_t i = 0; i < names.size(); ++i) { @@ -119,7 +119,7 @@ namespace storm { DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { auto const& nameVariablePair = metaVariableMap.find(metaVariableName); - if (!this->containsMetaVariable(metaVariableName)) { + if (!this->hasMetaVariable(metaVariableName)) { throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name."; } @@ -138,7 +138,7 @@ namespace storm { return this->metaVariableMap.size(); } - bool DdManager::containsMetaVariable(std::string const& metaVariableName) const { + bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end(); } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 4e421f9ec..1d0d32a99 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -119,7 +119,7 @@ namespace storm { * @param metaVariableName The meta variable name whose membership to query. * @return True if the given meta variable name is managed by this manager. */ - bool containsMetaVariable(std::string const& metaVariableName) const; + bool hasMetaVariable(std::string const& metaVariableName) const; private: /*! diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 994b0841a..f6c90cc21 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -68,13 +68,13 @@ namespace storm { */ std::shared_ptr> getDdManager() const; - /*! * Retrieves the number of DD variables for this meta variable. * * @return The number of DD variables for this meta variable. */ std::size_t getNumberOfDdVariables() const; + private: /*! * Retrieves the variables used to encode the meta variable. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 3a9b1dde9..a92dbc929 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -36,7 +36,7 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(2, two.getMax()); } -TEST(CuddDdManager, AddMetaVariableTest) { +TEST(CuddDdManager, MetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); @@ -51,4 +51,21 @@ TEST(CuddDdManager, AddMetaVariableTest) { names = {"y", "y'"}; ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3)); EXPECT_EQ(3, manager->getNumberOfMetaVariables()); -} \ No newline at end of file + + EXPECT_FALSE(manager->hasMetaVariable("x'")); + EXPECT_TRUE(manager->hasMetaVariable("y'")); + + std::set metaVariableSet = {"x", "y", "y'"}; + EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); + + ASSERT_THROW(storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x")); + storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x"); + + EXPECT_EQ(1, metaVariableX.getLow()); + EXPECT_EQ(9, metaVariableX.getHigh()); + EXPECT_EQ("x", metaVariableX.getName()); + EXPECT_EQ(manager, metaVariableX.getDdManager()); + EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables()); +} + From a528610d985d015f9f0307bc12bd39de17d1c0df Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 29 Mar 2014 15:04:32 +0100 Subject: [PATCH 19/20] version is now written into a seperate header file to prevent recompile of many files after a commit Former-commit-id: a287aacefa12dbab2516037840b10849fadda34e --- CMakeLists.txt | 7 +++++++ src/storm.cpp | 1 + storm-config.h.in | 7 ------- storm-version.h.in | 12 ++++++++++++ 4 files changed, 20 insertions(+), 7 deletions(-) create mode 100644 storm-version.h.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 5831d731f..09eef57a9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -216,6 +216,13 @@ configure_file ( "${PROJECT_SOURCE_DIR}/storm-config.h.in" "${PROJECT_BINARY_DIR}/include/storm-config.h" ) + +# Configure a header file to pass the storm version to the source code +configure_file ( + "${PROJECT_SOURCE_DIR}/storm-version.h.in" + "${PROJECT_BINARY_DIR}/include/storm-version.h" +) + # Add the binary dir include directory for storm-config.h include_directories("${PROJECT_BINARY_DIR}/include") diff --git a/src/storm.cpp b/src/storm.cpp index 81e77cf11..a13bf8e23 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -21,6 +21,7 @@ #include #include "storm-config.h" +#include "storm-version.h" #include "src/models/Dtmc.h" #include "src/models/MarkovAutomaton.h" #include "src/storage/SparseMatrix.h" diff --git a/storm-config.h.in b/storm-config.h.in index 85a33e032..cb90e5af6 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -8,13 +8,6 @@ #ifndef STORM_GENERATED_STORMCONFIG_H_ #define STORM_GENERATED_STORMCONFIG_H_ -// Version Information -#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ // The major version of StoRM -#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ // The minor version of StoRM -#define STORM_CPP_VERSION_PATCH @STORM_CPP_VERSION_PATCH@ // The patch version of StoRM -#define STORM_CPP_VERSION_COMMITS_AHEAD @STORM_CPP_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set -#define STORM_CPP_VERSION_HASH "@STORM_CPP_VERSION_HASH@" // The short hash of the git commit this build is bases on -#define STORM_CPP_VERSION_DIRTY @STORM_CPP_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else // The path of the sources from which StoRM will be/was build #define STORM_CPP_BASE_PATH "@PROJECT_SOURCE_DIR@" diff --git a/storm-version.h.in b/storm-version.h.in new file mode 100644 index 000000000..5ccac6125 --- /dev/null +++ b/storm-version.h.in @@ -0,0 +1,12 @@ +#ifndef STORM_GENERATED_VERSION_H_ +#define STORM_GENERATED_VERSION_H_ + +// Version Information +#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ // The major version of StoRM +#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ // The minor version of StoRM +#define STORM_CPP_VERSION_PATCH @STORM_CPP_VERSION_PATCH@ // The patch version of StoRM +#define STORM_CPP_VERSION_COMMITS_AHEAD @STORM_CPP_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set +#define STORM_CPP_VERSION_HASH "@STORM_CPP_VERSION_HASH@" // The short hash of the git commit this build is bases on +#define STORM_CPP_VERSION_DIRTY @STORM_CPP_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else + +#endif \ No newline at end of file From 0eb13c6415a7101b8f5527ce5d9699028537a182 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 29 Mar 2014 15:20:42 +0100 Subject: [PATCH 20/20] fixed a lot of unused variable warnings Former-commit-id: 806f74b30d501e2f463d99ea58f8b6a2d66a83ef --- src/adapters/SymbolicModelAdapter.h | 2 -- src/counterexamples/MILPMinimalLabelSetGenerator.h | 8 -------- src/models/MarkovAutomaton.h | 2 +- src/solver/GlpkLpSolver.cpp | 2 -- src/solver/GmmxxLinearEquationSolver.cpp | 1 - src/solver/GmmxxNondeterministicLinearEquationSolver.cpp | 1 - src/solver/NativeLinearEquationSolver.cpp | 1 - src/solver/NativeNondeterministicLinearEquationSolver.cpp | 1 - src/storage/BitVector.cpp | 2 -- src/storage/SparseMatrix.cpp | 1 - src/utility/vector.h | 1 - 11 files changed, 1 insertion(+), 21 deletions(-) diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index be0729729..29ab6c613 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -157,7 +157,6 @@ private: for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); - bool initialValue = booleanVariable.getInitialValue()->getValueAsBool(nullptr); *initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]); } for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { @@ -187,7 +186,6 @@ private: } bool changed; - int iter = 0; do { changed = false; *newReachableStates = *reachableStates * *systemAdd01; diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 027369182..de9c6b057 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -169,7 +169,6 @@ namespace storm { * @return A mapping from labels to variable indices. */ static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { - int error = 0; std::stringstream variableNameBuffer; std::unordered_map resultingMap; for (auto const& label : relevantLabels) { @@ -190,7 +189,6 @@ namespace storm { * @return A mapping from states to a list of choice variable indices. */ static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map> resultingMap; @@ -219,7 +217,6 @@ namespace storm { * @return A mapping from initial states to choice variable indices. */ static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -245,7 +242,6 @@ namespace storm { * @return A mapping from states to the index of the corresponding probability variables. */ static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -269,7 +265,6 @@ namespace storm { * @return The index of the variable for the probability of the virtual initial state. */ static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver, bool maximizeProbability = false) { - int error = 0; std::stringstream variableNameBuffer; variableNameBuffer << "pinit"; @@ -285,7 +280,6 @@ namespace storm { * @return A mapping from problematic states to the index of the corresponding variables. */ static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -329,7 +323,6 @@ namespace storm { * @return A mapping from problematic choices to the index of the corresponding variables. */ static std::pair, uint_fast64_t, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, uint_fast64_t, PairHash> resultingMap; @@ -539,7 +532,6 @@ namespace storm { */ static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - int error = 0; for (auto state : stateInformation.relevantStates) { std::vector coefficients; std::vector variables; diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 1f9250c10..22b6ab13f 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -123,7 +123,7 @@ namespace storm { } // Then compute how many rows the new matrix is going to have. - uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; + //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates() + 1); diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index e343526f2..e122fcb16 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -110,8 +110,6 @@ namespace storm { glp_set_row_name(this->lp, nextConstraintIndex, name.c_str()); // Determine the type of the constraint and add it properly. - bool isUpperBound = boundType == LESS || boundType == LESS_EQUAL; - bool isStrict = boundType == LESS || boundType == GREATER; switch (boundType) { case LESS: glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index f81f4267a..c7ef52247 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -152,7 +152,6 @@ namespace storm { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index 29829f535..1b408d740 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp @@ -59,7 +59,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index d55b4e2e5..d26ad0344 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -106,7 +106,6 @@ namespace storm { void NativeLinearEquationSolver::performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp index 5dc25f2c1..7f88258f1 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/src/solver/NativeNondeterministicLinearEquationSolver.cpp @@ -54,7 +54,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index b4b282e0b..6907c45be 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -200,7 +200,6 @@ namespace storm { } BitVector& BitVector::operator&=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { @@ -224,7 +223,6 @@ namespace storm { } BitVector& BitVector::operator|=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 0f8d0acfa..6955ec053 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -743,7 +743,6 @@ namespace storm { const_iterator it = this->begin(); const_iterator ite; typename std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::const_iterator rowIteratorEnd = rowIndications.end(); typename std::vector::iterator resultIterator = result.begin(); typename std::vector::iterator resultIteratorEnd = result.end(); diff --git a/src/utility/vector.h b/src/utility/vector.h index dd3bb2a1f..82913a902 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -94,7 +94,6 @@ namespace storm { */ template void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; for (uint_fast64_t i = 0; i < vector.size(); ++i) { vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; }