Browse Source

fixed an issue pointed out by Tim

tempestpy_adaptions
dehnert 7 years ago
parent
commit
99647c11fb
  1. 4
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 11
      src/storm/storage/SparseMatrix.cpp
  3. 7
      src/storm/storage/SparseMatrix.h

4
src/storm/builder/ExplicitModelBuilder.cpp

@ -309,8 +309,8 @@ namespace storm {
buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates);
// Initialize the model components with the obtained information.
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getLastRowGroup()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
// Now finalize all reward models.
for (auto& rewardModelBuilder : rewardModelBuilders) {
modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));

11
src/storm/storage/SparseMatrix.cpp

@ -271,7 +271,16 @@ namespace storm {
typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getLastRow() const {
return lastRow;
}
template<typename ValueType>
typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getLastRowGroup() const {
if (this->hasCustomRowGrouping) {
return currentRowGroup;
} else {
return getLastRow();
}
}
template<typename ValueType>
typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getLastColumn() const {
return lastColumn;

7
src/storm/storage/SparseMatrix.h

@ -219,6 +219,13 @@ namespace storm {
*/
index_type getLastRow() const;
/*!
* Retrieves the most recently used row group.
*
* @return The most recently used row group.
*/
index_type getLastRowGroup() const;
/*!
* Retrieves the most recently used row.
*

Loading…
Cancel
Save