diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 8c3ef0448..975d01f4a 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/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); diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index 95e73e82e..e80b0a101 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -29,6 +29,15 @@ namespace storm { return *terminationCondition; } + template + bool AbstractEquationSolver::terminateNow(std::vector const& values, SolverGuarantee const& guarantee) const { + if (!this->hasCustomTerminationCondition()) { + return false; + } + + return this->getTerminationCondition().terminateNow(values, guarantee); + } + template bool AbstractEquationSolver::hasLowerBound(BoundType const& type) const { if (type == BoundType::Any) { diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 09ced5229..6a55c34e1 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/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 const& getTerminationCondition() const; + bool terminateNow(std::vector const& values, SolverGuarantee const& guarantee) const; enum class BoundType { Global, @@ -110,6 +109,13 @@ namespace storm { void setBounds(std::vector const& lower, std::vector const& upper); protected: + /*! + * Retrieves the custom termination condition (if any was set). + * + * @return The custom termination condition. + */ + TerminationCondition const& getTerminationCondition() const; + void createUpperBoundsVector(std::unique_ptr>& upperBoundsVector, uint64_t length) const; void createLowerBoundsVector(std::vector& lowerBoundsVector) const; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index e0bc28db4..07db411d5 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/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(*this->cachedRowVector, x, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); + converged = storm::utility::vector::equalModuloPrecision(*this->cachedRowVector, x, static_cast(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* 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(*currentX, *nextX, static_cast(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(*currentX, *nextX, static_cast(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(), "Expected non-negative lower diff."); STORM_LOG_ASSERT(upperDiff >= storm::utility::zero(), "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(*lowerX, *upperX, storm::utility::convertNumber(2.0) * static_cast(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 + void NativeLinearEquationSolver::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 diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index d0c2ae410..75c334a91 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -76,6 +76,8 @@ namespace storm { virtual bool internalSolveEquations(std::vector& x, std::vector 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; diff --git a/src/storm/solver/SolverGuarantee.cpp b/src/storm/solver/SolverGuarantee.cpp new file mode 100644 index 000000000..53edbbf16 --- /dev/null +++ b/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; + } + + } +} diff --git a/src/storm/solver/TerminationCondition.cpp b/src/storm/solver/TerminationCondition.cpp index a30455564..0352c77e7 100644 --- a/src/storm/solver/TerminationCondition.cpp +++ b/src/storm/solver/TerminationCondition.cpp @@ -9,7 +9,7 @@ namespace storm { namespace solver { template - bool NoTerminationCondition::terminateNow(std::vector const& currentValues) const { + bool NoTerminationCondition::terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee) const { return false; } @@ -19,7 +19,11 @@ namespace storm { } template - bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector 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 - bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(std::vector 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 - bool TerminateIfFilteredExtremumBelowThreshold::terminateNow(std::vector const& currentValues) const { + bool TerminateIfFilteredExtremumBelowThreshold::terminateNow(std::vector 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; diff --git a/src/storm/solver/TerminationCondition.h b/src/storm/solver/TerminationCondition.h index ffa30d7f3..3e9be9b40 100644 --- a/src/storm/solver/TerminationCondition.h +++ b/src/storm/solver/TerminationCondition.h @@ -2,28 +2,30 @@ #define ALLOWEARLYTERMINATIONCONDITION_H #include -#include "storm/storage/BitVector.h" +#include "storm/solver/SolverGuarantee.h" +#include "storm/storage/BitVector.h" namespace storm { namespace solver { template class TerminationCondition { public: - virtual bool terminateNow(std::vector const& currentValues) const = 0; + virtual bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const = 0; }; template class NoTerminationCondition : public TerminationCondition { public: - bool terminateNow(std::vector const& currentValues) const; + bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const; }; template class TerminateIfFilteredSumExceedsThreshold : public TerminationCondition { public: TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict); - bool terminateNow(std::vector const& currentValues) const; + + bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const; protected: ValueType threshold; @@ -35,7 +37,8 @@ namespace storm { class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold{ public: TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum); - bool terminateNow(std::vector const& currentValue) const; + + bool terminateNow(std::vector const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const; protected: bool useMinimum; @@ -45,7 +48,8 @@ namespace storm { class TerminateIfFilteredExtremumBelowThreshold : public TerminateIfFilteredSumExceedsThreshold{ public: TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum); - bool terminateNow(std::vector const& currentValue) const; + + bool terminateNow(std::vector const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const; protected: bool useMinimum; diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 6a00b4cbf..be3809135 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -125,11 +125,6 @@ namespace storm { if (metaVariable.hasHigh()) { return Bdd(*this, internalDdManager.getBddEncodingLessOrEqualThan(static_cast(metaVariable.getHigh() - metaVariable.getLow()), metaVariable.getCube().getInternalBdd(), metaVariable.getNumberOfDdVariables()), {variable}); -// Bdd 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 result = this->getBddOne(); @@ -265,7 +260,7 @@ namespace storm { std::stringstream tmp1; std::vector 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>> variables(numberOfLayers); for (std::size_t i = 0; i < numberOfDdVariables; ++i) { std::vector> 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(*this, ddVariables[layer], {result[layer]})); }