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