All tests working with (partially) new sparse matrix implementation/interface.

Former-commit-id: 0272dd3524

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);

src/models/AbstractModel.h

@@ -160,8 +160,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
             }
             
             // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
-            storm::storage::SparseMatrix<T> dependencyGraph(numberOfStates);
-            dependencyGraph.initialize();
+            storm::storage::SparseMatrix<T> 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<AbstractModel<T>> {
                 // Now, we determine the blocks which are reachable (in one step) from the current block.
                 storm::storage::VectorSet<uint_fast64_t> allTargetBlocks;
                 for (auto state : block) {
-                    typename storm::storage::SparseMatrix<T>::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<AbstractModel<T>> {
                 
                 // 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<T>());
                 }
             }
             

src/parser/DeterministicSparseTransitionParser.cpp

@@ -201,7 +201,7 @@ storm::storage::SparseMatrix<double> 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<double> resultMatrix(maxStateId + 1, nonZeroEntryCount);
+	storm::storage::SparseMatrix<double> resultMatrix(maxStateId + 1, maxStateId + 1, nonZeroEntryCount);
 
 	int_fast64_t row, lastRow = -1, col;
 	double val;

src/storage/SparseMatrix.cpp

@@ -101,25 +101,21 @@ namespace storm {
         }
         
         template<typename T>
-        SparseMatrix<T>::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<T>::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<typename T>
-        SparseMatrix<T>::SparseMatrix(uint_fast64_t size, uint_fast64_t entries) : SparseMatrix(size, size, entries) {
-            // Intentionally left empty.
-        }
-        
+                
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T> 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<T>::SparseMatrix(SparseMatrix<T> 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<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T>&& 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<T>::SparseMatrix(SparseMatrix<T>&& 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<T>& SparseMatrix<T>::operator=(SparseMatrix<T> 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<T>& SparseMatrix<T>::operator=(SparseMatrix<T>&& 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<typename T>
-        void SparseMatrix<T>::finalize() {
+        void SparseMatrix<T>::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<typename T>
-        bool SparseMatrix<T>::isSubmatrixOf(SparseMatrix<T> const& matrix) const {
+        bool SparseMatrix<T>::isSubmatrixOf(SparseMatrix<T> 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<T>(entryCount, storm::utility::constantZero<T>());
                 columnIndications = std::vector<uint_fast64_t>(entryCount, 0);
                 rowIndications = std::vector<uint_fast64_t>(rowCount + 1, 0);
+            } else {
+                rowIndications.push_back(0);
             }
         }
         

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;
             

test/performance/graph/GraphTest.cpp

@@ -101,7 +101,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     storm::storage::SparseMatrix<double> 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;
 }