From 3bb3ff9bc7568b1b56390dade9b18c98e44642fb Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 27 Feb 2020 20:48:41 +0100
Subject: [PATCH] Support abortion in Unif+

---
 .../csl/helper/SparseMarkovAutomatonCslHelper.cpp        | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 2a39daf3c..3931279c1 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -29,6 +29,8 @@
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/solver/LpSolver.h"
 
+#include "storm/utility/resources.h"
+
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/InvalidOperationException.h"
@@ -403,6 +405,10 @@ namespace storm {
                                 unifVectors.resUpper[state] += foxGlynnResult.weights[index - foxGlynnResult.left] * unifVectors.wUpperNew[state];
                             }
                         }
+
+                        if (storm::utility::resources::isTerminate()) {
+                            break;
+                        }
                         progressSteps.updateProgress(N-k);
                     }
 
@@ -416,6 +422,9 @@ namespace storm {
                     // (6) Double lambda.
                     lambda *= 2;
                     STORM_LOG_DEBUG("Increased lambda to " << lambda << ", max diff is " << maxNorm << ".");
+                    if (storm::utility::resources::isTerminate()) {
+                        break;
+                    }
                     progressIterations.updateProgress(++iteration);
                 } while (maxNorm > epsilon * (1 - kappa));