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 transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0); - storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); + storm::storage::SparseMatrixBuilder 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 b; - typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size()); + typename storm::storage::SparseMatrixBuilder 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 newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates()); + storm::storage::SparseMatrixBuilder 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> const& choiceLabeling = this->getChoiceLabeling(); - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true); std::vector> 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 matrixBuilder; if(!isRewardFile) { - matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1); + matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, firstPass.highestStateIndex + 1); } else { - matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount()); + matrixBuilder = storm::storage::SparseMatrixBuilder(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 f4ad62d66..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,37 +54,27 @@ namespace storm { } template - SparseMatrixBuilder::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::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 void SparseMatrixBuilder::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,24 +82,9 @@ 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); - } - } - - if (!hasCustomRowGrouping) { - for (index_type i = lastRow + 1; i <= row; ++i) { - rowGroupIndices.push_back(i); - ++currentRowGroup; - } + // 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); } lastRow = row; @@ -117,109 +93,76 @@ namespace storm { 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); - if (!columnCountSet) { - columnCount = std::max(columnCount, column + 1); - } - if (!rowCountSet) { - 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 void SparseMatrixBuilder::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."; - } - if (rowGroupCountSet) { - rowGroupIndices[currentRowGroup] = startingRow; - ++currentRowGroup; - } else { - rowGroupIndices.push_back(startingRow); - } + 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 SparseMatrix SparseMatrixBuilder::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 { - 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); - } - } - } + 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); - return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); - } - - template - void SparseMatrixBuilder::prepareInternalStorage() { - // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known. - if (storagePreallocated) { - columnsAndValues = std::vector>(entryCount, MatrixEntry(0, storm::utility::constantZero())); - rowIndications = std::vector(rowCount + 1, 0); - } else { - rowIndications.push_back(0); + // If the current row count was overridden, we may need to add empty rows. + for (index_type i = lastRow + 1; i < rowCount; ++i) { + rowIndications.push_back(currentEntryCount); } - // 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(rowGroupCount + 1, 0); + // 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); + + 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 << "."); + } + + // Check whether row groups are missing some entries. + if (!hasCustomRowGrouping) { + for (index_type i = 0; i <= rowCount; ++i) { + rowGroupIndices.push_back(i); + } } else { - if (hasCustomRowGrouping) { - // Nothing to do in this case - } else { - rowGroupIndices.push_back(0); + 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(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } template @@ -531,7 +474,7 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true); + SparseMatrixBuilder 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 e87f215af..b419ca841 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -122,16 +122,20 @@ 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. * @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, @@ -178,42 +182,38 @@ namespace storm { SparseMatrix 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 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> columnsAndValues; @@ -235,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/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()) { if (currentState == successorIt->getColumn()) { statesWithSelfLoop.set(currentState); } 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 builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder 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 builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder 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 builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder 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 builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder 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 matrixBuilder(5, 4, 9, true); + storm::storage::SparseMatrixBuilder 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 matrixBuilder2(0, 0, 0, true); + storm::storage::SparseMatrixBuilder 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 constrainedRowSum = matrix.getConstrainedRowSumVector(storm::storage::BitVector(5, true), columnConstraint); ASSERT_TRUE(constrainedRowSum == std::vector({1.0, 0.7, 0, 0, 0.5})); - storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 9, true); + storm::storage::SparseMatrixBuilder 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 matrixBuilder(5, 4, 9, true); + storm::storage::SparseMatrixBuilder 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 matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false)); storm::storage::SparseMatrix matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false); - storm::storage::SparseMatrixBuilder matrixBuilder3(3, 2, 3, true); + storm::storage::SparseMatrixBuilder 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));