Browse Source

fixed serious bug in model generation from PRISM code; can't believe that didn't cause wrong models until now

Former-commit-id: 8fef881161
tempestpy_adaptions
dehnert 9 years ago
parent
commit
5d9f225f9f
  1. 8
      src/generator/PrismNextStateGenerator.cpp

8
src/generator/PrismNextStateGenerator.cpp

@ -336,9 +336,17 @@ namespace storm {
for (auto const& stateProbabilityPair : *currentTargetStates) { for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states. // Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update); CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
// 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())); newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
} }
} }
}
// If there is one more command to come, shift the target states one time step back. // If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) { if (i < iteratorList.size() - 1) {

Loading…
Cancel
Save