From 629de20da04e66901eaee5b99f3250c38afb49dc Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:06:45 +0100
Subject: [PATCH] Fixed running in an infinite loop when computing LRA on
markov automata with relative precision.
---
.../modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index a0c8829bc..c78948727 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -1047,7 +1047,7 @@ namespace storm {
}
// Check for convergence
- if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) {
+ if ((maxDiff - minDiff) <= (relative ? (precision * (v.front() + minDiff)) : precision)) {
break;
}