Pcaa: Implemented termination signal.

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 <class SparseModelType, typename GeometryValueType>
             bool SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::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;
             }
 

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<GeometryValueType>());
                     direction[objIndex] = storm::utility::one<GeometryValueType>();
                     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<storm::storage::geometry::Halfspace<GeometryValueType>> underApproxHalfspaces = this->underApproximation->getHalfspaces();
                     std::vector<Point> 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::models::sparse::Mdp<double>, storm::RationalNumber>;
             template class SparsePcaaParetoQuery<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;

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<GeometryValueType>();
-                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<typename SparseModelType::ValueType>(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;
             }