diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index a7d9df2d1..3de67e8d0 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -119,138 +119,141 @@ namespace storm {
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.Equals(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.NotEquals(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.LessThan(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.LessThanOrEqual(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.GreaterThan(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result.cuddAdd = result.cuddAdd.GreaterThanOrEqual(other.getCuddAdd());
- return result;
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
-
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
-
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames);
}
- void Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) {
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
for (auto const& metaVariableName : metaVariableNames) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
}
- this->getContainedMetaVariableNames().erase(metaVariableName);
+ newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
- this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
- void Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) {
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
for (auto const& metaVariableName : metaVariableNames) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
}
- this->getContainedMetaVariableNames().erase(metaVariableName);
+ newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
- this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
- void Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
for (auto const& metaVariableName : metaVariableNames) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
}
- this->getContainedMetaVariableNames().erase(metaVariableName);
+ newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
- this->cuddAdd = this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
- void Dd<DdType::CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) {
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
for (auto const& metaVariableName : metaVariableNames) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
}
- this->getContainedMetaVariableNames().erase(metaVariableName);
+ newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
- this->cuddAdd = this->cuddAdd.MinAbstract(cubeDd.getCuddAdd());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
- void Dd<DdType::CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) {
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
for (auto const& metaVariableName : metaVariableNames) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
}
- this->getContainedMetaVariableNames().erase(metaVariableName);
+ newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
- this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> const& other, double precision, bool relative) const {
@@ -410,7 +413,7 @@ namespace storm {
}
Dd<DdType::CUDD> value = *this * valueEncoding;
- value.sumAbstract(this->getContainedMetaVariableNames());
+ value = value.sumAbstract(this->getContainedMetaVariableNames());
return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
}
@@ -430,18 +433,19 @@ namespace storm {
return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
}
- std::vector<double> Dd<DdType::CUDD>::toDoubleVector() const {
- return this->toDoubleVector(Odd<DdType::CUDD>(*this));
+ std::vector<double> Dd<DdType::CUDD>::toVector() const {
+ return this->toVector(Odd<DdType::CUDD>(*this));
}
- std::vector<double> Dd<DdType::CUDD>::toDoubleVector(Odd<DdType::CUDD> const& odd) const {
+ std::vector<double> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& odd) const {
std::vector<double> result(odd.getTotalOffset());
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
- toDoubleVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices);
+ toVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices);
return result;
}
- void Dd<DdType::CUDD>::toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const {
+ void Dd<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const {
+ // For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
return;
}
@@ -452,12 +456,92 @@ namespace storm {
} else if (ddVariableIndices[currentLevel] < dd->index) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
- toDoubleVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
- toDoubleVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
+ toVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
+ toVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
} else {
// Otherwise, we simply recursively call the function for both (different) cases.
- toDoubleVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
- toDoubleVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
+ toVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
+ toVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
+ }
+ }
+
+ storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
+ std::set<std::string> rowVariables;
+ std::set<std::string> columnVariables;
+ std::vector<uint_fast64_t> ddRowVariableIndices;
+ std::vector<uint_fast64_t> ddColumnVariableIndices;
+
+ for (auto const& variableName : this->getContainedMetaVariableNames()) {
+ DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variableName);
+ if (variableName.size() > 0 && variableName.back() == '\'') {
+ columnVariables.insert(variableName);
+ for (auto const& ddVariable : metaVariable.getDdVariables()) {
+ ddColumnVariableIndices.push_back(ddVariable.getIndex());
+ }
+ } else {
+ rowVariables.insert(variableName);
+ for (auto const& ddVariable : metaVariable.getDdVariables()) {
+ ddRowVariableIndices.push_back(ddVariable.getIndex());
+ }
+ }
+ }
+
+ Odd<DdType::CUDD> columnOdd(this->existsAbstract(rowVariables));
+ Odd<DdType::CUDD> rowOdd(this->existsAbstract(columnVariables));
+
+ storm::storage::SparseMatrixBuilder<double> builder;
+ toMatrixRec(this->getCuddAdd().getNode(), builder, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices);
+ return builder.build();
+ }
+
+ void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, storm::storage::SparseMatrixBuilder<double>& builder, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const {
+ // FIXME: this method currently assumes a strict interleaved order, which does not seem necessary.
+
+ // For the empty DD, we do not need to add any entries.
+ if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
+ return;
+ }
+
+ // If we are at the maximal level, the value to be set is stored as a constant in the DD.
+ if (currentRowLevel + currentColumnLevel == maxLevel) {
+ builder.addNextValue(currentRowOffset, currentColumnOffset, Cudd_V(dd));
+ } else {
+ DdNode const* elseElse;
+ DdNode const* elseThen;
+ DdNode const* thenElse;
+ DdNode const* thenThen;
+
+ if (ddColumnVariableIndices[currentColumnLevel] < dd->index) {
+ elseElse = elseThen = thenElse = thenThen = dd;
+ } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) {
+ elseElse = thenElse = Cudd_E(dd);
+ elseThen = thenThen = Cudd_T(dd);
+ } else {
+ DdNode const* elseNode = Cudd_E(dd);
+ if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) {
+ elseElse = elseThen = elseNode;
+ } else {
+ elseElse = Cudd_E(elseNode);
+ elseThen = Cudd_T(elseNode);
+ }
+
+ DdNode const* thenNode = Cudd_T(dd);
+ if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) {
+ thenElse = thenThen = thenNode;
+ } else {
+ thenElse = Cudd_E(thenNode);
+ thenThen = Cudd_T(thenNode);
+ }
+ }
+
+ // Visit else-else.
+ toMatrixRec(elseElse, builder, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices);
+ // Visit else-then.
+ toMatrixRec(elseThen, builder, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices);
+ // Visit then-else.
+ toMatrixRec(thenElse, builder, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices);
+ // Visit then-then.
+ toMatrixRec(thenThen, builder, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices);
}
}
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index a7951cfb3..6a25b8c78 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -8,6 +8,7 @@
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/CuddDdForwardIterator.h"
+#include "src/storage/SparseMatrix.h"
#include "src/storage/expressions/Expression.h"
#include "src/utility/OsDetection.h"
@@ -234,35 +235,35 @@ namespace storm {
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
- void existsAbstract(std::set<std::string> const& metaVariableNames);
+ Dd<DdType::CUDD> existsAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Universally abstracts from the given meta variables.
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
- void universalAbstract(std::set<std::string> const& metaVariableNames);
+ Dd<DdType::CUDD> universalAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Sum-abstracts from the given meta variables.
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
- void sumAbstract(std::set<std::string> const& metaVariableNames);
+ Dd<DdType::CUDD> sumAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Min-abstracts from the given meta variables.
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
- void minAbstract(std::set<std::string> const& metaVariableNames);
+ Dd<DdType::CUDD> minAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Max-abstracts from the given meta variables.
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
- void maxAbstract(std::set<std::string> const& metaVariableNames);
+ Dd<DdType::CUDD> maxAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Checks whether the current and the given DD represent the same function modulo some given precision.
@@ -461,7 +462,13 @@ namespace storm {
*
* @return The double vector that is represented by this DD.
*/
- std::vector<double> toDoubleVector() const;
+ std::vector<double> toVector() const;
+
+ /*!
+ * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the
+ * row, whereas all primed variables are assumed to encode the column.
+ */
+ storm::storage::SparseMatrix<double> toMatrix() const;
/*!
* Converts the DD to a double vector using the given ODD (that needs to be constructed for the DD).
@@ -469,7 +476,7 @@ namespace storm {
* @param odd The ODD for the DD.
* @return The double vector that is represented by this DD.
*/
- std::vector<double> toDoubleVector(Odd<DdType::CUDD> const& odd) const;
+ std::vector<double> toVector(Odd<DdType::CUDD> const& odd) const;
/*!
* Retrieves whether the given meta variable is contained in the DD.
@@ -623,7 +630,24 @@ namespace storm {
* @param currentOffset The current offset.
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
*/
- void toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const;
+ void toVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const;
+
+ /*!
+ * Helper function to convert the DD into a (sparse) matrix.
+ *
+ * @param dd The DD to convert.
+ * @param builder A matrix builder that can be used to insert the nonzero entries.
+ * @param rowOdd The ODD used for the row translation.
+ * @param columnOdd The ODD used for the column translation.
+ * @param currentRowLevel The currently considered row level in the DD.
+ * @param currentColumnLevel The currently considered row level in the DD.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param currentRowOffset The current row offset.
+ * @param currentColumnOffset The current row offset.
+ * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
+ * @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered.
+ */
+ void toMatrixRec(DdNode const* dd, storm::storage::SparseMatrixBuilder<double>& builder, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const;
/*!
* Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support,
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index 5a6376e9f..0c75253b5 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -163,12 +163,12 @@ TEST(CuddDd, OperatorTest) {
dd4 = dd3.minimum(dd1);
dd4 *= manager->getEncoding("x", 2);
- dd4.sumAbstract({"x"});
+ dd4 = dd4.sumAbstract({"x"});
EXPECT_EQ(2, dd4.getValue());
dd4 = dd3.maximum(dd1);
dd4 *= manager->getEncoding("x", 2);
- dd4.sumAbstract({"x"});
+ dd4 = dd4.sumAbstract({"x"});
EXPECT_EQ(5, dd4.getValue());
dd1 = manager->getConstant(0.01);
@@ -188,36 +188,36 @@ TEST(CuddDd, AbstractionTest) {
dd2 = manager->getConstant(5);
dd3 = dd1.equals(dd2);
EXPECT_EQ(1, dd3.getNonZeroCount());
- ASSERT_THROW(dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(dd3.existsAbstract({"x"}));
+ ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
EXPECT_EQ(1, dd3.getNonZeroCount());
- ASSERT_THROW(dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(dd3.existsAbstract({"x"}));
+ ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"}));
EXPECT_TRUE(dd3 == manager->getZero());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
- ASSERT_THROW(dd3.sumAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(dd3.sumAbstract({"x"}));
+ ASSERT_THROW(dd3 = dd3.sumAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(dd3 = dd3.sumAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
- ASSERT_THROW(dd3.minAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(dd3.minAbstract({"x"}));
+ ASSERT_THROW(dd3 = dd3.minAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(dd3 = dd3.minAbstract({"x"}));
EXPECT_EQ(0, dd3.getNonZeroCount());
EXPECT_EQ(0, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
- ASSERT_THROW(dd3.maxAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(dd3.maxAbstract({"x"}));
+ ASSERT_THROW(dd3 = dd3.maxAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(dd3 = dd3.maxAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax());
}
@@ -389,9 +389,16 @@ TEST(CuddDd, OddTest) {
EXPECT_EQ(12, odd.getNodeCount());
std::vector<double> ddAsVector;
- ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector());
+ ASSERT_NO_THROW(ddAsVector = dd.toVector());
EXPECT_EQ(9, ddAsVector.size());
for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
EXPECT_TRUE(i+1 == ddAsVector[i]);
}
+
+ dd = manager->getIdentity("x").equals(manager->getIdentity("x'")) * manager->getRange("x");
+ storm::storage::SparseMatrix<double> matrix;
+ ASSERT_NO_THROW(matrix = dd.toMatrix());
+ EXPECT_EQ(9, matrix.getRowCount());
+ EXPECT_EQ(9, matrix.getColumnCount());
+ EXPECT_EQ(9, matrix.getNonzeroEntryCount());
}
\ No newline at end of file