From 6b07643c9623599800f45a90e528df85380ef0ca Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Mar 2014 16:57:55 +0100 Subject: [PATCH] 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()); +} +