diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index aa3b7c675..6fbf38a11 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -12,7 +12,7 @@ namespace storm { } bool Dd::operator==(Dd const& other) const { - return this->getCuddAdd() == other.getCuddAdd(); + return this->cuddAdd == other.getCuddAdd(); } Dd Dd::operator+(Dd const& other) const { @@ -22,7 +22,7 @@ namespace storm { } Dd& Dd::operator+=(Dd const& other) { - this->getCuddAdd() += other.getCuddAdd(); + this->cuddAdd += other.getCuddAdd(); // Join the variable sets of the two participating DDs. this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); @@ -37,7 +37,7 @@ namespace storm { } Dd& Dd::operator*=(Dd const& other) { - this->getCuddAdd() *= other.getCuddAdd(); + this->cuddAdd *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); @@ -52,7 +52,7 @@ namespace storm { } Dd& Dd::operator-=(Dd const& other) { - this->getCuddAdd() -= other.getCuddAdd(); + this->cuddAdd -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); @@ -67,7 +67,7 @@ namespace storm { } Dd& Dd::operator/=(Dd const& other) { - this->getCuddAdd().Divide(other.getCuddAdd()); + this->cuddAdd.Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); @@ -82,7 +82,7 @@ namespace storm { } Dd& Dd::complement() { - this->getCuddAdd() = ~this->getCuddAdd(); + this->cuddAdd = ~this->cuddAdd; return *this; } @@ -136,7 +136,7 @@ namespace storm { cubeDd *= metaVariable.getCube(); } - this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); + this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()); } void Dd::sumAbstract(std::set const& metaVariableNames) { @@ -153,7 +153,7 @@ namespace storm { cubeDd *= metaVariable.getCube(); } - this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); + this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()); } void Dd::minAbstract(std::set const& metaVariableNames) { @@ -170,7 +170,7 @@ namespace storm { cubeDd *= metaVariable.getCube(); } - this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); + this->cuddAdd.Minimum(cubeDd.getCuddAdd()); } void Dd::maxAbstract(std::set const& metaVariableNames) { @@ -187,7 +187,7 @@ namespace storm { cubeDd *= metaVariable.getCube(); } - this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); + this->cuddAdd.Maximum(cubeDd.getCuddAdd()); } void Dd::swapVariables(std::vector> const& metaVariablePairs) { @@ -223,7 +223,7 @@ namespace storm { } // Finally, call CUDD to swap the variables. - this->getCuddAdd().SwapVariables(from, to); + this->cuddAdd.SwapVariables(from, to); } Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { @@ -241,7 +241,7 @@ namespace storm { 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); + return Dd(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); } @@ -262,35 +262,55 @@ namespace storm { } double Dd::getMin() const { - ADD constantMinAdd = this->getCuddAdd().FindMin(); + ADD constantMinAdd = this->cuddAdd.FindMin(); return static_cast(Cudd_V(constantMinAdd.getNode())); } double Dd::getMax() const { - ADD constantMaxAdd = this->getCuddAdd().FindMax(); + ADD constantMaxAdd = this->cuddAdd.FindMax(); return static_cast(Cudd_V(constantMaxAdd.getNode())); } void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { - std::unordered_map metaVariableNameToValueMap; + std::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; + std::map metaVariableNameToValueMap; metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1); metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2); this->setValue(metaVariableNameToValueMap, targetValue); } - void Dd::setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue) { + void Dd::setValue(std::map const& metaVariableNameToValueMap, double targetValue) { Dd valueEncoding(this->getDdManager()->getOne()); for (auto const& nameValuePair : metaVariableNameToValueMap) { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + // Also record that the DD now contains the meta variable. + this->addContainedMetaVariable(nameValuePair.first); } - this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + } + + double Dd::getValue(std::map const& metaVariableNameToValueMap) const { + std::set remainingMetaVariables(this->getContainedMetaVariableNames()); + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableNameToValueMap) { + valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + if (this->containsMetaVariable(nameValuePair.first)) { + remainingMetaVariables.erase(nameValuePair.first); + } + } + + if (!remainingMetaVariables.empty()) { + throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given."; + } + + Dd value = *this * valueEncoding; + return static_cast(Cudd_V(value.getCuddAdd().getNode())); } bool Dd::isOne() const { @@ -327,15 +347,15 @@ namespace storm { void Dd::exportToDot(std::string const& filename) const { if (filename.empty()) { - this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()}); + this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}); } else { FILE* filePointer = fopen(filename.c_str() , "w"); - this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()}, nullptr, nullptr, filePointer); + this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer); fclose(filePointer); } } - ADD& Dd::getCuddAdd() { + ADD Dd::getCuddAdd() { return this->cuddAdd; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 0255ae58e..0a665108e 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -1,7 +1,7 @@ #ifndef STORM_STORAGE_DD_CUDDDD_H_ #define STORM_STORAGE_DD_CUDDDD_H_ -#include +#include #include #include #include @@ -295,7 +295,16 @@ namespace storm { * 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); + void setValue(std::map const& metaVariableNameToValueMap, double targetValue); + + /*! + * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. + * Note that the mapping must specify values for all meta variables contained in the DD. + * + * @param metaVariableNameToValueMap A mapping of meta variable names to their values. + * @return The value of the function evaluated with the given input. + */ + double getValue(std::map const& metaVariableNameToValueMap) const; /*! * Retrieves whether this DD represents the constant one function. @@ -362,7 +371,7 @@ namespace storm { * * @return The CUDD ADD object associated with this DD. */ - ADD& getCuddAdd(); + ADD getCuddAdd(); /*! * Retrieves the CUDD ADD object associated with this DD. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 4b96e685a..3c87157b2 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -28,18 +28,23 @@ namespace storm { throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'."; } + DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + // Check whether the value is legal for this meta variable. - if (value < this->getMetaVariable(metaVariableName).getLow() || value > this->getMetaVariable(metaVariableName).getHigh()) { + if (value < metaVariable.getLow() || value > metaVariable.getHigh()) { throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'."; } - std::vector> const& ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); + // Now compute the encoding relative to the low value of the meta variable. + value -= metaVariable.getLow(); + + std::vector> const& ddVariables = metaVariable.getDdVariables(); Dd result; if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { - result = ddVariables[0]; + result = ~ddVariables[0]; } for (std::size_t i = 1; i < ddVariables.size(); ++i) { @@ -49,16 +54,37 @@ namespace storm { result *= ~ddVariables[i]; } } + + return result; + } + + Dd DdManager::getRange(std::string const& metaVariableName) { + // Check whether the meta variable exists. + if (!this->hasMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << 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, static_cast(1)); + } return result; } - Dd DdManager::getRange(std::string const metaVariableName) { + Dd DdManager::getIdentity(std::string const& metaVariableName) { + // Check whether the meta variable exists. + if (!this->hasMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << 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)); + result.setValue(metaVariableName, value, static_cast(value)); } return result; } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 1d0d32a99..569ccf1c9 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -69,9 +69,18 @@ namespace storm { * 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 + * @return The range of the meta variable. */ - Dd getRange(std::string const metaVariableName); + Dd getRange(std::string const& metaVariableName); + + /*! + * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal + * values of the range of the meta variable to themselves. + * + * @param metaVariableName The name of the meta variable whose identity to retrieve. + * @return The identity of the meta variable. + */ + Dd getIdentity(std::string const& metaVariableName); /*! * Adds a meta variable with the given name and range. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index fb6856c75..245b1f283 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, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); @@ -71,12 +71,39 @@ TEST(CuddDdManager, EncodingTest) { ASSERT_THROW(encoding = manager->getEncoding("x", 0), storm::exceptions::InvalidArgumentException); ASSERT_THROW(encoding = manager->getEncoding("x", 10), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(encoding = manager->getEncoding("x", 4)); - encoding.exportToDot("out.dot"); EXPECT_EQ(1, encoding.getNonZeroCount()); EXPECT_EQ(6, encoding.getNodeCount()); EXPECT_EQ(2, encoding.getLeafCount()); } +TEST(CuddDdManager, RangeTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + + storm::dd::Dd range; + ASSERT_THROW(range = manager->getRange("y"), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(range = manager->getRange("x")); + + EXPECT_EQ(9, range.getNonZeroCount()); + EXPECT_EQ(2, range.getLeafCount()); + EXPECT_EQ(6, range.getNodeCount()); +} + +TEST(CuddDdManager, IdentityTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + + storm::dd::Dd range; + ASSERT_THROW(range = manager->getIdentity("y"), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(range = manager->getIdentity("x")); + + EXPECT_EQ(9, range.getNonZeroCount()); + EXPECT_EQ(10, range.getLeafCount()); + EXPECT_EQ(21, range.getNodeCount()); +} + TEST(CuddDdMetaVariable, AccessorTest) { std::shared_ptr> manager(new storm::dd::DdManager());