fixed termination condition applications in a number of spots, fixed uint64 vs uint64_t issue

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -416,7 +416,7 @@ namespace storm {
                     cucNodes.push_back(nodeCUC);
                     builder.setPlaceLayoutInfo(nodeCUC, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter+5.0));
                     if (j > 0) {
-                        uint64 tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name());
+                        uint64_t tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name());
                         builder.setTransitionLayoutInfo(tclaim, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter));
                         builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim);
                         builder.addInputArc(considerNodes.back(), tclaim);

src/storm/solver/AbstractEquationSolver.cpp

@@ -29,6 +29,15 @@ namespace storm {
             return *terminationCondition;
         }
         
+        template<typename ValueType>
+        bool AbstractEquationSolver<ValueType>::terminateNow(std::vector<ValueType> const& values, SolverGuarantee const& guarantee) const {
+            if (!this->hasCustomTerminationCondition()) {
+                return false;
+            }
+            
+            return this->getTerminationCondition().terminateNow(values, guarantee);
+        }
+        
         template<typename ValueType>
         bool AbstractEquationSolver<ValueType>::hasLowerBound(BoundType const& type) const {
             if (type == BoundType::Any) {

src/storm/solver/AbstractEquationSolver.h

@@ -32,11 +32,10 @@ namespace storm {
             bool hasCustomTerminationCondition() const;
             
             /*!
-             * Retrieves the custom termination condition (if any was set).
-             * 
-             * @return The custom termination condition.
+             * Checks whether the solver can terminate wrt. to its termination condition. If no termination condition,
+             * this will yield false.
              */
-            TerminationCondition<ValueType> const& getTerminationCondition() const;
+            bool terminateNow(std::vector<ValueType> const& values, SolverGuarantee const& guarantee) const;
             
             enum class BoundType {
                 Global,
@@ -110,6 +109,13 @@ namespace storm {
             void setBounds(std::vector<ValueType> const& lower, std::vector<ValueType> const& upper);
             
         protected:
+            /*!
+             * Retrieves the custom termination condition (if any was set).
+             *
+             * @return The custom termination condition.
+             */
+            TerminationCondition<ValueType> const& getTerminationCondition() const;
+            
             void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const;
             void createLowerBoundsVector(std::vector<ValueType>& lowerBoundsVector) const;
 

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -159,14 +159,16 @@ namespace storm {
             }
             
             // Set up additional environment variables.
-            uint_fast64_t iterationCount = 0;
+            uint_fast64_t iterations = 0;
             bool converged = false;
+            bool terminate = false;
             
-            while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations()) {
+            while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 A->performSuccessiveOverRelaxationStep(omega, x, b);
                 
                 // Now check if the process already converged within our precision.
-                converged = storm::utility::vector::equalModuloPrecision<ValueType>(*this->cachedRowVector, x, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x));
+                converged = storm::utility::vector::equalModuloPrecision<ValueType>(*this->cachedRowVector, x, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
+                terminate = this->terminateNow(x, SolverGuarantee::None);
                 
                 // If we did not yet converge, we need to backup the contents of x.
                 if (!converged) {
@@ -174,18 +176,14 @@ namespace storm {
                 }
                 
                 // Increase iteration count so we can abort if convergence is too slow.
-                ++iterationCount;
+                ++iterations;
             }
             
             if (!this->isCachingEnabled()) {
                 clearCache();
             }
             
-            if (converged) {
-                STORM_LOG_INFO("Iterative solver converged in " << iterationCount << " iterations.");
-            } else {
-                STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations.");
-            }
+            this->logIterations(converged, terminate, iterations);
             
             return converged;
         }
@@ -209,10 +207,11 @@ namespace storm {
             std::vector<ValueType>* nextX = this->cachedRowVector.get();
             
             // Set up additional environment variables.
-            uint_fast64_t iterationCount = 0;
+            uint_fast64_t iterations = 0;
             bool converged = false;
+            bool terminate = false;
 
-            while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
+            while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Compute D^-1 * (b - LU * x) and store result in nextX.
                 multiplier.multAdd(jacobiLU, *currentX, nullptr, *nextX);
 
@@ -221,12 +220,13 @@ namespace storm {
                 
                 // Now check if the process already converged within our precision.
                 converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
+                terminate = this->terminateNow(*currentX, SolverGuarantee::None);
                 
                 // Swap the two pointers as a preparation for the next iteration.
                 std::swap(nextX, currentX);
                 
                 // Increase iteration count so we can abort if convergence is too slow.
-                ++iterationCount;
+                ++iterations;
             }
             
             // If the last iteration did not write to the original x we have to swap the contents, because the
@@ -239,12 +239,8 @@ namespace storm {
                 clearCache();
             }
             
-            if (converged) {
-                STORM_LOG_INFO("Iterative solver converged in " << iterationCount << " iterations.");
-            } else {
-                STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations.");
-            }
-            
+            this->logIterations(converged, terminate, iterations);
+
             return converged;
         }
         
@@ -396,8 +392,9 @@ namespace storm {
             bool useGaussSeidelMultiplication = this->getSettings().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel;
             
             bool converged = false;
+            bool terminate = this->terminateNow(*currentX, SolverGuarantee::GreaterOrEqual);
             uint64_t iterations = 0;
-            while (!converged && iterations < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
+            while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 if (useGaussSeidelMultiplication) {
                     *nextX = *currentX;
                     this->multiplier.multAddGaussSeidelBackward(*this->A, *nextX, &b);
@@ -405,8 +402,9 @@ namespace storm {
                     this->multiplier.multAdd(*this->A, *currentX, &b, *nextX);
                 }
                 
-                // Now check if the process already converged within our precision.
+                // Now check for termination.
                 converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
+                terminate = this->terminateNow(*currentX, SolverGuarantee::GreaterOrEqual);
                 
                 // Set up next iteration.
                 std::swap(currentX, nextX);
@@ -421,11 +419,7 @@ namespace storm {
                 clearCache();
             }
             
-            if (converged) {
-                STORM_LOG_INFO("Iterative solver converged in " << iterations << " iterations.");
-            } else {
-                STORM_LOG_WARN("Iterative solver did not converge in " << iterations << " iterations.");
-            }
+            this->logIterations(converged, terminate, iterations);
 
             return converged;
         }
@@ -449,13 +443,20 @@ namespace storm {
             }
             
             bool converged = false;
+            bool terminate = false;
             uint64_t iterations = 0;
             bool doConvergenceCheck = false;
             ValueType upperDiff;
             ValueType lowerDiff;
-            while (!converged && iterations < this->getSettings().getMaximalNumberOfIterations()) {
+            while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
+                // Remember in which directions we took steps in this iteration.
+                bool lowerStep = false;
+                bool upperStep = false;
+                
                 // In every thousandth iteration, we improve both bounds.
                 if (iterations % 1000 == 0) {
+                    lowerStep = true;
+                    upperStep = true;
                     if (useGaussSeidelMultiplication) {
                         lowerDiff = (*lowerX)[0];
                         this->multiplier.multAddGaussSeidelBackward(*this->A, *lowerX, &b);
@@ -478,26 +479,30 @@ namespace storm {
                             lowerDiff = (*lowerX)[0];
                             this->multiplier.multAddGaussSeidelBackward(*this->A, *lowerX, &b);
                             lowerDiff = (*lowerX)[0] - lowerDiff;
+                            lowerStep = true;
                         } else {
                             upperDiff = (*upperX)[0];
                             this->multiplier.multAddGaussSeidelBackward(*this->A, *upperX, &b);
                             upperDiff = upperDiff - (*upperX)[0];
+                            upperStep = true;
                         }
                     } else {
                         if (lowerDiff >= upperDiff) {
                             this->multiplier.multAdd(*this->A, *lowerX, &b, *tmp);
                             lowerDiff = (*tmp)[0] - (*lowerX)[0];
                             std::swap(tmp, lowerX);
+                            lowerStep = true;
                         } else {
                             this->multiplier.multAdd(*this->A, *upperX, &b, *tmp);
                             upperDiff = (*upperX)[0] - (*tmp)[0];
                             std::swap(tmp, upperX);
+                            upperStep = true;
                         }
                     }
                 }
                 STORM_LOG_ASSERT(lowerDiff >= storm::utility::zero<ValueType>(), "Expected non-negative lower diff.");
                 STORM_LOG_ASSERT(upperDiff >= storm::utility::zero<ValueType>(), "Expected non-negative upper diff.");
-                if (iterations % 100 == 0) {
+                if (iterations % 1000 == 0) {
                     STORM_LOG_TRACE("Iteration " << iterations << ": lower difference: " << lowerDiff << ", upper difference: " << upperDiff << ".");
                 }
                 
@@ -506,6 +511,12 @@ namespace storm {
                     // 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, storm::utility::convertNumber<ValueType>(2.0) * static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
+                    if (lowerStep) {
+                        terminate |= this->terminateNow(*lowerX, SolverGuarantee::GreaterOrEqual);
+                    }
+                    if (upperStep) {
+                        terminate |= this->terminateNow(*upperX, SolverGuarantee::GreaterOrEqual);
+                    }
                 }
                 
                 // Set up next iteration.
@@ -527,13 +538,20 @@ namespace storm {
                 clearCache();
             }
             
+            this->logIterations(converged, terminate, iterations);
+
+            return converged;
+        }
+        
+        template<typename ValueType>
+        void NativeLinearEquationSolver<ValueType>::logIterations(bool converged, bool terminate, uint64_t iterations) const {
             if (converged) {
                 STORM_LOG_INFO("Iterative solver converged in " << iterations << " iterations.");
+            } else if (terminate) {
+                STORM_LOG_INFO("Iterative solver terminated after " << iterations << " iterations.");
             } else {
                 STORM_LOG_WARN("Iterative solver did not converge in " << iterations << " iterations.");
             }
-            
-            return converged;
         }
         
         template<typename ValueType>

src/storm/solver/NativeLinearEquationSolver.h

@@ -76,6 +76,8 @@ namespace storm {
             virtual bool internalSolveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
             
         private:
+            void logIterations(bool converged, bool terminate, uint64_t iterations) const;
+            
             virtual uint64_t getMatrixRowCount() const override;
             virtual uint64_t getMatrixColumnCount() const override;
 

src/storm/solver/SolverGuarantee.cpp

@@ -0,0 +1,16 @@
+#include "storm/solver/SolverGuarantee.h"
+
+namespace storm {
+    namespace solver {
+        
+        std::ostream& operator<<(std::ostream& out, SolverGuarantee const& guarantee) {
+            switch (guarantee) {
+                case SolverGuarantee::GreaterOrEqual: out << "greater-or-equal";  break;
+                case SolverGuarantee::LessOrEqual: out << "greater-or-equal";  break;
+                case SolverGuarantee::None: out << "none";  break;
+            }
+            return out;
+        }
+        
+    }
+}

src/storm/solver/TerminationCondition.cpp

@@ -9,7 +9,7 @@ namespace storm {
     namespace solver {
         
         template<typename ValueType>
-        bool NoTerminationCondition<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const {
+        bool NoTerminationCondition<ValueType>::terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee) const {
             return false;
         }
         
@@ -19,7 +19,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool TerminateIfFilteredSumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const {
+        bool TerminateIfFilteredSumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee) const {
+            if (guarantee != SolverGuarantee::GreaterOrEqual) {
+                return false;
+            }
+            
             STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch.");
             ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter);
             return strict ? currentThreshold > this->threshold : currentThreshold >= this->threshold;
@@ -31,7 +35,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const {
+        bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee) const {
+            if (guarantee != SolverGuarantee::GreaterOrEqual) {
+                return false;
+            }
+            
             STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch.");
             ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter);
             return this->strict ? currentValue > this->threshold : currentValue >= this->threshold;
@@ -43,7 +51,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool TerminateIfFilteredExtremumBelowThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const {
+        bool TerminateIfFilteredExtremumBelowThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee) const {
+            if (guarantee != SolverGuarantee::LessOrEqual) {
+                return false;
+            }
+            
             STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch.");
             ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter);
             return this->strict ? currentValue < this->threshold : currentValue <= this->threshold;

src/storm/solver/TerminationCondition.h

@@ -2,28 +2,30 @@
 #define	ALLOWEARLYTERMINATIONCONDITION_H
 
 #include <vector>
-#include "storm/storage/BitVector.h"
 
+#include "storm/solver/SolverGuarantee.h"
+#include "storm/storage/BitVector.h"
 
 namespace storm {
     namespace solver {
         template<typename ValueType>
         class TerminationCondition {
         public:
-            virtual bool terminateNow(std::vector<ValueType> const& currentValues) const = 0;
+            virtual bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const = 0;
         };
         
         template<typename ValueType>
         class NoTerminationCondition : public TerminationCondition<ValueType> {
         public:
-            bool terminateNow(std::vector<ValueType> const& currentValues) const;
+            bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
         };
         
         template<typename ValueType>
         class TerminateIfFilteredSumExceedsThreshold : public TerminationCondition<ValueType> {
         public:
             TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict);
-            bool terminateNow(std::vector<ValueType> const& currentValues) const;
+            
+            bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
             
         protected:
             ValueType threshold;
@@ -35,7 +37,8 @@ namespace storm {
         class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold<ValueType>{
         public:
             TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum);
-            bool terminateNow(std::vector<ValueType> const& currentValue) const;
+            
+            bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
             
         protected:
             bool useMinimum;
@@ -45,7 +48,8 @@ namespace storm {
         class TerminateIfFilteredExtremumBelowThreshold : public TerminateIfFilteredSumExceedsThreshold<ValueType>{
         public:
             TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum);
-            bool terminateNow(std::vector<ValueType> const& currentValue) const;
+            
+            bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
             
         protected:
             bool useMinimum;

src/storm/storage/dd/DdManager.cpp

@@ -125,11 +125,6 @@ namespace storm {
 
             if (metaVariable.hasHigh()) {
                 return Bdd<LibraryType>(*this, internalDdManager.getBddEncodingLessOrEqualThan(static_cast<uint64_t>(metaVariable.getHigh() - metaVariable.getLow()), metaVariable.getCube().getInternalBdd(), metaVariable.getNumberOfDdVariables()), {variable});
-//                Bdd<LibraryType> result = this->getBddZero();
-//                for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-//                    result |= this->getEncoding(variable, value);
-//                }
-//                return result;
             } else {
                 // If there is no upper bound on this variable, the whole range is valid.
                 Bdd<LibraryType> result = this->getBddOne();
@@ -265,7 +260,7 @@ namespace storm {
             
             std::stringstream tmp1;
             std::vector<storm::expressions::Variable> result;
-            for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
+            for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
                 if (type == MetaVariableType::Int) {
                     result.emplace_back(manager->declareIntegerVariable(name + tmp1.str()));
                 } else if (type == MetaVariableType::Bool) {
@@ -279,7 +274,7 @@ namespace storm {
             std::vector<std::vector<Bdd<LibraryType>>> variables(numberOfLayers);
             for (std::size_t i = 0; i < numberOfDdVariables; ++i) {
                 std::vector<InternalBdd<LibraryType>> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level);
-                for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
+                for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
                     variables[layer].emplace_back(Bdd<LibraryType>(*this, ddVariables[layer], {result[layer]}));
                 }