From 2c23b1ed993ccc5931e1f07a0ed1f56742946d46 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 Jun 2016 16:28:56 +0200 Subject: [PATCH] fixed bug in sparse DTMC model checker Former-commit-id: 41d21093c0c72e1c0d2715ae134314518f1c6c56 --- src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 98cbcf2ea..692a4028e 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -127,12 +127,12 @@ namespace storm { template std::vector SparseDtmcPrctlHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Initialize result to the null vector. + std::vector result(transitionMatrix.getRowCount()); + // Compute the reward vector to add in each step based on the available reward models. std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); - // Initialize result to either the state rewards of the model or the null vector. - std::vector result = rewardModel.getTotalStateActionRewardVector(transitionMatrix.getRowCount(), transitionMatrix.getRowGroupIndices()); - // Perform the matrix vector multiplication as often as required by the formula bound. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); solver->performMatrixVectorMultiplication(result, &totalRewardVector, stepBound);