diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index fdcf0bb3a..8f63110c8 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -451,7 +451,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType = boost::optional()) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 25beb4093..58a842cd3 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -239,20 +239,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) { - for (auto const& element : *this) { - if (element.getValue() != storm::utility::zero()) { - ++this->nonzeroEntryCount; - } - } + 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)) { - for (auto const& element : *this) { - if (element.getValue() != storm::utility::zero()) { - ++this->nonzeroEntryCount; - } - } + this->updateNonzeroEntryCount(); } template @@ -366,7 +358,23 @@ namespace storm { template typename SparseMatrix::index_type SparseMatrix::getNonzeroEntryCount() const { return nonzeroEntryCount; - } + } + + template + void SparseMatrix::updateNonzeroEntryCount() const { + //SparseMatrix* self = const_cast*>(this); + this->nonzeroEntryCount = 0; + for (auto const& element : *this) { + if (element.getValue() != storm::utility::zero()) { + ++this->nonzeroEntryCount; + } + } + } + + template + void SparseMatrix::updateNonzeroEntryCount(std::make_signed::type difference) { + this->nonzeroEntryCount += difference; + } template typename SparseMatrix::index_type SparseMatrix::getRowGroupCount() const { @@ -416,6 +424,7 @@ namespace storm { columnValuePtr->setValue(storm::utility::one()); ++columnValuePtr; for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { + ++this->nonzeroEntryCount; columnValuePtr->setColumn(0); columnValuePtr->setValue(storm::utility::zero()); } @@ -606,8 +615,12 @@ namespace storm { SparseMatrix SparseMatrix::transpose(bool joinGroups, bool keepZeros) const { index_type rowCount = this->getColumnCount(); index_type columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); - //index_type entryCount = keepZeros ? this->getEntryCount() : this->getNonzeroEntryCount(); this wont work if someone modified the matrix after creation... - index_type entryCount = this->getEntryCount(); + if (keepZeros) { + index_type entryCount = this->getEntryCount(); + } else { + this->updateNonzeroEntryCount(); + index_type entryCount = this->getNonzeroEntryCount(); + } std::vector rowIndications(rowCount + 1); std::vector> columnsAndValues(entryCount); @@ -660,13 +673,22 @@ namespace storm { template void SparseMatrix::invertDiagonal() { // Now iterate over all row groups and set the diagonal elements to the inverted value. - // If there is a row without the diagonal element, an exception is thrown. - ValueType one = storm::utility::one(); + // If there is a row without the diagonal element, an exception is thrown. + ValueType one = storm::utility::one(); + ValueType zero = storm::utility::zero(); bool foundDiagonalElement = false; for (index_type group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { - entry.setValue(one - entry.getValue()); + if (entry.getValue() == one) { + --this->nonzeroEntryCount; + entry.setValue(zero); + } else if (entry.getValue() == zero) { + ++this->nonzeroEntryCount; + entry.setValue(one); + } else { + entry.setValue(one - entry.getValue()); + } foundDiagonalElement = true; } } @@ -696,6 +718,7 @@ namespace storm { for (index_type group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { + --this->nonzeroEntryCount; entry.setValue(storm::utility::zero()); } } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index bf0193c7e..45e7b19ae 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -465,12 +465,26 @@ namespace storm { */ uint_fast64_t getRowGroupEntryCount(uint_fast64_t const group) const; - /*! - * Returns the number of nonzero entries in the matrix. - * - * @return The number of nonzero entries in the matrix. - */ - index_type getNonzeroEntryCount() const; + /*! + * Returns the cached number of nonzero entries in the matrix. + * + * @see updateNonzeroEntryCount() + * + * @return The number of nonzero entries in the matrix. + */ + index_type getNonzeroEntryCount() const; + + /*! + * Recompute the nonzero entry count + */ + void updateNonzeroEntryCount() const; + + /*! + * Change the nonzero entry count by the provided value. + * + * @param difference Difference between old and new nonzero entry count. + */ + void updateNonzeroEntryCount(std::make_signed::type difference); /*! * Returns the number of row groups in the matrix. @@ -827,7 +841,7 @@ namespace storm { index_type entryCount; // The number of nonzero entries in the matrix. - index_type nonzeroEntryCount; + mutable index_type nonzeroEntryCount; // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues;