From 5d9f225f9f1af6f38bc64f4f89240aadcf6bb027 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 16 Apr 2016 17:00:11 +0200 Subject: [PATCH] fixed serious bug in model generation from PRISM code; can't believe that didn't cause wrong models until now Former-commit-id: 8fef881161689e3521bd2ea28934e9f692e2661e --- src/generator/PrismNextStateGenerator.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 3ba8b89f7..9ccec9605 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -336,7 +336,15 @@ namespace storm { for (auto const& stateProbabilityPair : *currentTargetStates) { // Compute the new state under the current update and add it to the set of new target states. CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update); - newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); + + // If the new state was already found as a successor state, update the probability + // and otherwise insert it. + auto targetStateIt = newTargetStates->find(newTargetState); + if (targetStateIt != newTargetStates->end()) { + targetStateIt->second += stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()); + } else { + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); + } } }