diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index f915a4842..689d45ba2 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -459,6 +459,7 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::cout << this->getModel().getTransitionMatrix() << std::endl; storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseDtmcPrctlModelChecker::computeLongRunAverageHelper(this->getModel(), probabilityMatrix, subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory))); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index ae76c832f..8a13a147c 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -356,13 +356,29 @@ namespace storm { // Now transpose the matrix. This internally removes all explicit zeros from the matrix that were. // introduced when subtracting the identity matrix. bsccEquationSystem = bsccEquationSystem.transpose(); + + std::cout << bsccEquationSystem << std::endl; + + // Add a row to the matrix that expresses that the sum over all entries needs to be one. + storm::storage::SparseMatrixBuilder builder(std::move(bsccEquationSystem)); + typename storm::storage::SparseMatrixBuilder::index_type row = builder.getLastRow(); + for (uint_fast64_t i = 0; i <= row; ++i) { + builder.addNextValue(row + 1, i, 1); + } + bsccEquationSystem = builder.build(); + std::cout << bsccEquationSystem << std::endl; std::vector bsccEquationSystemRightSide(bsccEquationSystem.getColumnCount(), zero); + bsccEquationSystemRightSide.back() = one; std::vector bsccEquationSystemSolution(bsccEquationSystem.getColumnCount(), one); { std::unique_ptr> solver = linearEquationSolverFactory.create(bsccEquationSystem); solver->solveEquationSystem(bsccEquationSystemSolution, bsccEquationSystemRightSide); } + + for (auto const& elem : bsccEquationSystemSolution) { + std::cout << "sol " << elem << std::endl; + } // Calculate LRA Value for each BSCC from steady state distribution in BSCCs. // We have to scale the results, as the probabilities for each BSCC have to sum up to one, which they don't diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 58a842cd3..2c1b1a582 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -82,6 +82,20 @@ namespace storm { rowIndications.push_back(0); } + template + SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(matrix.nontrivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount()), currentRowGroup() { + + // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again. + if (hasCustomRowGrouping) { + rowGroupIndices = std::move(matrix.rowGroupIndices); + rowGroupIndices.pop_back(); + currentRowGroup = rowGroupIndices.size() - 1; + } + + // Likewise, we need to 'open' the row indications again. + rowIndications.pop_back(); + } + template void SparseMatrixBuilder::addNextValue(index_type row, index_type column, ValueType const& value) { // Check that we did not move backwards wrt. the row. @@ -176,7 +190,17 @@ namespace storm { } } - return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping); + } + + template + typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastRow() const { + return lastRow; + } + + template + typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastColumn() const { + return lastColumn; } template @@ -220,17 +244,17 @@ namespace storm { } template - SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { + SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), nontrivialRowGrouping(false), rowGroupIndices() { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix other.rowCount = 0; other.columnCount = 0; @@ -238,12 +262,12 @@ namespace storm { } template - SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { + SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) { this->updateNonzeroEntryCount(); } template - SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { + SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(std::move(rowGroupIndices)) { this->updateNonzeroEntryCount(); } @@ -259,6 +283,7 @@ namespace storm { columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; rowGroupIndices = other.rowGroupIndices; + nontrivialRowGrouping = other.nontrivialRowGrouping; } return *this; @@ -276,6 +301,7 @@ namespace storm { columnsAndValues = std::move(other.columnsAndValues); rowIndications = std::move(other.rowIndications); rowGroupIndices = std::move(other.rowGroupIndices); + nontrivialRowGrouping = other.nontrivialRowGrouping; } return *this; @@ -506,7 +532,7 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true, true); + SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true, this->hasNontrivialRowGrouping()); // 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. @@ -534,7 +560,9 @@ namespace storm { // Copy over selected entries. index_type rowCount = 0; for (auto index : rowGroupConstraint) { - matrixBuilder.newRowGroup(rowCount); + if (this->hasNontrivialRowGrouping()) { + matrixBuilder.newRowGroup(rowCount); + } for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { bool insertedDiagonalElement = false; @@ -659,7 +687,7 @@ namespace storm { rowGroupIndices[i] = i; } - storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), false); return transposedMatrix; } @@ -906,6 +934,11 @@ namespace storm { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } + template + bool SparseMatrix::hasNontrivialRowGrouping() const { + return nontrivialRowGrouping; + } + template ValueType SparseMatrix::getRowSum(index_type row) const { ValueType sum = storm::utility::zero(); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 45e7b19ae..16c7fac19 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -149,6 +149,14 @@ namespace storm { */ SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0); + /*! + * Moves the contents of the given matrix into the matrix builder so that its contents can be modified again. + * This is, for example, useful if rows need to be added to the matrix. + * + * @param matrix The matrix that is to be made editable again. + */ + SparseMatrixBuilder(SparseMatrix&& matrix); + /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, * a call to finalize(false) is mandatory. @@ -193,6 +201,20 @@ namespace storm { */ SparseMatrix build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0); + /*! + * Retrieves the most recently used row. + * + * @return The most recently used row. + */ + index_type getLastRow() const; + + /*! + * Retrieves the most recently used row. + * + * @return The most recently used row. + */ + index_type getLastColumn() const; + private: // A flag indicating whether a row count was set upon construction. bool initialRowCountSet; @@ -277,6 +299,7 @@ namespace storm { friend class storm::adapters::EigenAdapter; friend class storm::adapters::StormAdapter; friend class storm::solver::TopologicalValueIterationMinMaxLinearEquationSolver; + friend class SparseMatrixBuilder; typedef uint_fast64_t index_type; typedef ValueType value_type; @@ -402,8 +425,9 @@ namespace storm { * @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. + * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial. */ - SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); + SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices, bool hasNontrivialRowGrouping); /*! * Constructs a sparse matrix by moving the given contents. @@ -412,8 +436,9 @@ namespace storm { * @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. + * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial. */ - SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); + SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices, bool hasNontrivialRowGrouping); /*! * Assigns the contents of the given matrix to the current one by deep-copying its contents. @@ -798,6 +823,13 @@ namespace storm { * @return An iterator that points past the end of the last row of the matrix. */ iterator end(); + + /*! + * Retrieves whether the matrix has a (possibly) non-trivial row grouping. + * + * @return True iff the matrix has a (possibly) non-trivial row grouping. + */ + bool hasNontrivialRowGrouping() const; /*! * Returns a copy of the matrix with the chosen internal data type @@ -813,7 +845,7 @@ namespace storm { new_columnsAndValues.at(i) = MatrixEntry(columnsAndValues.at(i).getColumn(), static_cast(columnsAndValues.at(i).getValue())); } - return SparseMatrix(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices)); + return SparseMatrix(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices), nontrivialRowGrouping); } private: @@ -852,6 +884,10 @@ namespace storm { // entry is not included anymore. std::vector rowIndications; + // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one + // row per row group. + bool nontrivialRowGrouping; + // A vector indicating the row groups of the matrix. std::vector rowGroupIndices; }; diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 6b7f2067f..5eaded696 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -557,7 +557,7 @@ namespace storm { rowIndications[0] = 0; // Construct matrix and return result. - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); } storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { @@ -680,7 +680,7 @@ namespace storm { } rowIndications[0] = 0; - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); } std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { @@ -804,7 +804,7 @@ namespace storm { } rowIndications[0] = 0; - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector)); + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); } template diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 20716916a..d16b5558d 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -154,8 +154,8 @@ 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, {0, 1, 2, 3})); - storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}); + ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}, false)); + storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}, false); ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); @@ -328,7 +328,7 @@ TEST(SparseMatrix, Submatrix) { ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build()); - + std::vector rowGroupIndices = {0, 1, 2, 4, 5}; storm::storage::BitVector rowGroupConstraint(4);