From 40285bac26f4cc6c8c0d882c728b90c707297da2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 14 Mar 2018 17:35:06 +0100 Subject: [PATCH] handled early termination in svi more carefully --- .../helper/SoundValueIterationHelper.cpp | 21 ++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/storm/solver/helper/SoundValueIterationHelper.cpp b/src/storm/solver/helper/SoundValueIterationHelper.cpp index 68bd1f03a..ab0ace1a7 100644 --- a/src/storm/solver/helper/SoundValueIterationHelper.cpp +++ b/src/storm/solver/helper/SoundValueIterationHelper.cpp @@ -282,9 +282,24 @@ namespace storm { template void SoundValueIterationHelper::setSolutionVector() { - STORM_LOG_WARN_COND(hasLowerBound && hasUpperBound, "No lower or upper result bound could be computed within the given number of Iterations."); - - ValueType meanBound = (upperBound + lowerBound) / storm::utility::convertNumber(2.0); + + // Due to a custom termination criterion it might be the case that one of the bounds was not yet established. + ValueType meanBound; + if (!hasLowerBound) { + STORM_LOG_WARN("No lower result bound was computed during sound value iteration."); + if (hasUpperBound) { + meanBound = upperBound; + } else { + STORM_LOG_WARN("No upper result bound was computed during sound value iteration."); + meanBound = storm::utility::zero(); + } + } else if (!hasUpperBound) { + STORM_LOG_WARN("No upper result bound was computed during sound value iteration."); + meanBound = lowerBound; + } else { + meanBound = (upperBound + lowerBound) / storm::utility::convertNumber(2.0); + } + storm::utility::vector::applyPointwise(x, y, x, [&meanBound] (ValueType const& xi, ValueType const& yi) { return xi + yi * meanBound; }); STORM_LOG_INFO("Sound Value Iteration terminated with lower value bound "