From 14f07a2d1a7b6312d8acea85af40de58470925e5 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 6 Mar 2020 16:28:59 +0100
Subject: [PATCH] Unif+: Update kappa only based on the results at the initial
state
---
.../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index eaca15f80..d188f7a35 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -224,7 +224,12 @@ namespace storm {
if (relativePrecision) {
// Reduce kappa a bit
- ValueType minValue = *std::min_element(maybeStatesValuesUpper.begin(), maybeStatesValuesUpper.end());
+ ValueType minValue;
+ if (relevantMaybeStates) {
+ minValue = storm::utility::vector::min_if(maybeStatesValuesUpper, relevantMaybeStates.get());
+ } else {
+ minValue = *std::min_element(maybeStatesValuesUpper.begin(), maybeStatesValuesUpper.end());
+ }
minValue *= storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getUnifPlusKappa());
kappa = std::min(kappa, minValue);
STORM_LOG_DEBUG("Decreased kappa to " << kappa << ".");