diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 25daedf7a..4a29b0652 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -141,6 +141,7 @@ namespace storm { storm::storage::sparse::ModelComponents components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); components.exitRates = std::move(modelComponents.exitRates); if (deterministic) { + components.transitionMatrix.makeRowGroupingTrivial(); model = std::make_shared>(std::move(components)); } else { components.markovianStates = std::move(modelComponents.markovianStates); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index c42fa1bd0..18157bb94 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1472,6 +1472,16 @@ namespace storm { return trivialRowGrouping; } + template + void SparseMatrix::makeRowGroupingTrivial() { + if (trivialRowGrouping) { + STORM_LOG_ASSERT(!rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1), "Row grouping is supposed to be trivial but actually it is not."); + } else { + trivialRowGrouping = true; + rowGroupIndices = boost::none; + } + } + template ValueType SparseMatrix::getRowSum(index_type row) const { ValueType sum = storm::utility::zero(); diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index ba7d606a7..01e4079a0 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -998,6 +998,12 @@ s * @param insertDiagonalEntries If set to true, the resulting matri * @return True iff the matrix has a trivial row grouping. */ bool hasTrivialRowGrouping() const; + + /*! + * Makes the row grouping of this matrix trivial. + * Has no effect when the row grouping is already trivial. + */ + void makeRowGroupingTrivial(); /*! * Returns a copy of the matrix with the chosen internal data type