From 9fddf3858bfb0b99ffb860205cfbd09625c036cb Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 12 Mar 2020 09:47:36 +0100
Subject: [PATCH] Abort topological solvers if requested.

---
 src/storm/solver/TopologicalLinearEquationSolver.cpp       | 7 +++++++
 src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp | 7 +++++++
 2 files changed, 14 insertions(+)

diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp
index 4a797fc53..ba1a6e2db 100644
--- a/src/storm/solver/TopologicalLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp
@@ -7,6 +7,7 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidEnvironmentException.h"
 #include "storm/exceptions/UnexpectedException.h"
+#include "storm/utility/SignalHandler.h"
 
 namespace storm {
     namespace solver {
@@ -79,6 +80,7 @@ namespace storm {
                 returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b);
             } else {
                 storm::storage::BitVector sccAsBitVector(x.size(), false);
+                uint64_t sccIndex = 0;
                 for (auto const& scc : *this->sortedSccDecomposition) {
                     if (scc.size() == 1) {
                         returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue;
@@ -89,6 +91,11 @@ namespace storm {
                         }
                         returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue;
                     }
+                    ++sccIndex;
+                    if (storm::utility::resources::isTerminate()) {
+                        STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs.");
+                        break;
+                    }
                 }
             }
             
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
index 32f18ca0a..e22b53985 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -9,6 +9,7 @@
 #include "storm/exceptions/InvalidEnvironmentException.h"
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/UncheckedRequirementException.h"
+#include "storm/utility/SignalHandler.h"
 
 namespace storm {
     namespace solver {
@@ -77,6 +78,7 @@ namespace storm {
                 }
                 storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false);
                 storm::storage::BitVector sccRowsAsBitVector(b.size(), false);
+                uint64_t sccIndex = 0;
                 for (auto const& scc : *this->sortedSccDecomposition) {
                     if (scc.size() == 1) {
                         returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
@@ -92,6 +94,11 @@ namespace storm {
                         }
                         returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue;
                     }
+                    ++sccIndex;
+                    if (storm::utility::resources::isTerminate()) {
+                        STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs.");
+                        break;
+                    }
                 }
                 
                 // If requested, we store the scheduler for retrieval.