From f767cfe844a5010675add7c6c8ae95ca830e68c0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 5 Sep 2014 15:56:54 +0200
Subject: [PATCH 1/3] Started to modify the matrix builder to be a bit smarter
about preallocation.
Former-commit-id: 50be5c8af109981ed4ba11d34c7de57584b9c7f9
---
src/storage/SparseMatrix.cpp | 150 +++++++++++------------------------
src/storage/SparseMatrix.h | 2 +
2 files changed, 47 insertions(+), 105 deletions(-)
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index f4ad62d66..363f5413a 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -59,31 +59,11 @@ namespace storm {
template<typename ValueType>
void SparseMatrixBuilder<ValueType>::addNextValue(index_type row, index_type column, ValueType const& value) {
- // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat
- // differently.
- if (storagePreallocated) {
- // Check whether the given row and column positions are valid and throw error otherwise.
- if (row >= rowCount || column >= columnCount) {
- throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::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 SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds row " << row << " in matrix with " << rowCount << " rows.";
- }
- }
- if (columnCountSet) {
- if (column >= columnCount) {
- throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds column " << column << " in matrix with " << columnCount << " columns.";
- }
- }
- }
-
// Check that we did not move backwards wrt. the row.
if (row < lastRow) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.";
}
-
+
// Check that we did not move backwards wrt. to column.
if (row == lastRow && column < lastColumn) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row.";
@@ -91,23 +71,14 @@ namespace storm {
// If we switched to another row, we have to adjust the missing entries in the row indices vector.
if (row != lastRow) {
- if (storagePreallocated) {
- // If the storage was preallocated, we can access the elements in the vectors with the subscript
- // operator.
- for (index_type i = lastRow + 1; i <= row; ++i) {
- rowIndications[i] = currentEntryCount;
- }
- } else {
- // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
- for (index_type i = lastRow + 1; i <= row; ++i) {
- rowIndications.push_back(currentEntryCount);
- }
+ // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
+ for (index_type i = lastRow + 1; i <= row; ++i) {
+ rowIndications.push_back(currentEntryCount);
}
if (!hasCustomRowGrouping) {
for (index_type i = lastRow + 1; i <= row; ++i) {
rowGroupIndices.push_back(i);
- ++currentRowGroup;
}
}
@@ -121,12 +92,8 @@ namespace storm {
columnsAndValues[currentEntryCount] = std::make_pair(column, value);
} else {
columnsAndValues.emplace_back(column, value);
- if (!columnCountSet) {
- columnCount = std::max(columnCount, column + 1);
- }
- if (!rowCountSet) {
- rowCount = row + 1;
- }
+ columnCount = std::max(columnCount, column + 1);
+ rowCount = row + 1;
}
++currentEntryCount;
}
@@ -138,88 +105,61 @@ namespace storm {
} else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) {
throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size.";
}
- if (rowGroupCountSet) {
- rowGroupIndices[currentRowGroup] = startingRow;
- ++currentRowGroup;
- } else {
- rowGroupIndices.push_back(startingRow);
- }
+
+ rowGroupIndices.push_back(startingRow);
}
template<typename ValueType>
SparseMatrix<ValueType> SparseMatrixBuilder<ValueType>::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) {
- // Check whether it's safe to finalize the matrix and throw error otherwise.
- if (storagePreallocated && currentEntryCount != entryCount) {
- throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::build: expected " << entryCount << " entries, but got " << currentEntryCount << " instead.";
- } else {
- // Fill in the missing entries in the row indices array, as there may be empty rows at the end.
- if (storagePreallocated) {
- for (index_type i = lastRow + 1; i < rowCount; ++i) {
- rowIndications[i] = currentEntryCount;
- }
- } else {
- if (!rowCountSet) {
- rowCount = std::max(overriddenRowCount, rowCount);
- }
- for (index_type i = lastRow + 1; i < rowCount; ++i) {
- rowIndications.push_back(currentEntryCount);
- }
- }
-
- // We put a sentinel element at the last position of the row indices array. This eases iteration work,
- // 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] = currentEntryCount;
- } else {
+ // If the current row count was overridden, we may need to add empty rows.
+ if (overriddenRowCount > rowCount) {
+ for (index_type i = lastRow + 1; i < rowCount; ++i) {
rowIndications.push_back(currentEntryCount);
- if (!columnCountSet) {
- columnCount = std::max(columnCount, overriddenColumnCount);
- }
}
-
- entryCount = currentEntryCount;
-
- if (hasCustomRowGrouping && rowGroupCountSet) {
- rowGroupIndices[rowGroupCount] = rowCount;
- } else {
- if (!hasCustomRowGrouping) {
- for (index_type i = currentRowGroup; i < rowCount; ++i) {
- rowGroupIndices.push_back(i + 1);
- }
- } else {
- overriddenRowGroupCount = std::max(overriddenRowGroupCount, currentRowGroup + 1);
- for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) {
- rowGroupIndices.push_back(rowCount);
- }
+ }
+
+ // We put a sentinel element at the last position of the row indices array. This eases iteration work,
+ // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for
+ // the first and last row.
+ rowIndications.push_back(currentEntryCount);
+
+ // Check whether the column count has been overridden.
+ if (overriddenColumnCount > columnCount) {
+ columnCount = overriddenColumnCount;
+ }
+
+ entryCount = currentEntryCount;
+
+ // Check whether row groups are missing some entries.
+ if (!hasCustomRowGrouping) {
+ for (index_type i = currentRowGroup; i < rowCount; ++i) {
+ rowGroupIndices.push_back(i + 1);
+ }
+ } else {
+ // Check if the row group count has been overridden.
+ if (overriddenRowGroupCount > currentRowGroup + 1) {
+ for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) {
+ rowGroupIndices.push_back(rowCount);
}
}
}
-
+
return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
}
template<typename ValueType>
void SparseMatrixBuilder<ValueType>::prepareInternalStorage() {
- // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known.
- if (storagePreallocated) {
- columnsAndValues = std::vector<MatrixEntry<index_type, ValueType>>(entryCount, MatrixEntry<index_type, ValueType>(0, storm::utility::constantZero<ValueType>()));
- rowIndications = std::vector<index_type>(rowCount + 1, 0);
- } else {
- rowIndications.push_back(0);
+ if (rowCount > 0) {
+ rowIndications.reserve(rowCount + 1);
}
-
- // Only allocate the memory for the row grouping of the matrix contents if the number of groups is already
- // known.
- if (hasCustomRowGrouping && rowGroupCountSet) {
- rowGroupIndices = std::vector<index_type>(rowGroupCount + 1, 0);
- } else {
- if (hasCustomRowGrouping) {
- // Nothing to do in this case
- } else {
- rowGroupIndices.push_back(0);
- }
+ if (entryCount > 0) {
+ columnsAndValues.reserve(entryCount);
+ }
+ if (rowGroupCount > 0) {
+ rowGroupIndices.reserve(rowGroupCount + 1);
}
+ rowIndications.push_back(0);
+ rowGroupIndices.push_back(0);
}
template<typename ValueType>
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index e87f215af..a5964d220 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -122,6 +122,8 @@ namespace storm {
/*!
* Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries.
+ * The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are
+ * added, this will possibly lead to a reallocation.
*
* @param rows The number of rows of the resulting matrix.
* @param columns The number of columns of the resulting matrix.
From fff4e61fc3f7690a0284f932a4e783f0ad7857ea Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 6 Sep 2014 00:55:03 +0200
Subject: [PATCH 2/3] Changed interface of matrix builder slightly to be able
to also not force the resulting matrix to certain dimensions, but merely to
reserve the desired space.
Former-commit-id: e36d05398e30811a4061a4453ac2cdec27967525
---
src/adapters/ExplicitModelAdapter.h | 4 +-
.../SparseMarkovAutomatonCslModelChecker.h | 2 +-
src/models/MarkovAutomaton.h | 2 +-
src/models/Mdp.h | 2 +-
...NondeterministicSparseTransitionParser.cpp | 6 +-
src/storage/SparseMatrix.cpp | 109 +++++++++---------
src/storage/SparseMatrix.h | 45 ++++----
...ndeterministicLinearEquationSolverTest.cpp | 4 +-
...ndeterministicLinearEquationSolverTest.cpp | 4 +-
test/functional/storage/SparseMatrixTest.cpp | 10 +-
10 files changed, 96 insertions(+), 92 deletions(-)
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 25804b58a..211a3aecf 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -662,8 +662,8 @@ namespace storm {
bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;
// Build the transition and reward matrices.
- storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
- storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0);
+ storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
+ storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
// Finalize the resulting matrices.
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index 56b36ac37..493f286bf 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -347,7 +347,7 @@ namespace storm {
// Finally, we are ready to create the SSP matrix and right-hand side of the SSP.
std::vector<ValueType> b;
- typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size());
+ typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size());
// If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications).
uint_fast64_t currentChoice = 0;
diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h
index 8f5825d6d..ef73c26ea 100644
--- a/src/models/MarkovAutomaton.h
+++ b/src/models/MarkovAutomaton.h
@@ -126,7 +126,7 @@ namespace storm {
//uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates;
// Create the matrix for the new transition relation and the corresponding nondeterministic choice vector.
- storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates());
+ storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder(0, 0, 0, false, true, this->getNumberOfStates());
// Now copy over all choices that need to be kept.
uint_fast64_t currentChoice = 0;
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 5dd1c8c0e..0a0c2e06e 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -139,7 +139,7 @@ public:
std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
- storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true);
+ storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true);
std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling;
// Check for each choice of each state, whether the choice labels are fully contained in the given label set.
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 32557dbb2..5923f7778 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -92,9 +92,9 @@ namespace storm {
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
if(!isRewardFile) {
- matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1);
+ matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, firstPass.highestStateIndex + 1);
} else {
- matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount());
+ matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, modelInformation.getRowGroupCount());
}
// Initialize variables for the parsing run.
@@ -179,7 +179,7 @@ namespace storm {
// Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
if(isRewardFile) {
// We already have rowGroup 0.
- for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size(); index++) {
+ for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) {
matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]);
}
} else {
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 363f5413a..0b5846acc 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -9,6 +9,7 @@
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/ExceptionMacros.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
@@ -53,8 +54,18 @@ namespace storm {
}
template<typename ValueType>
- SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool hasCustomRowGrouping, index_type rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) {
- this->prepareInternalStorage();
+ SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) {
+ // Prepare the internal storage.
+ if (initialRowCountSet > 0) {
+ rowIndications.reserve(initialRowCount + 1);
+ }
+ if (initialEntryCountSet > 0) {
+ columnsAndValues.reserve(initialEntryCount);
+ }
+ if (initialRowGroupCountSet > 0) {
+ rowGroupIndices.reserve(initialRowGroupCount + 1);
+ }
+ rowIndications.push_back(0);
}
template<typename ValueType>
@@ -76,46 +87,44 @@ namespace storm {
rowIndications.push_back(currentEntryCount);
}
- if (!hasCustomRowGrouping) {
- for (index_type i = lastRow + 1; i <= row; ++i) {
- rowGroupIndices.push_back(i);
- }
- }
-
lastRow = row;
}
lastColumn = column;
// Finally, set the element and increase the current size.
- if (storagePreallocated) {
- columnsAndValues[currentEntryCount] = std::make_pair(column, value);
- } else {
- columnsAndValues.emplace_back(column, value);
- columnCount = std::max(columnCount, column + 1);
- rowCount = row + 1;
- }
+ columnsAndValues.emplace_back(column, value);
+ highestColumn = std::max(highestColumn, column);
++currentEntryCount;
+
+ // In case we did not expect this value, we throw an exception.
+ if (forceInitialDimensions) {
+ LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
+ LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << ".");
+ LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << ".");
+ }
}
template<typename ValueType>
void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
- if (!hasCustomRowGrouping) {
- throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping.";
- } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) {
- throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size.";
- }
-
+ LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
+ LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
rowGroupIndices.push_back(startingRow);
+ ++currentRowGroup;
}
template<typename ValueType>
SparseMatrix<ValueType> SparseMatrixBuilder<ValueType>::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) {
+ uint_fast64_t rowCount = lastRow + 1;
+ if (initialRowCountSet && forceInitialDimensions) {
+ LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
+ rowCount = std::max(rowCount, initialRowCount);
+ }
+ rowCount = std::max(rowCount, overriddenRowCount);
+
// If the current row count was overridden, we may need to add empty rows.
- if (overriddenRowCount > rowCount) {
- for (index_type i = lastRow + 1; i < rowCount; ++i) {
- rowIndications.push_back(currentEntryCount);
- }
+ for (index_type i = lastRow + 1; i < rowCount; ++i) {
+ rowIndications.push_back(currentEntryCount);
}
// We put a sentinel element at the last position of the row indices array. This eases iteration work,
@@ -123,45 +132,39 @@ namespace storm {
// the first and last row.
rowIndications.push_back(currentEntryCount);
- // Check whether the column count has been overridden.
- if (overriddenColumnCount > columnCount) {
- columnCount = overriddenColumnCount;
+ uint_fast64_t columnCount = highestColumn + 1;
+ if (initialColumnCountSet && forceInitialDimensions) {
+ LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
+ columnCount = std::max(columnCount, initialColumnCount);
+ }
+ columnCount = std::max(columnCount, overriddenColumnCount);
+
+ uint_fast64_t entryCount = currentEntryCount;
+ if (initialEntryCountSet && forceInitialDimensions) {
+ LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << ".");
}
-
- entryCount = currentEntryCount;
// Check whether row groups are missing some entries.
if (!hasCustomRowGrouping) {
- for (index_type i = currentRowGroup; i < rowCount; ++i) {
- rowGroupIndices.push_back(i + 1);
+ for (index_type i = 0; i <= rowCount; ++i) {
+ rowGroupIndices.push_back(i);
}
} else {
- // Check if the row group count has been overridden.
- if (overriddenRowGroupCount > currentRowGroup + 1) {
- for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) {
- rowGroupIndices.push_back(rowCount);
- }
+ uint_fast64_t rowGroupCount = currentRowGroup;
+ if (initialRowGroupCountSet && forceInitialDimensions) {
+ LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
+ rowGroupCount = std::max(rowGroupCount, initialRowGroupCount);
+ }
+ rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
+
+ for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) {
+ rowGroupIndices.push_back(rowCount);
}
}
return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
}
- template<typename ValueType>
- void SparseMatrixBuilder<ValueType>::prepareInternalStorage() {
- if (rowCount > 0) {
- rowIndications.reserve(rowCount + 1);
- }
- if (entryCount > 0) {
- columnsAndValues.reserve(entryCount);
- }
- if (rowGroupCount > 0) {
- rowGroupIndices.reserve(rowGroupCount + 1);
- }
- rowIndications.push_back(0);
- rowGroupIndices.push_back(0);
- }
-
template<typename ValueType>
SparseMatrix<ValueType>::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) {
// Intentionally left empty.
@@ -471,7 +474,7 @@ namespace storm {
}
// Create and initialize resulting matrix.
- SparseMatrixBuilder<ValueType> matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true);
+ SparseMatrixBuilder<ValueType> matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true, true);
// Create a temporary vector that stores for each index whose bit is set to true the number of bits that
// were set before that particular index.
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index a5964d220..b419ca841 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -128,12 +128,14 @@ namespace storm {
* @param rows The number of rows of the resulting matrix.
* @param columns The number of columns of the resulting matrix.
* @param entries The number of entries of the resulting matrix.
+ * @param forceDimensions If this flag is set, the matrix is expected to have exactly the given number of
+ * rows, columns and entries for all of these entities that are set to a nonzero value.
* @param hasCustomRowGrouping A flag indicating whether the builder is used to create a non-canonical
* grouping of rows for this matrix.
* @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix
* has a custom row grouping.
*/
- SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool hasCustomRowGrouping = false, index_type rowGroups = 0);
+ SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0);
/*!
* Sets the matrix entry at the given row and column to the given value. After all entries have been added,
@@ -180,42 +182,38 @@ namespace storm {
SparseMatrix<value_type> build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0);
private:
- /*!
- * Prepares the internal storage of the builder. This relies on the number of entries and the number of rows
- * being set correctly. They may, however, be zero, in which case the insertion of elements in the builder
- * will cause occasional reallocations.
- */
- void prepareInternalStorage();
-
- // A flag indicating whether the number of rows was set upon construction.
- bool rowCountSet;
+ // A flag indicating whether a row count was set upon construction.
+ bool initialRowCountSet;
- // The number of rows of the matrix.
- index_type rowCount;
+ // The row count that was initially set (if any).
+ index_type initialRowCount;
- // A flag indicating whether the number of columns was set upon construction.
- bool columnCountSet;
+ // A flag indicating whether a column count was set upon construction.
+ bool initialColumnCountSet;
+
+ // The column count that was initially set (if any).
+ index_type initialColumnCount;
- // The number of columns of the matrix.
- index_type columnCount;
+ // A flag indicating whether an entry count was set upon construction.
+ bool initialEntryCountSet;
// The number of entries in the matrix.
- index_type entryCount;
+ index_type initialEntryCount;
+
+ // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix.
+ bool forceInitialDimensions;
// A flag indicating whether the builder is to construct a custom row grouping for the matrix.
bool hasCustomRowGrouping;
// A flag indicating whether the number of row groups was set upon construction.
- bool rowGroupCountSet;
+ bool initialRowGroupCountSet;
// The number of row groups in the matrix.
- index_type rowGroupCount;
+ index_type initialRowGroupCount;
std::vector<index_type> rowGroupIndices;
- // Stores whether the storage of the matrix was preallocated or not.
- bool storagePreallocated;
-
// The storage for the columns and values of all entries in the matrix.
std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
@@ -237,6 +235,9 @@ namespace storm {
// entry into a matrix.
index_type lastColumn;
+ // Stores the highest column at which an entry was inserted into the matrix.
+ index_type highestColumn;
+
// Stores the currently active row group. This is used for correctly constructing the row grouping of the
// matrix.
index_type currentRowGroup;
diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
index ae9542bbb..04f0b4036 100644
--- a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
+++ b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
@@ -5,7 +5,7 @@
#include "src/settings/Settings.h"
TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
- storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+ storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
@@ -24,7 +24,7 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
}
TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
- storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+ storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
index 0ccdafd84..4c7f76337 100644
--- a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
+++ b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
@@ -5,7 +5,7 @@
#include "src/settings/Settings.h"
TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
- storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+ storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
@@ -24,7 +24,7 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
}
TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
- storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+ storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp
index 52746ef97..b677f6f3c 100644
--- a/test/functional/storage/SparseMatrixTest.cpp
+++ b/test/functional/storage/SparseMatrixTest.cpp
@@ -221,7 +221,7 @@ TEST(SparseMatrix, MakeAbsorbing) {
}
TEST(SparseMatrix, MakeRowGroupAbsorbing) {
- storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true);
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true, true);
ASSERT_NO_THROW(matrixBuilder.newRowGroup(0));
ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0));
ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2));
@@ -242,7 +242,7 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) {
ASSERT_NO_THROW(matrix.makeRowGroupsAbsorbing(absorbingRowGroups));
- storm::storage::SparseMatrixBuilder<double> matrixBuilder2(0, 0, 0, true);
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder2(0, 0, 0, false, true);
ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0));
ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0));
ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2));
@@ -283,7 +283,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
std::vector<double> constrainedRowSum = matrix.getConstrainedRowSumVector(storm::storage::BitVector(5, true), columnConstraint);
ASSERT_TRUE(constrainedRowSum == std::vector<double>({1.0, 0.7, 0, 0, 0.5}));
- storm::storage::SparseMatrixBuilder<double> matrixBuilder2(5, 4, 9, true);
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder2(5, 4, 9, true, true);
ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0));
ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0));
ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2));
@@ -312,7 +312,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
}
TEST(SparseMatrix, Submatrix) {
- storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true);
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true, true);
ASSERT_NO_THROW(matrixBuilder.newRowGroup(0));
ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0));
ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2));
@@ -342,7 +342,7 @@ TEST(SparseMatrix, Submatrix) {
ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false));
storm::storage::SparseMatrix<double> matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false);
- storm::storage::SparseMatrixBuilder<double> matrixBuilder3(3, 2, 3, true);
+ storm::storage::SparseMatrixBuilder<double> matrixBuilder3(3, 2, 3, true, true);
ASSERT_NO_THROW(matrixBuilder3.newRowGroup(0));
ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 0, 0.5));
ASSERT_NO_THROW(matrixBuilder3.newRowGroup(2));
From 2c231a794d490d483250c455b990165ac91f20e8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 10 Sep 2014 20:15:50 +0200
Subject: [PATCH 3/3] SCC decomposition now correctly ignores zero-entries in
the matrix.
Former-commit-id: 351c0ac6ade95a54f533a1318532632ac7266d78
---
src/storage/StronglyConnectedComponentDecomposition.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp
index 46990e7eb..784e99ab0 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.cpp
+++ b/src/storage/StronglyConnectedComponentDecomposition.cpp
@@ -161,7 +161,7 @@ namespace storm {
bool recursionStepIn = false;
for (; successorIt != model.getRows(currentState).end(); ++successorIt) {
- if (subsystem.get(successorIt->getColumn())) {
+ if (subsystem.get(successorIt->getColumn()) && successorIt->getValue() != storm::utility::constantZero<ValueType>()) {
if (currentState == successorIt->getColumn()) {
statesWithSelfLoop.set(currentState);
}