fixed termination criteria and equipped interval value iteration methods with check whether the method converged for the relevant states

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -238,7 +238,7 @@ namespace storm {
                 storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
                 if (storm::solver::minimize(dirForParameters)) {
                     // Terminate if the value for ALL relevant states is already below the threshold
-                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), false);
                 } else {
                     // Terminate if the value for ALL relevant states is already above the threshold
                     termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);

src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

@@ -272,7 +272,7 @@ namespace storm {
                 storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
                 if (storm::solver::minimize(dirForParameters)) {
                     // Terminate if the value for ALL relevant states is already below the threshold
-                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), false);
                 } else {
                     // Terminate if the value for ALL relevant states is already above the threshold
                     termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -472,8 +472,10 @@ namespace storm {
                 }
 
                 // Determine whether the method converged.
-                if (storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion())) {
-                    status = Status::Converged;
+                if (this->hasRelevantValues()) {
+                    status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                } else {
+                    status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
                 }
                 
                 // Update environment variables.

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -445,7 +445,7 @@ namespace storm {
             bool converged = false;
             bool terminate = false;
             uint64_t iterations = 0;
-            bool doConvergenceCheck = false;
+            bool doConvergenceCheck = true;
             ValueType upperDiff;
             ValueType lowerDiff;
             ValueType precision = static_cast<ValueType>(this->getSettings().getPrecision());
@@ -514,7 +514,11 @@ namespace storm {
                     // Now check if the process already converged within our precision. Note that we double the target
                     // precision here. Doing so, we need to take the means of the lower and upper values later to guarantee
                     // the original precision.
-                    converged = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion());
+                    if (this->hasRelevantValues()) {
+                        converged = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion());
+                    } else {
+                        converged = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion());
+                    }
                     if (lowerStep) {
                         terminate |= this->terminateNow(*lowerX, SolverGuarantee::LessOrEqual);
                     }

src/storm/solver/SolveGoal.h

@@ -96,7 +96,11 @@ namespace storm {
             std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = factory.create(std::forward<MatrixType>(matrix));
             solver->setOptimizationDirection(goal.direction());
             if (goal.isBounded()) {
-                solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<ValueType>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize()));
+                if (goal.boundIsALowerBound()) {
+                    solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<ValueType>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), true));
+                } else {
+                    solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumBelowThreshold<ValueType>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), false));
+                }
             } else if (goal.hasRelevantValues()) {
                 solver->setRelevantValues(std::move(goal.relevantValues()));
             }

src/storm/solver/TerminationCondition.cpp

@@ -46,7 +46,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        TerminateIfFilteredExtremumBelowThreshold<ValueType>::TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
+        TerminateIfFilteredExtremumBelowThreshold<ValueType>::TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
             // Intentionally left empty.
         }
         

src/storm/solver/TerminationCondition.h

@@ -1,5 +1,4 @@
-#ifndef ALLOWEARLYTERMINATIONCONDITION_H
-#define	ALLOWEARLYTERMINATIONCONDITION_H
+#pragma once
 
 #include <vector>
 
@@ -50,7 +49,7 @@ namespace storm {
         template<typename ValueType>
         class TerminateIfFilteredExtremumBelowThreshold : public TerminateIfFilteredSumExceedsThreshold<ValueType>{
         public:
-            TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum);
+            TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum);
             
             bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
             
@@ -59,10 +58,3 @@ namespace storm {
         };
     }
 }
-
-
-
-
-
-#endif	/* ALLOWEARLYTERMINATIONCONDITION_H */
-

src/storm/utility/vector.h

@@ -846,6 +846,30 @@ namespace storm {
                 return true;
             }
             
+            /*!
+             * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided
+             * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value
+             * or in absolute terms.
+             *
+             * @param vectorLeft The first vector of the comparison.
+             * @param vectorRight The second vector of the comparison.
+             * @param precision The precision up to which the vectors are to be checked for equality.
+             * @param positions A vector representing a set of positions at which the vectors are compared.
+             * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
+             */
+            template<class T>
+            bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, storm::storage::BitVector const& positions, T const& precision, bool relativeError) {
+                STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
+                
+                for (auto position : positions) {
+                    if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
+                        return false;
+                    }
+                }
+                
+                return true;
+            }
+            
             /*!
              * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided
              * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value