From 0e91887ebb363b29ec3dcb229a2a219495c0b83c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 9 Mar 2020 17:09:31 +0100
Subject: [PATCH] Queried the termination flag in a few more places.
---
.../csl/helper/SparseCtmcCslHelper.cpp | 4 ++++
.../helper/SparseMarkovAutomatonCslHelper.cpp | 6 +++---
.../prctl/helper/SparseMdpPrctlHelper.cpp | 3 +++
src/storm/settings/modules/ResourceSettings.cpp | 2 +-
src/storm/solver/Multiplier.cpp | 17 +++++++++++++++++
5 files changed, 28 insertions(+), 4 deletions(-)
diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 64f734e67..e163e0c02 100644
--- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -22,6 +22,7 @@
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/utility/numerical.h"
+#include "storm/utility/SignalHandler.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/InvalidStateException.h"
@@ -688,6 +689,9 @@ namespace storm {
if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) {
break;
}
+ if (storm::utility::resources::isTerminate()) {
+ break;
+ }
}
if (maxIter.is_initialized() && iter == maxIter.get()) {
STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations.");
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 38d62b1f3..0ce9d485f 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -222,9 +222,6 @@ 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);
@@ -1134,6 +1131,9 @@ namespace storm {
if ((maxDiff - minDiff) <= (relative ? (precision * (v.front() + minDiff)) : precision)) {
break;
}
+ if (storm::utility::resources::isTerminate()) {
+ break;
+ }
// update the rhs of the MinMax equation system
ValueType referenceValue = v.front();
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 0386d3335..174cf739f 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -1598,6 +1598,9 @@ namespace storm {
if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) {
break;
}
+ if (storm::utility::resources::isTerminate()) {
+ break;
+ }
}
if (maxIter.is_initialized() && iter == maxIter.get()) {
STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations.");
diff --git a/src/storm/settings/modules/ResourceSettings.cpp b/src/storm/settings/modules/ResourceSettings.cpp
index a8cc9a44e..4f9245dca 100644
--- a/src/storm/settings/modules/ResourceSettings.cpp
+++ b/src/storm/settings/modules/ResourceSettings.cpp
@@ -21,7 +21,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setIsAdvanced().setShortName(timeoutOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "Seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, signalWaitingTimeOptionName, false, "If given, computation will abort after the timeout has been reached.").setIsAdvanced()
+ this->addOption(storm::settings::OptionBuilder(moduleName, signalWaitingTimeOptionName, false, "Specifies how much time can pass until termination when receiving a termination signal.").setIsAdvanced()
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "Seconds after which to exit the program.").setDefaultValueUnsignedInteger(3).build()).build());
}
diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp
index f0a5c4204..4049b56ca 100644
--- a/src/storm/solver/Multiplier.cpp
+++ b/src/storm/solver/Multiplier.cpp
@@ -13,6 +13,8 @@
#include "storm/solver/GmmxxMultiplier.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/utility/SignalHandler.h"
+#include "storm/utility/ProgressMeasurement.h"
namespace storm {
namespace solver {
@@ -39,15 +41,30 @@ namespace storm {
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
+ storm::utility::ProgressMeasurement progress("multiplications");
+ progress.setMaxCount(n);
+ progress.startNewMeasurement(0);
for (uint64_t i = 0; i < n; ++i) {
+ progress.updateProgress(i);
multiply(env, x, b, x);
+ if (storm::utility::resources::isTerminate()) {
+ STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications.");
+ break;
+ }
}
}
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
+ storm::utility::ProgressMeasurement progress("multiplications");
+ progress.setMaxCount(n);
+ progress.startNewMeasurement(0);
for (uint64_t i = 0; i < n; ++i) {
multiplyAndReduce(env, dir, x, b, x);
+ if (storm::utility::resources::isTerminate()) {
+ STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications");
+ break;
+ }
}
}