From ca59635f8a4b427737859441f38d5e260ebc625a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 3 Mar 2020 22:28:51 +0100 Subject: [PATCH] Using new time bounded environment also for IMCA method. --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 39bfb81a4..bfc0d5b13 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -82,7 +82,7 @@ namespace storm { // Truncation error ValueType kappa = storm::utility::convertNumber(env.solver().timeBounded().getUnifPlusKappa()); // Precision to be achieved - ValueType epsilon = storm::utility::convertNumber(env.solver().timeBounded().getPrecision()); + ValueType epsilon = storm::utility::convertNumber(2.0) * storm::utility::convertNumber(env.solver().timeBounded().getPrecision()); bool relativePrecision = env.solver().timeBounded().getRelativeTerminationCriterion(); // Uniformization rate ValueType lambda = *std::max_element(markovianExitRates.begin(), markovianExitRates.end()); @@ -862,7 +862,7 @@ namespace storm { for (auto value : exitRateVector) { maxExitRate = std::max(maxExitRate, value); } - ValueType delta = (2 * storm::settings::getModule().getPrecision()) / (upperBound * maxExitRate * maxExitRate); + ValueType delta = (2.0 * storm::utility::convertNumber(env.solver().timeBounded().getPrecision())) / (upperBound * maxExitRate * maxExitRate); // (2) Compute the number of steps we need to make for the interval. uint64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta));