From 97fb2f97502a54cdb7ec3bcba2565659af037ee7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Dec 2013 20:28:33 +0100 Subject: [PATCH] All tests working with (partially) new sparse matrix implementation/interface. Former-commit-id: 0272dd35245b19963ce799febc15dfd0ca39c504 --- src/adapters/ExplicitModelAdapter.h | 2 +- src/models/AbstractModel.h | 10 ++-- .../DeterministicSparseTransitionParser.cpp | 2 +- src/storage/SparseMatrix.cpp | 60 ++++++++++++------- src/storage/SparseMatrix.h | 32 ++++++---- test/performance/graph/GraphTest.cpp | 8 +-- 6 files changed, 70 insertions(+), 44 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 270928779..a859ea441 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -637,7 +637,7 @@ namespace storm { // Finalize the resulting matrices. modelComponents.transitionMatrix.finalize(); - modelComponents.transitionRewardMatrix.finalize(); + modelComponents.transitionRewardMatrix.finalize(modelComponents.transitionMatrix.getRowCount()); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index f8ab02fd8..d222350c6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -160,8 +160,7 @@ class AbstractModel: public std::enable_shared_from_this> { } // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. - storm::storage::SparseMatrix dependencyGraph(numberOfStates); - dependencyGraph.initialize(); + storm::storage::SparseMatrix dependencyGraph(numberOfStates, numberOfStates); for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { // Get the next block. @@ -170,9 +169,8 @@ class AbstractModel: public std::enable_shared_from_this> { // Now, we determine the blocks which are reachable (in one step) from the current block. storm::storage::VectorSet allTargetBlocks; for (auto state : block) { - typename storm::storage::SparseMatrix::Rows rows = this->getRows(state); - for (auto& transition : rows) { - uint_fast64_t targetBlock = stateToBlockMap[transition.column()]; + for (auto const& transitionEntry : this->getRows(state)) { + uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.column()]; // We only need to consider transitions that are actually leaving the SCC. if (targetBlock != currentBlockIndex) { @@ -183,7 +181,7 @@ class AbstractModel: public std::enable_shared_from_this> { // Now we can just enumerate all the target SCCs and insert the corresponding transitions. for (auto targetBlock : allTargetBlocks) { - dependencyGraph.insertNextValue(currentBlockIndex, targetBlock, true); + dependencyGraph.addNextValue(currentBlockIndex, targetBlock, storm::utility::constantOne()); } } diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index f824dcd28..e436ebbce 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -201,7 +201,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st * The number of non-zero elements is computed by firstPass(). */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - storm::storage::SparseMatrix resultMatrix(maxStateId + 1, nonZeroEntryCount); + storm::storage::SparseMatrix resultMatrix(maxStateId + 1, maxStateId + 1, nonZeroEntryCount); int_fast64_t row, lastRow = -1, col; double val; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index c1c54a643..c4e773d34 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -101,25 +101,21 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCount(rows), columnCount(columns), entryCount(entries), valueStorage(), columnIndications(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { - storagePreallocated = rows != 0 && columns != 0 && entries != 0; + SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), storagePreallocated(rows != 0 && columns != 0 && entries != 0), valueStorage(), columnIndications(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { prepareInternalStorage(); } - - template - SparseMatrix::SparseMatrix(uint_fast64_t size, uint_fast64_t entries) : SparseMatrix(size, size, entries) { - // Intentionally left empty. - } - + template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), valueStorage(other.valueStorage), columnIndications(other.columnIndications), rowIndications(other.rowIndications), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), valueStorage(other.valueStorage), columnIndications(other.columnIndications), rowIndications(other.rowIndications), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), valueStorage(std::move(other.valueStorage)), columnIndications(std::move(other.columnIndications)), rowIndications(std::move(other.rowIndications)), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), valueStorage(std::move(other.valueStorage)), columnIndications(std::move(other.columnIndications)), rowIndications(std::move(other.rowIndications)), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { // Now update the source matrix + other.rowCountSet = false; other.rowCount = 0; + other.columnCountSet = false; other.columnCount = 0; other.entryCount = 0; other.storagePreallocated = false; @@ -143,7 +139,9 @@ namespace storm { SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. if (this != &other) { + rowCountSet = other.rowCountSet; rowCount = other.rowCount; + columnCountSet = other.columnCountSet; columnCount = other.columnCount; entryCount = other.entryCount; @@ -164,7 +162,9 @@ namespace storm { SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { // Only perform assignment if source and target are not the same. if (this != &other) { + rowCountSet = other.rowCountSet; rowCount = other.rowCount; + columnCountSet = other.columnCountSet; columnCount = other.columnCount; entryCount = other.entryCount; @@ -187,9 +187,17 @@ namespace storm { // differently. if (storagePreallocated) { // Check whether the given row and column positions are valid and throw error otherwise. - if (row > rowCount || column > columnCount) { + if (row >= rowCount || column >= columnCount) { throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::addNextValue: adding entry at out-of-bounds position (" << row << ", " << column << ") in matrix of size (" << rowCount << ", " << columnCount << ")."; } + } else if (rowCountSet) { + if (row >= rowCount) { + throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::addNextValue: adding entry at out-of-bounds row " << row << " in matrix with " << rowCount << " rows."; + } + } else if (columnCountSet) { + if (column >= columnCount) { + throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::addNextValue: adding entry at out-of-bounds column " << column << " in matrix with " << columnCount << " columns."; + } } // Check that we did not move backwards wrt. the row. @@ -225,18 +233,21 @@ namespace storm { if (storagePreallocated) { valueStorage[currentEntryCount] = value; columnIndications[currentEntryCount] = column; - ++currentEntryCount; } else { valueStorage.push_back(value); columnIndications.push_back(column); - columnCount = column + 1; - rowCount = row + 1; - ++currentEntryCount; + if (!columnCountSet) { + columnCount = column + 1; + } + if (!rowCountSet) { + rowCount = row + 1; + } } + ++currentEntryCount; } template - void SparseMatrix::finalize() { + void SparseMatrix::finalize(uint_fast64_t overriddenRowCount, uint_fast64_t overridenColumnCount) { // Check whether it's safe to finalize the matrix and throw error otherwise. if (internalStatus == INITIALIZED) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::finalize: finalizing an initialized matrix is forbidden."; @@ -249,6 +260,9 @@ namespace storm { rowIndications[i] = currentEntryCount; } } else { + if (!rowCountSet) { + rowCount = std::max(overriddenRowCount, rowCount); + } for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); } @@ -258,11 +272,15 @@ namespace storm { // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. if (storagePreallocated) { - rowIndications[rowCount] = entryCount; + rowIndications[rowCount] = currentEntryCount; } else { - rowIndications.push_back(entryCount); + rowIndications.push_back(currentEntryCount); + if (!columnCountSet) { + columnCount = std::max(columnCount, overridenColumnCount); + } } + entryCount = currentEntryCount; internalStatus = INITIALIZED; } } @@ -383,7 +401,7 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrix result(constraint.getNumberOfSetBits(), subEntries); + SparseMatrix result(constraint.getNumberOfSetBits(), constraint.getNumberOfSetBits(), subEntries); // Create a temporary vecotr that stores for each index whose bit is set to true the number of bits that // were set before that particular index. @@ -834,7 +852,7 @@ namespace storm { } template - bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { + bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; @@ -914,6 +932,8 @@ namespace storm { valueStorage = std::vector(entryCount, storm::utility::constantZero()); columnIndications = std::vector(entryCount, 0); rowIndications = std::vector(rowCount + 1, 0); + } else { + rowIndications.push_back(0); } } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 7b7a908b3..680cee636 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -245,16 +245,8 @@ namespace storm { * @param columns The number of columns of the matrix. * @param entries The number of entries of the matrix. */ - SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries); - - /*! - * Constructs a square sparse matrix object with the given number rows and entries. - * - * @param size The number of rows and columns of the matrix. - * @param entries The number of entries of the matrix. - */ - SparseMatrix(uint_fast64_t size = 0, uint_fast64_t entries = 0); - + SparseMatrix(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0); + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * @@ -316,13 +308,23 @@ namespace storm { * @param column The column in which the matrix entry is to be set. * @param value The value that is to be set at the specified row and column. */ - void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value); + void addNextValue(uint_fast64_t row, uint_fast64_t column,T const& value); /* * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix * may now be used. This must be called after all entries have been added to the matrix via addNextValue. + * + * @param overriddenRowCount If this is set to a value that is greater than the current number of rows, + * this will cause the finalize method to add empty rows at the end of the matrix until the given row count + * has been matched. Note that this will *not* override the row count that has been given upon construction + * (if any), but will only take effect if the matrix has been created without the number of rows given. + * @param overriddenColumnCount If this is set to a value that is greater than the current number of columns, + * this will cause the finalize method to set the number of columns to the given value. Note that this will + * *not* override the column count that has been given upon construction (if any), but will only take effect + * if the matrix has been created without the number of columns given. By construction, the matrix will have + * no entries in the columns that have been added this way. */ - void finalize(); + void finalize(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0); /*! * Returns the number of rows of the matrix. @@ -633,9 +635,15 @@ namespace storm { */ void prepareInternalStorage(); + // A flag indicating whether the number of rows was set upon construction. + bool rowCountSet; + // The number of rows of the matrix. uint_fast64_t rowCount; + // A flag indicating whether the number of columns was set upon construction. + bool columnCountSet; + // The number of columns of the matrix. uint_fast64_t columnCount; diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 0f1459e52..8bbb44518 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -101,7 +101,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { storm::storage::SparseMatrix sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition))); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253ull); + ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1371253ull); dtmc = nullptr; @@ -118,7 +118,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDependencyGraph = std::move(dtmc2->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367ull); + ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1535367ull); dtmc2 = nullptr; @@ -135,7 +135,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 489918ull); + ASSERT_EQ(sccDependencyGraph.getEntryCount(), 489918ull); mdp = nullptr; @@ -152,7 +152,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7888ull); + ASSERT_EQ(sccDependencyGraph.getEntryCount(), 7888ull); mdp2 = nullptr; }