From ebc3f61b8298cc889df436d12f88528688ab9f2e Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 11 Dec 2017 16:50:36 +0100 Subject: [PATCH] Fixed wrong size of state reward vector during conditional reward computation --- .../modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 781024096..8d3f0f68d 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -427,7 +427,7 @@ namespace storm { } // Build the new transition matrix and the new targets. - result.transitionMatrix = builder.build(); + result.transitionMatrix = builder.build(addDeadlockState ? (deadlockState + 1) : deadlockState); storm::storage::BitVector newTargetStates = targetStates % result.beforeStates; newTargetStates.resize(result.transitionMatrix.get().getRowCount()); for (auto state : targetStates % statesWithProbabilityGreater0) { @@ -440,15 +440,16 @@ namespace storm { std::vector newStateRewards(result.beforeStates.getNumberOfSetBits()); storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get()); - newStateRewards.reserve(newStateRewards.size() + statesWithProbabilityGreater0.getNumberOfSetBits() + 1); + newStateRewards.reserve(result.transitionMatrix.get().getRowCount()); for (auto state : statesWithProbabilityGreater0) { newStateRewards.push_back(stateRewards.get()[state]); } // Add a zero reward to the deadlock state. - newStateRewards.push_back(storm::utility::zero()); + if (addDeadlockState) { + newStateRewards.push_back(storm::utility::zero()); + } result.stateRewards = std::move(newStateRewards); } - } return result;