From 38833e308f19df4e800788b13157e1bb56ed613d Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Feb 2014 22:43:19 +0100 Subject: [PATCH] Started to add row-grouping to sparse matrix class. Former-commit-id: 39e37030952d004f233883925bab9495e6dfc918 --- src/adapters/ExplicitModelAdapter.h | 5 +- src/modelchecker/prctl/AbstractModelChecker.h | 2 +- .../prctl/SparseMdpPrctlModelChecker.h | 8 +- src/models/AbstractModel.h | 2 +- src/models/AbstractNondeterministicModel.h | 41 +----- src/storage/SparseMatrix.cpp | 122 ++++++++++++++---- src/storage/SparseMatrix.h | 70 +++++++++- test/functional/solver/GurobiLpSolverTest.cpp | 2 +- test/functional/storage/SparseMatrixTest.cpp | 5 +- 9 files changed, 175 insertions(+), 82 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 9d3f5f74f..9001803ba 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -542,6 +542,7 @@ namespace storm { } else { // If the model is nondeterministic, we add all choices individually. nondeterministicChoiceIndices.push_back(currentRow); + transitionMatrixBuilder.addRowGroup(); // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { @@ -631,8 +632,8 @@ namespace storm { bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC; // Build the transition and reward matrices. - storm::storage::SparseMatrixBuilder transitionMatrixBuilder; - storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0); + storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0); std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first); modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 4658c779f..5862fe9c9 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -177,7 +177,7 @@ public: result = this->checkNoBoundOperator(noBoundFormula); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : model.getInitialStates()) { + for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index f7fe02731..7aa5ae581 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -284,23 +284,23 @@ namespace storm { */ static std::pair, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr> nondeterministicLinearEquationSolver, bool qualitative) { size_t numberOfStates = phiStates.size(); - + // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; if (minimize) { statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + } else { statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); } storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - + // Create resulting vector. std::vector result(numberOfStates); @@ -317,7 +317,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, Type(0.5)); } else { // In this case we have have to compute the probabilities. - + // First, we can eliminate the rows and columns from the original transition probability matrix for states // whose probabilities are already known. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(maybeStates, nondeterministicChoiceIndices); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index b9fda426d..3a77907a6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -194,7 +194,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return A sparse matrix that represents the backward transitions of this model. */ storm::storage::SparseMatrix getBackwardTransitions() const { - return this->transitionMatrix.transpose(); + return this->transitionMatrix.transpose(true); } /*! diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 8de7ef8c4..fdc005b41 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -123,46 +123,7 @@ namespace storm { * @return A sparse matrix that represents the backward transitions of this model. */ storm::storage::SparseMatrix getBackwardTransitions() const { - uint_fast64_t numberOfStates = this->getNumberOfStates(); - uint_fast64_t numberOfTransitions = this->getTransitionMatrix().getEntryCount(); - - std::vector rowIndications(numberOfStates + 1); - std::vector> columnsAndValues(numberOfTransitions, std::make_pair(0, storm::utility::constantZero())); - - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::const_rows rows = this->getRows(i); - for (auto const& transition : rows) { - if (transition.second > 0) { - ++rowIndications[transition.first + 1]; - } - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates + 1; ++i) { - rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; - } - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = rowIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::const_rows rows = this->getRows(i); - for (auto const& transition : rows) { - if (transition.second > 0) { - columnsAndValues[nextIndices[transition.first]] = std::make_pair(i, transition.second); - ++nextIndices[transition.first]; - } - } - } - - storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnsAndValues)); - - return backwardTransitionMatrix; + return this->getTransitionMatrix().transpose(true); } /*! diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 1ba121550..a2a5e6b82 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -18,7 +18,7 @@ namespace storm { namespace storage { template - SparseMatrixBuilder::SparseMatrixBuilder(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), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrixBuilder::SparseMatrixBuilder(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries, bool hasCustomRowGrouping, uint_fast64_t 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(); } @@ -68,6 +68,14 @@ namespace storm { rowIndications.push_back(currentEntryCount); } } + + if (!hasCustomRowGrouping) { + for (uint_fast64_t i = lastRow + 1; i <= row; ++i) { + rowGroupIndices.push_back(row); + ++currentRowGroup; + } + } + lastRow = row; } @@ -86,14 +94,26 @@ namespace storm { } } ++currentEntryCount; - } template - SparseMatrix SparseMatrixBuilder::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount) { + void SparseMatrixBuilder::addRowGroup() { + if (!hasCustomRowGrouping) { + throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::addRowGroup: matrix was not created to have a custom row grouping."; + } + if (rowGroupCountSet) { + rowGroupIndices[currentRowGroup] = lastRow + 1; + ++currentRowGroup; + } else { + rowGroupIndices.push_back(lastRow + 1); + } + } + + template + SparseMatrix SparseMatrixBuilder::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount, uint_fast64_t 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::finalize: expected " << entryCount << " entries, but got " << currentEntryCount << " instead."; + 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) { @@ -122,20 +142,47 @@ namespace storm { } entryCount = currentEntryCount; + + if (hasCustomRowGrouping && rowGroupCountSet) { + rowGroupIndices[rowGroupCount] = rowCount; + } else { + if (!hasCustomRowGrouping) { + for (uint_fast64_t i = currentRowGroup; i < rowCount; ++i) { + rowGroupIndices.push_back(i + 1); + } + } else { + overriddenRowGroupCount = std::max(overriddenRowGroupCount, currentRowGroup + 1); + for (uint_fast64_t i = currentRowGroup; i < overriddenRowGroupCount; ++i) { + rowGroupIndices.push_back(rowCount); + } + } + } } - return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues)); + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } template void SparseMatrixBuilder::prepareInternalStorage() { - // Only allocate the memory if the dimensions of the matrix are already known. + // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known. if (storagePreallocated) { columnsAndValues = std::vector>(entryCount, std::make_pair(0, storm::utility::constantZero())); rowIndications = std::vector(rowCount + 1, 0); } else { rowIndications.push_back(0); } + + // 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); + } else { + if (hasCustomRowGrouping) { + // Nothing to do in this case + } else { + rowGroupIndices.push_back(0); + } + } } template @@ -169,17 +216,17 @@ namespace storm { } template - SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications() { + SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications) { + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)) { + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix other.rowCount = 0; other.columnCount = 0; @@ -187,12 +234,12 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { // Intentionally left empty. } @@ -206,6 +253,7 @@ namespace storm { columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; + rowGroupIndices = other.rowGroupIndices; } return *this; @@ -221,6 +269,7 @@ namespace storm { columnsAndValues = std::move(other.columnsAndValues); rowIndications = std::move(other.rowIndications); + rowGroupIndices = std::move(other.rowGroupIndices); } return *this; @@ -236,6 +285,7 @@ namespace storm { equalityResult &= rowCount == other.rowCount; equalityResult &= columnCount == other.columnCount; + equalityResult &= rowGroupIndices == other.rowGroupIndices; // For the actual contents, we need to do a little bit more work, because we want to ignore elements that // are set to zero, please they may be represented implicitly in the other matrix. @@ -278,6 +328,11 @@ namespace storm { return entryCount; } + template + uint_fast64_t SparseMatrix::getRowGroupCount() const { + return rowGroupIndices.size() - 1; + } + template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { for (auto row : rows) { @@ -502,19 +557,19 @@ namespace storm { } template - SparseMatrix SparseMatrix::transpose() const { - uint_fast64_t rowCount = this->columnCount; - uint_fast64_t columnCount = this->rowCount; - uint_fast64_t entryCount = this->entryCount; + SparseMatrix SparseMatrix::transpose(bool joinGroups) const { + uint_fast64_t rowCount = this->getColumnCount(); + uint_fast64_t columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); + uint_fast64_t entryCount = this->getEntryCount(); std::vector rowIndications(rowCount + 1); std::vector> columnsAndValues(entryCount); // First, we need to count how many entries each column has. - for (uint_fast64_t row = 0; row < this->rowCount; ++row) { - for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { - if (it->second > 0) { - ++rowIndications[it->first + 1]; + for (uint_fast64_t group = 0; group < columnCount; ++group) { + for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { + if (transition.second != storm::utility::constantZero()) { + ++rowIndications[transition.first + 1]; } } } @@ -530,20 +585,25 @@ namespace storm { std::vector nextIndices = rowIndications; // Now we are ready to actually fill in the values of the transposed matrix. - for (uint_fast64_t row = 0; row < this->rowCount; ++row) { - for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { - if (it->second > 0) { - columnsAndValues[nextIndices[it->first]] = std::make_pair(row, it->second); - nextIndices[it->first]++; + for (uint_fast64_t group = 0; group < columnCount; ++group) { + for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { + if (transition.second != storm::utility::constantZero()) { + columnsAndValues[nextIndices[transition.first]] = std::make_pair(group, transition.second); + nextIndices[transition.first]++; } } } - storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues)); + std::vector rowGroupIndices(rowCount + 1); + for (uint_fast64_t i = 0; i <= rowCount; ++i) { + rowGroupIndices[i] = i; + } + storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return transposedMatrix; } - + template void SparseMatrix::convertToEquationSystem() { invertDiagonal(); @@ -738,6 +798,16 @@ namespace storm { return getRows(row, row); } + template + typename SparseMatrix::const_rows SparseMatrix::getRowGroup(uint_fast64_t rowGroup) const { + return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1); + } + + template + typename SparseMatrix::rows SparseMatrix::getRowGroup(uint_fast64_t rowGroup) { + return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1); + } + template typename SparseMatrix::const_iterator SparseMatrix::begin(uint_fast64_t row) const { return this->columnsAndValues.begin() + this->rowIndications[row]; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index dbb80745b..f066744de 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -39,8 +39,12 @@ 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 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(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0); + SparseMatrixBuilder(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0, bool hasCustomRowGrouping = false, uint_fast64_t rowGroups = 0); /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, @@ -57,6 +61,12 @@ namespace storm { */ void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value); + /*! + * Adds a new row group to the matrix. Note that this needs to be called before any entries in the new row + * group are added. + */ + void addRowGroup(); + /* * 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. @@ -70,8 +80,13 @@ namespace storm { * *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. + * @param overriddenRowGroupCount If this is set to a value that is greater than the current number of row + * groups, this will cause the method to set the number of row groups to the given value. Note that this will + * *not* override the row group count that has been given upon construction (if any), but will only take + * effect if the matrix has been created without the number of row groups given. By construction, the row + * groups added this way will be empty. */ - SparseMatrix build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0); + SparseMatrix build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0, uint_fast64_t overriddenRowGroupCount = 0); private: /*! @@ -96,6 +111,17 @@ namespace storm { // The number of entries in the matrix. uint_fast64_t entryCount; + // 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; + + // The number of row groups in the matrix. + uint_fast64_t rowGroupCount; + + std::vector rowGroupIndices; + // Stores whether the storage of the matrix was preallocated or not. bool storagePreallocated; @@ -119,6 +145,10 @@ namespace storm { // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an // entry into a matrix. uint_fast64_t lastColumn; + + // Stores the currently active row group. This is used for correctly constructing the row grouping of the + // matrix. + uint_fast64_t currentRowGroup; }; /*! @@ -250,8 +280,9 @@ namespace storm { * @param columnCount The number of columns of the matrix. * @param rowIndications The row indications vector of the matrix to be constructed. * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. + * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues); + SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); /*! * Constructs a sparse matrix by moving the given contents. @@ -259,8 +290,9 @@ namespace storm { * @param columnCount The number of columns of the matrix. * @param rowIndications The row indications vector of the matrix to be constructed. * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. + * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues); + SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); /*! * Assigns the contents of the given matrix to the current one by deep-copying its contents. @@ -305,6 +337,13 @@ namespace storm { */ uint_fast64_t getEntryCount() const; + /*! + * Returns the number of row groups in the matrix. + * + * @return The number of row groups in the matrix. + */ + uint_fast64_t getRowGroupCount() const; + /*! * This function makes the given rows absorbing. * @@ -411,9 +450,11 @@ namespace storm { /*! * Transposes the matrix. * + * @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows. + * * @return A sparse matrix that represents the transpose of this matrix. */ - storm::storage::SparseMatrix transpose() const; + storm::storage::SparseMatrix transpose(bool joinGroups = false) const; /*! * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). @@ -498,6 +539,22 @@ namespace storm { */ rows getRow(uint_fast64_t row); + /*! + * Returns an object representing the given row group. + * + * @param rowGroup The row group to get. + * @return An object representing the given row group. + */ + const_rows getRowGroup(uint_fast64_t rowGroup) const; + + /*! + * Returns an object representing the given row group. + * + * @param rowGroup The row group to get. + * @return An object representing the given row group. + */ + rows getRowGroup(uint_fast64_t rowGroup); + /*! * Retrieves an iterator that points to the beginning of the given row. * @@ -596,6 +653,9 @@ namespace storm { // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; + + // A vector indicating the row groups of the matrix. + std::vector rowGroupIndices; }; } // namespace storage diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index b8c7fe885..508c0882c 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -14,7 +14,7 @@ TEST(GurobiLpSolver, LPOptimizeMax) { ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2)); uint_fast64_t zIndex; ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1)); - + ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5)); ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5)); diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index ecde843cb..88aa2cf3c 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -154,11 +154,12 @@ TEST(SparseMatrix, CreationWithMovingContents) { columnsAndValues.emplace_back(1, 0.7); columnsAndValues.emplace_back(3, 0.2); - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues)); - storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues); + ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3})); + storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}); ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); + ASSERT_EQ(3, matrix.getRowGroupCount()); } TEST(SparseMatrix, CopyConstruct) {