From 8587f68eb17e3f74c7bd77fc83c455b1b8a9e735 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 17 Jun 2014 23:33:55 +0200 Subject: [PATCH] Fixed toMatrix conversion using ODDs. The next step is to generate non-deterministic matrices, i.e., matrices with row groups. Former-commit-id: e4a9c5f0ed3f2eac5712f7a8e8d825641ca17c35 --- src/storage/dd/CuddDd.cpp | 55 +++++++++++++++++++++----- src/storage/dd/CuddDd.h | 13 +++++- test/functional/storage/CuddDdTest.cpp | 3 +- 3 files changed, 59 insertions(+), 12 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 3de67e8d0..4eb5eff5a 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -489,12 +489,46 @@ namespace storm { 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(); + // Prepare the vectors that represent the matrix. + std::vector rowIndications(rowOdd.getTotalOffset() + 1); + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent + // it from actually generating the entries in the entry vector. + toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + // Create a trivial row grouping. + std::vector trivialRowGroupIndices(rowIndications.size()); + uint_fast64_t i = 0; + for (auto& entry : trivialRowGroupIndices) { + entry = i; + ++i; + } + + // Construct matrix and return result. + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); } - 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 { + void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, 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, bool generateValues) 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. @@ -504,7 +538,10 @@ namespace storm { // 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)); + if (generateValues) { + columnsAndValues[rowIndications[currentRowOffset]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + } + ++rowIndications[currentRowOffset]; } else { DdNode const* elseElse; DdNode const* elseThen; @@ -535,13 +572,13 @@ namespace storm { } // Visit else-else. - toMatrixRec(elseElse, builder, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices); + toMatrixRec(elseElse, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); // Visit else-then. - toMatrixRec(elseThen, builder, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices); + toMatrixRec(elseThen, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); // Visit then-else. - toMatrixRec(thenElse, builder, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices); + toMatrixRec(thenElse, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); // Visit then-then. - toMatrixRec(thenThen, builder, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices); + toMatrixRec(thenThen, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); } } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 6a25b8c78..045f547a0 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -636,7 +636,13 @@ namespace storm { * 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 rowIndications A vector indicating at which position in the columnsAndValues vector the entries + * of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the + * vector will be increased by the number of entries in the row. This can be used to count the number + * of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries + * need to be restored afterwards. + * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful + * completion. * @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. @@ -646,8 +652,11 @@ namespace storm { * @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. + * @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which + * only works if the offsets given in rowIndications are already correct. If they need to be computed first, + * this flag needs to be false. */ - 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; + void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, 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, bool generateValues = true) 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 0c75253b5..98a528b3d 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -396,9 +396,10 @@ TEST(CuddDd, OddTest) { } dd = manager->getIdentity("x").equals(manager->getIdentity("x'")) * manager->getRange("x"); + dd += manager->getEncoding("x", 1) * manager->getRange("x'") + manager->getEncoding("x'", 1) * 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()); + EXPECT_EQ(25, matrix.getNonzeroEntryCount()); } \ No newline at end of file