diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 087382c71..fd26a782c 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -3,6 +3,7 @@ #include #include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/Settings.h" @@ -49,17 +50,9 @@ namespace storm { } Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { - // Check whether the meta variable exists. - if (!this->hasMetaVariable(metaVariableName)) { - 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 < metaVariable.getLow() || value > metaVariable.getHigh()) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'."; - } + LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'."); // Now compute the encoding relative to the low value of the meta variable. value -= metaVariable.getLow(); @@ -85,11 +78,6 @@ namespace storm { } 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(); @@ -101,11 +89,6 @@ namespace storm { } 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(); @@ -116,91 +99,57 @@ namespace storm { } void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + // Check whether the variable name is legal. + LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); + // Check whether a meta variable already exists. - if (this->hasMetaVariable(name)) { - throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; - } + LOG_THROW(!this->hasMetaVariable(name), 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."; - } + LOG_THROW(high != low, 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 + 1))); std::vector> variables; + std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name + "'"})); + } + + // Now group the non-primed and primed variable. + for (uint_fast64_t i = 0; i < numberOfBits; ++i) { + this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); } metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); + metaVariableMap.emplace(name + "'", DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); } void DdManager::addMetaVariable(std::string const& name) { + // Check whether the variable name is legal. + LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); + // Check whether a meta variable already exists. - if (this->hasMetaVariable(name)) { - throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; - } + LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); std::vector> variables; + std::vector> variablesPrime; variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); - - metaVariableMap.emplace(name, DdMetaVariable(name, variables, this->shared_from_this())); - } - - void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup) { - // 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."; - } + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name + "'"})); - // Check whether a meta variable already exists. - for (auto const& metaVariableName : names) { - 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 + 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) { - variables[i].emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {names[i]})); - } - } - - // If required, we group the bits on the same layer of the interleaved meta variables. - if (fixedGroup) { - for (uint_fast64_t i = 0; i < names.size(); ++i) { - this->getCuddManager().MakeTreeNode(variables[i].front().getCuddAdd().NodeReadIndex(), names.size(), MTR_FIXED); - } - } + // Now group the non-primed and primed variable. + this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); - // Now add the meta variables. - for (uint_fast64_t i = 0; i < names.size(); ++i) { - metaVariableMap.emplace(names[i], DdMetaVariable(names[i], low, high, variables[i], this->shared_from_this())); - } + metaVariableMap.emplace(name, DdMetaVariable(name, variables, this->shared_from_this())); + metaVariableMap.emplace(name + "'", DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); } DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { auto const& nameVariablePair = metaVariableMap.find(metaVariableName); - if (!this->hasMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'."; - } + // Check whether the meta variable exists. + LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'."); return nameVariablePair->second; } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 6fba4d254..a4607a57c 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -16,6 +16,7 @@ namespace storm { class DdManager : public std::enable_shared_from_this> { public: friend class Dd; + friend class DdForwardIterator; /*! * Creates an empty manager without any meta variables. @@ -83,7 +84,7 @@ namespace storm { /*! * Adds an integer meta variable with the given name and range. * - * @param name The name of the meta variable. + * @param name The (non-empty) 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. */ @@ -92,30 +93,10 @@ namespace storm { /*! * Adds a boolean meta variable with the given name. * - * @param name The name of the meta variable. + * @param name The (non-empty) name of the meta variable. */ void addMetaVariable(std::string const& name); - /*! - * Adds integer 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. - * @param fixedGroup If set to true, the interleaved bits of the meta variable are always kept together as - * a group during a potential reordering. - */ - void addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup = 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 names of all meta variables that have been added to the manager. * @@ -157,6 +138,15 @@ namespace storm { */ void triggerReordering(); + protected: + /*! + * 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; + private: /*! * Retrieves a list of names of the DD variables in the order of their index. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index ce40c94d1..f39e4ad48 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -38,26 +38,18 @@ TEST(CuddDdManager, Constants) { TEST(CuddDdManager, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); - EXPECT_EQ(1, manager->getNumberOfMetaVariables()); + EXPECT_EQ(2, manager->getNumberOfMetaVariables()); - std::vector names = {"x", "x'"}; - ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException); - names = {"y", "y"}; - ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3)); + EXPECT_EQ(4, manager->getNumberOfMetaVariables()); - names = {"y", "y'"}; - ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3)); - EXPECT_EQ(3, manager->getNumberOfMetaVariables()); - - EXPECT_FALSE(manager->hasMetaVariable("x'")); + EXPECT_TRUE(manager->hasMetaVariable("x'")); EXPECT_TRUE(manager->hasMetaVariable("y'")); - std::set metaVariableSet = {"x", "y", "y'"}; + std::set metaVariableSet = {"x", "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")); } TEST(CuddDdManager, EncodingTest) { @@ -99,20 +91,6 @@ TEST(CuddDdManager, IdentityTest) { EXPECT_EQ(21, range.getNodeCount()); } -TEST(CuddDdMetaVariable, AccessorTest) { - std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); - EXPECT_EQ(1, manager->getNumberOfMetaVariables()); - 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()); -} - TEST(CuddDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); manager->addMetaVariable("x", 1, 9); @@ -200,7 +178,7 @@ TEST(CuddDd, OperatorTest) { TEST(CuddDd, AbstractionTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9); + manager->addMetaVariable("x", 1, 9); storm::dd::Dd dd1; storm::dd::Dd dd2; storm::dd::Dd dd3; @@ -246,7 +224,7 @@ TEST(CuddDd, AbstractionTest) { TEST(CuddDd, SwapTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9); + manager->addMetaVariable("x", 1, 9); manager->addMetaVariable("z", 2, 8); storm::dd::Dd dd1; storm::dd::Dd dd2; @@ -259,7 +237,7 @@ TEST(CuddDd, SwapTest) { TEST(CuddDd, MultiplyMatrixTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9); + manager->addMetaVariable("x", 1, 9); storm::dd::Dd dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'")); storm::dd::Dd dd2 = manager->getRange("x'");