diff --git a/src/storm/exceptions/AbortException.h b/src/storm/exceptions/AbortException.h new file mode 100644 index 000000000..b04f5f588 --- /dev/null +++ b/src/storm/exceptions/AbortException.h @@ -0,0 +1,12 @@ +#pragma once + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(AbortException) + + } +} diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index a42386c0e..9142ba1d6 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -4,14 +4,12 @@ #include #include "storm/adapters/GmmxxAdapter.h" - #include "storm/environment/solver/GmmxxSolverEnvironment.h" - -#include "storm/utility/vector.h" +#include "storm/exceptions/AbortException.h" #include "storm/utility/constants.h" - #include "storm/utility/gmm.h" #include "storm/utility/vector.h" +#include "storm/utility/SignalHandler.h" namespace storm { namespace solver { @@ -71,32 +69,38 @@ namespace storm { maxIter = env.solver().gmmxx().getMaximalNumberOfIterations(); } gmm::iteration iter(storm::utility::convertNumber(env.solver().gmmxx().getPrecision()), 0, maxIter); - - // Invoke gmm with the corresponding settings - if (method == GmmxxLinearEquationSolverMethod::Bicgstab) { - if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { - gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { - gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { - gmm::bicgstab(*gmmxxA, x, b, gmm::identity_matrix(), iter); - } - } else if (method == GmmxxLinearEquationSolverMethod::Qmr) { - if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { - gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { - gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { - gmm::qmr(*gmmxxA, x, b, gmm::identity_matrix(), iter); - } - } else if (method == GmmxxLinearEquationSolverMethod::Gmres) { - if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { - gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { - gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); - } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { - gmm::gmres(*gmmxxA, x, b, gmm::identity_matrix(), env.solver().gmmxx().getRestartThreshold(), iter); + iter.set_callback([](const gmm::iteration& iteration) -> void { STORM_LOG_THROW(!storm::utility::resources::isTerminate(), storm::exceptions::AbortException, "Gmm++ (externally) aborted after " << iteration.get_iteration() << " iterations."); }); + + // We use throwing an exception to abort within Gmm++ + try { + // Invoke gmm with the corresponding settings + if (method == GmmxxLinearEquationSolverMethod::Bicgstab) { + if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { + gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { + gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { + gmm::bicgstab(*gmmxxA, x, b, gmm::identity_matrix(), iter); + } + } else if (method == GmmxxLinearEquationSolverMethod::Qmr) { + if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { + gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { + gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { + gmm::qmr(*gmmxxA, x, b, gmm::identity_matrix(), iter); + } + } else if (method == GmmxxLinearEquationSolverMethod::Gmres) { + if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { + gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { + gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); + } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { + gmm::gmres(*gmmxxA, x, b, gmm::identity_matrix(), env.solver().gmmxx().getRestartThreshold(), iter); + } } + } catch (storm::exceptions::AbortException const& e) { + // Do nothing } if (!this->isCachingEnabled()) {