diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 145eed1b1..78f48a173 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -651,15 +651,24 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory*/) { - // Compute expected time on CTMC by reduction to DTMC with rewards + // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + // Initialize rewards. std::vector totalRewardVector; - for (auto exitRate : exitRateVector) { - totalRewardVector.push_back(storm::utility::one() / exitRate); + for (size_t i = 0; i < exitRateVector.size(); ++i) { + std::cout << i << std::endl; + if (targetStates[i]) { + // Set reward for target states to 0. + totalRewardVector.push_back(storm::utility::zero()); + } else { + // Reward is (1 / exitRate). + totalRewardVector.push_back(storm::utility::one() / exitRateVector[i]); + } } return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false, qualitative); - // Enable again, if RationalFunction finally is supported + // Enable again, if RationalFunction finally is supported. //return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); }