Added SolverStatus::Abort for abort signal handling

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -4,21 +4,18 @@
 #include "storm/solver/IterativeMinMaxLinearEquationSolver.h"
 #include "storm/solver/helper/OptimisticValueIterationHelper.h"
 
-#include "storm/utility/ConstantsComparator.h"
-
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/OviSolverEnvironment.h"
 
+#include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/KwekMehlhorn.h"
 #include "storm/utility/NumberTraits.h"
-
-#include "storm/utility/Stopwatch.h"
-#include "storm/utility/vector.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
 #include "storm/exceptions/InvalidEnvironmentException.h"
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/UnmetRequirementException.h"
-#include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/PrecisionExceededException.h"
 
 namespace storm {
@@ -206,6 +203,9 @@ namespace storm {
 
                 // Potentially show progress.
                 this->showProgressIterative(iterations);
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             } while (status == SolverStatus::InProgress);
             
             reportStatus(status, iterations);
@@ -749,6 +749,9 @@ namespace storm {
                 
                 // Potentially show progress.
                 this->showProgressIterative(iterations);
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             this->soundValueIterationHelper->setSolutionVector();
             
@@ -1047,6 +1050,9 @@ namespace storm {
                     // Increase the precision.
                     precision /= storm::utility::convertNumber<ValueType>(static_cast<uint64_t>(10));
                 }
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             
             // Swap the two vectors if the current result is not in the original x.
@@ -1105,6 +1111,8 @@ namespace storm {
                     status = SolverStatus::TerminatedEarly;
                 } else if (iterations >= maximalNumberOfIterations) {
                     status = SolverStatus::MaximalIterationsExceeded;
+                } else if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
                 }
             }
             return status;
@@ -1116,6 +1124,7 @@ namespace storm {
                 case SolverStatus::Converged: STORM_LOG_TRACE("Iterative solver converged after " << iterations << " iterations."); break;
                 case SolverStatus::TerminatedEarly: STORM_LOG_TRACE("Iterative solver terminated early after " << iterations << " iterations."); break;
                 case SolverStatus::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
+                case SolverStatus::Aborted: STORM_LOG_WARN("Iterative solver was aborted."); break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly.");
             }

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -7,6 +7,7 @@
 #include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/KwekMehlhorn.h"
 #include "storm/utility/NumberTraits.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/solver/helper/SoundValueIterationHelper.h"
@@ -309,10 +310,9 @@ namespace storm {
 
             bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel;
             
-            bool converged = false;
-            bool terminate = this->terminateNow(*currentX, guarantee);
             uint64_t iterations = currentIterations;
-            while (!converged && !terminate && iterations < maxIterations) {
+            SolverStatus status = this->terminateNow(*currentX, guarantee) ? SolverStatus::TerminatedEarly : SolverStatus::InProgress;
+            while (status == SolverStatus::InProgress && iterations < maxIterations) {
                 if (useGaussSeidelMultiplication) {
                     *newX = *currentX;
                     this->multiplier->multiplyGaussSeidel(env, *newX, &b);
@@ -321,18 +321,28 @@ namespace storm {
                 }
                 
                 // Check for convergence.
-                converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative);
+                if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
+                    status = SolverStatus::Converged;
+                }
 
                 // Check for termination.
                 std::swap(currentX, newX);
                 ++iterations;
-                terminate = this->terminateNow(*currentX, guarantee);
-                
+                if (this->terminateNow(*currentX, guarantee)) {
+                    status = SolverStatus::TerminatedEarly;
+                }
+
                 // Potentially show progress.
                 this->showProgressIterative(iterations);
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
-            
-            return PowerIterationResult(iterations - currentIterations, converged ? SolverStatus::Converged : (terminate ? SolverStatus::TerminatedEarly : SolverStatus::MaximalIterationsExceeded));
+            if (status == SolverStatus::InProgress && iterations == maxIterations) {
+                status = SolverStatus::MaximalIterationsExceeded;
+            }
+
+            return PowerIterationResult(iterations - currentIterations, status);
         }
         
         template<typename ValueType>
@@ -773,6 +783,9 @@ namespace storm {
                     // Increase the precision.
                     precision = precision / 10;
                 }
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             
             // Swap the two vectors if the current result is not in the original x.

src/storm/solver/SolverStatus.cpp

@@ -9,6 +9,7 @@ namespace storm {
                 case SolverStatus::TerminatedEarly: out << "terminated"; break;
                 case SolverStatus::MaximalIterationsExceeded: out << "maximal iterations exceeded"; break;
                 case SolverStatus::InProgress: out << "in progress"; break;
+                case SolverStatus::Aborted: out << "aborted"; break;
             }
             return out;
         }

