Browse Source

fixed bug in sparse DTMC model checker

Former-commit-id: 41d21093c0
tempestpy_adaptions
dehnert 9 years ago
parent
commit
2c23b1ed99
  1. 6
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

6
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@ -127,12 +127,12 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Initialize result to the null vector.
std::vector<ValueType> result(transitionMatrix.getRowCount());
// Compute the reward vector to add in each step based on the available reward models.
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
// Initialize result to either the state rewards of the model or the null vector.
std::vector<ValueType> result = rewardModel.getTotalStateActionRewardVector(transitionMatrix.getRowCount(), transitionMatrix.getRowGroupIndices());
// Perform the matrix vector multiplication as often as required by the formula bound.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix);
solver->performMatrixVectorMultiplication(result, &totalRewardVector, stepBound);

Loading…
Cancel
Save