diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index eba51a557..aa3b7c675 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -326,12 +326,16 @@ namespace storm { } 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); + if (filename.empty()) { + this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()}); + } else { + FILE* filePointer = fopen(filename.c_str() , "w"); + this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()}, nullptr, nullptr, filePointer); + fclose(filePointer); + } } - ADD Dd::getCuddAdd() { + ADD& Dd::getCuddAdd() { return this->cuddAdd; } @@ -350,5 +354,11 @@ namespace storm { std::shared_ptr> Dd::getDdManager() const { return this->ddManager; } + + std::ostream & operator<<(std::ostream& out, const Dd& dd) { + dd.exportToDot(); + return out; + } + } } \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 1f8339fe6..0255ae58e 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/storage/dd/Dd.h" #include "src/utility/OsDetection.h" @@ -345,7 +346,7 @@ namespace storm { * * @param filename The name of the file to which the DD is to be exported. */ - void exportToDot(std::string const& filename) const; + void exportToDot(std::string const& filename = "") const; /*! * Retrieves the manager that is responsible for this DD. @@ -354,13 +355,14 @@ namespace storm { */ std::shared_ptr> getDdManager() const; + friend std::ostream & operator<<(std::ostream& out, const Dd& dd); private: /*! - * Retrieves the CUDD ADD object associated with this DD. + * Retrieves a reference to the CUDD ADD object associated with this DD. * - * @return The CUDD ADD object assoicated with this DD. + * @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 dd6ce4f4f..4b96e685a 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -4,8 +4,6 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h" -#include - namespace storm { namespace dd { DdManager::DdManager() : metaVariableMap(), cuddManager() { @@ -25,7 +23,17 @@ namespace storm { } Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { - std::vector> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); + // Check whether the meta variable exists. + if (!this->hasMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'."; + } + + // Check whether the value is legal for this meta variable. + if (value < this->getMetaVariable(metaVariableName).getLow() || value > this->getMetaVariable(metaVariableName).getHigh()) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'."; + } + + std::vector> const& ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); Dd result; if (value & (1ull << (ddVariables.size() - 1))) { @@ -120,7 +128,7 @@ namespace storm { auto const& nameVariablePair = metaVariableMap.find(metaVariableName); if (!this->hasMetaVariable(metaVariableName)) { - throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name."; + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'."; } return nameVariablePair->second; diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index a92dbc929..fb6856c75 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, MetaVariableTest) { +TEST(CuddDdManager, AddMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); @@ -60,6 +60,29 @@ TEST(CuddDdManager, MetaVariableTest) { 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) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + + storm::dd::Dd encoding; + 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(CuddDdMetaVariable, AccessorTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(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()); @@ -69,3 +92,13 @@ TEST(CuddDdManager, MetaVariableTest) { EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables()); } +//TEST(CuddDd, OperatorTest) { +// std::shared_ptr> manager(new storm::dd::DdManager()); +// +// ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); +// EXPECT_EQ(manager->getZero(), manager->getZero()); +// EXPECT_NE(manager->getZero(), manager->getOne()); +// +// storm::dd::Dd add; +// +//}