From ce14b45578fa92477678ab8b904b8098866bc8e5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 2 Oct 2020 12:09:42 +0200 Subject: [PATCH] Pcaa: Implemented termination signal. --- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 5 +++-- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 10 ++++++---- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 9 +++++---- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 8f81dab76..d87edbf00 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/SignalHandler.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" @@ -56,7 +57,7 @@ namespace storm { template bool SparsePcaaAchievabilityQuery::checkAchievability(Environment const& env) { // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx. - while(!this->maxStepsPerformed(env)){ + while (!this->maxStepsPerformed(env) && !storm::utility::resources::isTerminate()) { WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecision(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); @@ -67,7 +68,7 @@ namespace storm { return true; } } - STORM_LOG_ERROR("Could not check whether thresholds are achievable: Exceeded maximum number of refinement steps"); + STORM_LOG_ERROR("Could not check whether thresholds are achievable: Termination requested or maximum number of refinement steps exceeded."); return false; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index c7be2fc7e..f1c4145df 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/SignalHandler.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h" @@ -59,9 +60,12 @@ namespace storm { WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); this->performRefinementStep(env, std::move(direction)); + if (storm::utility::resources::isTerminate()) { + break; + } } - while(!this->maxStepsPerformed(env)) { + while(!this->maxStepsPerformed(env) && !storm::utility::resources::isTerminate()) { // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation std::vector> underApproxHalfspaces = this->underApproximation->getHalfspaces(); std::vector overApproxVertices = this->overApproximation->getVertices(); @@ -84,12 +88,10 @@ namespace storm { WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); this->performRefinementStep(env, std::move(direction)); } - STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); + STORM_LOG_ERROR("Could not reach the desired precision: Termination requested or maximum number of refinement steps exceeded."); } - - #ifdef STORM_HAVE_CARL template class SparsePcaaParetoQuery, storm::RationalNumber>; template class SparsePcaaParetoQuery, storm::RationalNumber>; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index d43aec7c6..f6f640cfa 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -8,6 +8,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/SignalHandler.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/exceptions/InvalidOperationException.h" @@ -97,7 +98,7 @@ namespace storm { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); - while(!this->maxStepsPerformed(env)){ + while(!this->maxStepsPerformed(env) && !storm::utility::resources::isTerminate()){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecisionInAchievabilityPhase(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); @@ -114,7 +115,7 @@ namespace storm { // If there is only one objective than its the optimizing one. Thus the query has to be achievable. return true; } - STORM_LOG_ERROR("Could not check whether thresholds are achievable: Exceeded maximum number of refinement steps"); + STORM_LOG_ERROR("Could not check whether thresholds are achievable: Termination requested or maximum number of refinement steps exceeded."); return false; } @@ -149,7 +150,7 @@ namespace storm { // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. GeometryValueType result = storm::utility::zero(); - while(!this->maxStepsPerformed(env)) { + while(!this->maxStepsPerformed(env) && !storm::utility::resources::isTerminate()) { if (this->refinementSteps.empty()) { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(env.modelchecker().multi().getPrecision())); @@ -178,7 +179,7 @@ namespace storm { this->updateWeightedPrecisionInImprovingPhase(env, separatingVector); this->performRefinementStep(env, std::move(separatingVector)); } - STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); + STORM_LOG_ERROR("Could not reach the desired precision: Termination requested or maximum number of refinement steps exceeded."); return result; }