From cf5c04065eec918b2cfa1b2d5442236801ed5c82 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 28 Mar 2014 19:24:24 +0100
Subject: [PATCH] Added streaming functionality to DD. More tests, more
bugfixes.
Former-commit-id: 3c3078fbdcd9414ab52894c26a36806730f75a4f
---
src/storage/dd/CuddDd.cpp | 18 ++++++++++---
src/storage/dd/CuddDd.h | 10 +++++---
src/storage/dd/CuddDdManager.cpp | 16 +++++++++---
test/functional/storage/CuddDdTest.cpp | 35 +++++++++++++++++++++++++-
4 files changed, 66 insertions(+), 13 deletions(-)
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<CUDD>::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<CUDD>::getCuddAdd() {
+ ADD& Dd<CUDD>::getCuddAdd() {
return this->cuddAdd;
}
@@ -350,5 +354,11 @@ namespace storm {
std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const {
return this->ddManager;
}
+
+ std::ostream & operator<<(std::ostream& out, const Dd<CUDD>& 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 <unordered_map>
#include <set>
#include <memory>
+#include <iostream>
#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<DdManager<CUDD>> getDdManager() const;
+ friend std::ostream & operator<<(std::ostream& out, const Dd<CUDD>& 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 <iostream>
-
namespace storm {
namespace dd {
DdManager<CUDD>::DdManager() : metaVariableMap(), cuddManager() {
@@ -25,7 +23,17 @@ namespace storm {
}
Dd<CUDD> DdManager<CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
- std::vector<Dd<CUDD>> 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<Dd<CUDD>> const& ddVariables = this->getMetaVariable(metaVariableName).getDdVariables();
Dd<CUDD> 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<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
@@ -60,6 +60,29 @@ TEST(CuddDdManager, MetaVariableTest) {
ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
+}
+
+TEST(CuddDdManager, EncodingTest) {
+ std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+
+ ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
+
+ storm::dd::Dd<storm::dd::CUDD> 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<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+
+ ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
+ EXPECT_EQ(1, manager->getNumberOfMetaVariables());
+ ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
storm::dd::DdMetaVariable<storm::dd::CUDD> 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<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+//
+// ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
+// EXPECT_EQ(manager->getZero(), manager->getZero());
+// EXPECT_NE(manager->getZero(), manager->getOne());
+//
+// storm::dd::Dd<storm::dd::CUDD> add;
+//
+//}