From d35d31ce943c23cd484bd30af5dd663f243752ea Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 5 Mar 2020 15:13:35 +0100 Subject: [PATCH] Added SolverStatus::Abort for abort signal handling --- .../IterativeMinMaxLinearEquationSolver.cpp | 21 ++++++++++---- .../solver/NativeLinearEquationSolver.cpp | 29 ++++++++++++++----- src/storm/solver/SolverStatus.cpp | 1 + src/storm/solver/SolverStatus.h | 2 +- src/storm/solver/StandardGameSolver.cpp | 4 +++ .../SymbolicMinMaxLinearEquationSolver.cpp | 11 +++++-- .../SymbolicNativeLinearEquationSolver.cpp | 17 ++++++----- .../helper/OptimisticValueIterationHelper.h | 6 +++- 8 files changed, 65 insertions(+), 26 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 9ea865138..1c5506bae 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/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(static_cast(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."); } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index da2ba626d..067a2a5cf 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/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(*currentX, *newX, precision, relative); + if (storm::utility::vector::equalModuloPrecision(*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 @@ -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. diff --git a/src/storm/solver/SolverStatus.cpp b/src/storm/solver/SolverStatus.cpp index 116a39fc9..b411d59fd 100644 --- a/src/storm/solver/SolverStatus.cpp +++ b/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; } diff --git a/src/storm/solver/SolverStatus.h b/src/storm/solver/SolverStatus.h index 624890f3a..114b08543 100644 --- a/src/storm/solver/SolverStatus.h +++ b/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); diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 9f20b568b..812fdb3c6 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/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."); } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 2ba997ed8..db5cc8915 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/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(10); } + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; + } } - if (status == SolverStatus::InProgress) { + if (status == SolverStatus::InProgress && overallIterations < maxIter) { status = SolverStatus::MaximalIterationsExceeded; } diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 95a9769ba..b21819b5a 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/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(10); } + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; + } } - if (status == SolverStatus::InProgress) { + if (status == SolverStatus::InProgress && overallIterations == maxIter) { status = SolverStatus::MaximalIterationsExceeded; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 1adb29b38..2869540d6 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/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) {