From 1136ff0d374ff05fae6f3afabdd8580da475e284 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 1 Apr 2016 14:36:00 +0200 Subject: [PATCH] fixed a failing test (uninitialized data issue) Former-commit-id: ca0f456ba25e349aaca113677fdc1f8b37f31925 --- src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 1 + src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 9e1b6ef14..98cbcf2ea 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -367,6 +367,7 @@ 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); } } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 637c30cb5..0be762298 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -45,6 +45,10 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); struct BaierTransformedModel { + BaierTransformedModel() : noTargetStates(false) { + // Intentionally left empty. + } + storm::storage::BitVector beforeStates; boost::optional> transitionMatrix; boost::optional targetStates;