From 3debbbc64dea706c7c7864a2973115ab02380317 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 5 Mar 2020 15:38:27 +0100
Subject: [PATCH] Added more abortion checks

---
 .../helper/SparseMarkovAutomatonCslHelper.cpp | 49 ++++++++++---------
 ...ewardBoundedMdpPcaaWeightVectorChecker.cpp | 35 ++++++-------
 .../prctl/helper/SparseDtmcPrctlHelper.cpp    |  4 ++
 .../prctl/helper/SparseMdpPrctlHelper.cpp     |  4 ++
 4 files changed, 52 insertions(+), 40 deletions(-)

diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 76b603142..eaca15f80 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -1,41 +1,32 @@
 #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h"
 
-#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
-
-#include "storm/models/sparse/StandardRewardModel.h"
-
-#include "storm/storage/StronglyConnectedComponentDecomposition.h"
-#include "storm/storage/MaximalEndComponentDecomposition.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
-
 #include "storm/environment/Environment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/TopologicalSolverEnvironment.h"
 #include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
 #include "storm/environment/solver/EigenSolverEnvironment.h"
 #include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
-
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
+#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/solver/Multiplier.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/LpSolver.h"
+#include "storm/storage/StronglyConnectedComponentDecomposition.h"
+#include "storm/storage/MaximalEndComponentDecomposition.h"
+#include "storm/storage/expressions/Variable.h"
+#include "storm/storage/expressions/Expression.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/NumberTraits.h"
 #include "storm/utility/SignalHandler.h"
 
-#include "storm/storage/expressions/Variable.h"
-#include "storm/storage/expressions/Expression.h"
-#include "storm/storage/expressions/ExpressionManager.h"
-
-#include "storm/solver/Multiplier.h"
-#include "storm/solver/MinMaxLinearEquationSolver.h"
-#include "storm/solver/LpSolver.h"
 
-#include "storm/exceptions/InvalidStateException.h"
-#include "storm/exceptions/InvalidPropertyException.h"
-#include "storm/exceptions/InvalidOperationException.h"
-#include "storm/exceptions/UncheckedRequirementException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -203,6 +194,9 @@ namespace storm {
                                 }
 
                                 progressSteps.updateProgress(N-k);
+                                if (storm::utility::resources::isTerminate()) {
+                                    break;
+                                }
                             }
                             if (computeLowerBound) {
                                 storm::utility::vector::scaleVectorInPlace(maybeStatesValuesLower, storm::utility::one<ValueType>() / foxGlynnResult.totalWeight);
@@ -215,6 +209,9 @@ namespace storm {
                             if (converged) {
                                 break;
                             }
+                            if (storm::utility::resources::isTerminate()) {
+                                break;
+                            }
                         }
                         
                         if (!converged) {
@@ -240,6 +237,9 @@ namespace storm {
                             std::fill(maybeStatesValuesUpper.begin(), maybeStatesValuesUpper.end(), storm::utility::zero<ValueType>());
                         }
                         progressIterations.updateProgress(++iteration);
+                        if (storm::utility::resources::isTerminate()) {
+                            break;
+                        }
                     }
                     
                     // We take the average of the lower and upper bounds
@@ -529,6 +529,9 @@ namespace storm {
                     } else {
                         storm::utility::vector::addVectors(markovianNonGoalValues, bMarkovianFixed, markovianNonGoalValues);
                     }
+                    if (storm::utility::resources::isTerminate()) {
+                        break;
+                    }
                 }
                 
                 if (existProbabilisticStates) {
diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
index 548eb1390..fee359020 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
@@ -1,31 +1,29 @@
 #include "storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
-#include "storm/models/sparse/Mdp.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
-#include "storm/utility/macros.h"
-#include "storm/utility/vector.h"
-#include "storm/utility/ProgressMeasurement.h"
-#include "storm/logic/Formulas.h"
-#include "storm/solver/MinMaxLinearEquationSolver.h"
-#include "storm/solver/LinearEquationSolver.h"
-
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/utility/export.h"
-#include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/CoreSettings.h"
-
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/UncheckedRequirementException.h"
+#include "storm/logic/Formulas.h"
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/LinearEquationSolver.h"
+#include "storm/utility/ProgressMeasurement.h"
+#include "storm/utility/SignalHandler.h"
+#include "storm/utility/export.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
 
 
 namespace storm {
@@ -101,6 +99,9 @@ namespace storm {
                     }
                     ++numCheckedEpochs;
                     progress.updateProgress(numCheckedEpochs);
+                    if (storm::utility::resources::isTerminate()) {
+                        break;
+                    }
                 }
                 
                 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index a03914c8c..b1ec53e30 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -28,6 +28,7 @@
 
 #include "storm/utility/Stopwatch.h"
 #include "storm/utility/ProgressMeasurement.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/export.h"
 
 #include "storm/utility/macros.h"
@@ -137,6 +138,9 @@ namespace storm {
                     }
                     ++numCheckedEpochs;
                     progress.updateProgress(numCheckedEpochs);
+                    if (storm::utility::resources::isTerminate()) {
+                        break;
+                    }
                 }
                 
                 std::map<storm::storage::sparse::state_type, ValueType> result;
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 122814633..0386d3335 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -32,6 +32,7 @@
 
 #include "storm/utility/Stopwatch.h"
 #include "storm/utility/ProgressMeasurement.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/export.h"
 #include "storm/utility/NumberTraits.h"
 
@@ -135,6 +136,9 @@ namespace storm {
                     }
                     ++numCheckedEpochs;
                     progress.updateProgress(numCheckedEpochs);
+                    if (storm::utility::resources::isTerminate()) {
+                        break;
+                    }
                 }
                 
                 std::map<storm::storage::sparse::state_type, ValueType> result;