Browse Source

Fixed explicit dft model builder.

tempestpy_adaptions
TimQu 8 years ago
parent
commit
790ae46e4f
  1. 1
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 10
      src/storm/storage/SparseMatrix.cpp
  3. 6
      src/storm/storage/SparseMatrix.h

1
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@ -141,6 +141,7 @@ namespace storm {
storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
components.exitRates = std::move(modelComponents.exitRates);
if (deterministic) {
components.transitionMatrix.makeRowGroupingTrivial();
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
} else {
components.markovianStates = std::move(modelComponents.markovianStates);

10
src/storm/storage/SparseMatrix.cpp

@ -1472,6 +1472,16 @@ namespace storm {
return trivialRowGrouping;
}
template<typename ValueType>
void SparseMatrix<ValueType>::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<typename ValueType>
ValueType SparseMatrix<ValueType>::getRowSum(index_type row) const {
ValueType sum = storm::utility::zero<ValueType>();

6
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

Loading…
Cancel
Save