src/storm/solver/SolverStatus.h

@@ -6,7 +6,7 @@ namespace storm {
     namespace solver {
         
         enum class SolverStatus {
-            Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
+            Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress, Aborted
         };
      
         std::ostream& operator<<(std::ostream& out, SolverStatus const& status);

src/storm/solver/StandardGameSolver.cpp

@@ -12,6 +12,7 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/utility/ConstantsComparator.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/macros.h"
@@ -566,6 +567,8 @@ namespace storm {
                     status = SolverStatus::TerminatedEarly;
                 } else if (iterations >= maximalNumberOfIterations) {
                     status = SolverStatus::MaximalIterationsExceeded;
+                } else if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
                 }
             }
             return status;
@@ -577,6 +580,7 @@ namespace storm {
                 case SolverStatus::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break;
                 case SolverStatus::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break;
                 case SolverStatus::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
+                case SolverStatus::Aborted: STORM_LOG_WARN("Iterative solver was aborted."); break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly.");
             }

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -11,6 +11,7 @@
 
 #include "storm/utility/dd.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/exceptions/InvalidEnvironmentException.h"
 #include "storm/exceptions/PrecisionExceededException.h"
 
@@ -98,9 +99,12 @@ namespace storm {
                 // Set up next iteration.
                 localX = tmp;
                 ++iterations;
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             
-            if (status != SolverStatus::Converged) {
+            if (status == SolverStatus::InProgress && iterations < maximalIterations) {
                 status = SolverStatus::MaximalIterationsExceeded;
             }
             
@@ -177,9 +181,12 @@ namespace storm {
                     currentX = viResult.values;
                     precision /= storm::utility::convertNumber<ValueType, uint64_t>(10);
                 }
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             
-            if (status == SolverStatus::InProgress) {
+            if (status == SolverStatus::InProgress && overallIterations < maxIter) {
                 status = SolverStatus::MaximalIterationsExceeded;
             }
             

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -1,17 +1,15 @@
 #include "storm/solver/SymbolicNativeLinearEquationSolver.h"
 
+#include "storm/environment/solver/NativeSolverEnvironment.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/PrecisionExceededException.h"
 #include "storm/storage/dd/DdManager.h"
 #include "storm/storage/dd/Add.h"
-
-#include "storm/utility/dd.h"
 #include "storm/utility/constants.h"
-
-#include "storm/environment/solver/NativeSolverEnvironment.h"
-
+#include "storm/utility/dd.h"
 #include "storm/utility/KwekMehlhorn.h"
 #include "storm/utility/macros.h"
-#include "storm/exceptions/NotSupportedException.h"
-#include "storm/exceptions/PrecisionExceededException.h"
+#include "storm/utility/SignalHandler.h"
 
 namespace storm {
     namespace solver {
@@ -222,9 +220,12 @@ namespace storm {
                     currentX = result.values;
                     precision /= storm::utility::convertNumber<ValueType, uint64_t>(10);
                 }
+                if (storm::utility::resources::isTerminate()) {
+                    status = SolverStatus::Aborted;
+                }
             }
             
-            if (status == SolverStatus::InProgress) {
+            if (status == SolverStatus::InProgress && overallIterations == maxIter) {
                 status = SolverStatus::MaximalIterationsExceeded;
             }
             

src/storm/solver/helper/OptimisticValueIterationHelper.h

@@ -7,6 +7,7 @@
 #include "storm/solver/SolverStatus.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/ProgressMeasurement.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/storage/BitVector.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/OviSolverEnvironment.h"
@@ -230,8 +231,11 @@ namespace storm {
                                 }
                             }
                         }
+                        if (storm::utility::resources::isTerminate()) {
+                            status = SolverStatus::Aborted;
+                        }
                     }
-                }
+                } // end while
                 
                 // Swap the results into the output vectors.
                 if (initLowerX == lowerX) {