From d054f3c64a5909100c5d6f2cf6b27b98cd5a7553 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 7 Dec 2018 00:06:58 +0100 Subject: [PATCH] Result for upper bounds needs only be calculated for k=0 --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 1671f6245..0b7d03b95 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -391,14 +391,16 @@ namespace storm { calculateUnifPlusVector(env, k, state, false, lambda, numberOfProbabilisticChoices, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); } - // Calculate result for upper bound - // resUpperNew was already initialized with zeros - uint64_t left = std::max(foxGlynnResult.left, (uint64_t)(k)); - uint64_t right = std::min(foxGlynnResult.right, N-1); - for (uint64_t state = 0; state < numberOfStates; ++state) { - for (uint64_t i = left; i <= right; ++i) { - STORM_LOG_ASSERT(unifVectors.wUpper[N-1-(i-k)][state] != -1, "wUpper was not computed before."); - unifVectors.resUpperNew[state] += foxGlynnResult.weights[i - foxGlynnResult.left] * unifVectors.wUpper[N-1-(i-k)][state]; + if (k == 0) { + // Calculate result for upper bound + // resUpperNew was already initialized with zeros + uint64_t left = std::max(foxGlynnResult.left, (uint64_t)(k)); + uint64_t right = std::min(foxGlynnResult.right, N-1); + for (uint64_t state = 0; state < numberOfStates; ++state) { + for (uint64_t i = left; i <= right; ++i) { + STORM_LOG_ASSERT(unifVectors.wUpper[N-1-(i-k)][state] != -1, "wUpper was not computed before."); + unifVectors.resUpperNew[state] += foxGlynnResult.weights[i - foxGlynnResult.left] * unifVectors.wUpper[N-1-(i-k)][state]; + } } } }