From b3483211ff47b7f5ca7a559e274cb6c4cdfe96b4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 Feb 2016 19:41:16 +0100 Subject: [PATCH] alpha version of conditional rewards for dtmc Former-commit-id: 1adfb3d405ffb6b2332dc5a71e4238e85dfe7ec5 --- src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 2be798889..9e1b6ef14 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -391,8 +391,8 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + std::vector conditionalRewards = computeReachabilityRewards(newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } }