From 236e7fa2908b29aeae48f30999f387314792e2ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 15 Jun 2014 22:45:49 +0200 Subject: [PATCH] Another step towards generating explicit data structures from DDs using ODDs. Former-commit-id: 5b7e3e8680d385c60fb68c1024e960171688272b --- src/storage/dd/CuddDd.cpp | 174 ++++++++++++++++++------- src/storage/dd/CuddDd.h | 40 ++++-- test/functional/storage/CuddDdTest.cpp | 33 +++-- 3 files changed, 181 insertions(+), 66 deletions(-) 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 Dd::equals(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.Equals(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariableNames); } Dd Dd::notEquals(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.NotEquals(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariableNames); } Dd Dd::less(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.LessThan(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariableNames); } Dd Dd::lessOrEqual(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.LessThanOrEqual(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariableNames); } Dd Dd::greater(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.GreaterThan(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariableNames); } Dd Dd::greaterOrEqual(Dd const& other) const { - Dd result(*this); - result.cuddAdd = result.cuddAdd.GreaterThanOrEqual(other.getCuddAdd()); - return result; + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariableNames); } Dd Dd::minimum(Dd const& other) const { std::set metaVariableNames(this->getContainedMetaVariableNames()); metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames); } Dd Dd::maximum(Dd const& other) const { std::set metaVariableNames(this->getContainedMetaVariableNames()); metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames); } - void Dd::existsAbstract(std::set const& metaVariableNames) { + Dd Dd::existsAbstract(std::set const& metaVariableNames) const { Dd cubeDd(this->getDdManager()->getOne()); + std::set 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 const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } - this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()); + return Dd(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - void Dd::universalAbstract(std::set const& metaVariableNames) { + Dd Dd::universalAbstract(std::set const& metaVariableNames) const { Dd cubeDd(this->getDdManager()->getOne()); + std::set 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 const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } - this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()); + return Dd(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - void Dd::sumAbstract(std::set const& metaVariableNames) { + Dd Dd::sumAbstract(std::set const& metaVariableNames) const { Dd cubeDd(this->getDdManager()->getOne()); + std::set 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 const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } - this->cuddAdd = this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()); + return Dd(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - void Dd::minAbstract(std::set const& metaVariableNames) { + Dd Dd::minAbstract(std::set const& metaVariableNames) const { Dd cubeDd(this->getDdManager()->getOne()); + std::set 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 const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } - this->cuddAdd = this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()); + return Dd(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables); } - void Dd::maxAbstract(std::set const& metaVariableNames) { + Dd Dd::maxAbstract(std::set const& metaVariableNames) const { Dd cubeDd(this->getDdManager()->getOne()); + std::set 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 const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } - this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()); + return Dd(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables); } bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { @@ -410,7 +413,7 @@ namespace storm { } Dd value = *this * valueEncoding; - value.sumAbstract(this->getContainedMetaVariableNames()); + value = value.sumAbstract(this->getContainedMetaVariableNames()); return static_cast(Cudd_V(value.getCuddAdd().getNode())); } @@ -430,18 +433,19 @@ namespace storm { return static_cast(this->getCuddAdd().NodeReadIndex()); } - std::vector Dd::toDoubleVector() const { - return this->toDoubleVector(Odd(*this)); + std::vector Dd::toVector() const { + return this->toVector(Odd(*this)); } - std::vector Dd::toDoubleVector(Odd const& odd) const { + std::vector Dd::toVector(Odd const& odd) const { std::vector result(odd.getTotalOffset()); std::vector 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::toDoubleVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const { + void Dd::toVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector 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 Dd::toMatrix() const { + std::set rowVariables; + std::set columnVariables; + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + + for (auto const& variableName : this->getContainedMetaVariableNames()) { + DdMetaVariable 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 columnOdd(this->existsAbstract(rowVariables)); + Odd rowOdd(this->existsAbstract(columnVariables)); + + storm::storage::SparseMatrixBuilder builder; + toMatrixRec(this->getCuddAdd().getNode(), builder, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices); + return builder.build(); + } + + void Dd::toMatrixRec(DdNode const* dd, storm::storage::SparseMatrixBuilder& builder, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector 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 const& metaVariableNames); + Dd existsAbstract(std::set 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 const& metaVariableNames); + Dd universalAbstract(std::set 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 const& metaVariableNames); + Dd sumAbstract(std::set 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 const& metaVariableNames); + Dd minAbstract(std::set 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 const& metaVariableNames); + Dd maxAbstract(std::set 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 toDoubleVector() const; + std::vector 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 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 toDoubleVector(Odd const& odd) const; + std::vector toVector(Odd 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& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const; + void toVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector 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& builder, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector 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 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 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