From d8d3404b87ec561bc9a536906d8fcdfee6da02b1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Sep 2017 16:07:05 +0200 Subject: [PATCH] fixed termination criteria and equipped interval value iteration methods with check whether the method converged for the relevant states --- ...SparseDtmcParameterLiftingModelChecker.cpp | 2 +- .../SparseMdpParameterLiftingModelChecker.cpp | 2 +- .../IterativeMinMaxLinearEquationSolver.cpp | 6 +++-- .../solver/NativeLinearEquationSolver.cpp | 8 +++++-- src/storm/solver/SolveGoal.h | 6 ++++- src/storm/solver/TerminationCondition.cpp | 2 +- src/storm/solver/TerminationCondition.h | 12 ++-------- src/storm/utility/vector.h | 24 +++++++++++++++++++ 8 files changed, 44 insertions(+), 18 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 41a92d433..119e3791d 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); + termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), false); } else { // Terminate if the value for ALL relevant states is already above the threshold termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 65e16d628..19ac39b62 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); + termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), false); } else { // Terminate if the value for ALL relevant states is already above the threshold termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 78d7f033b..fba6865ee 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -472,8 +472,10 @@ namespace storm { } // Determine whether the method converged. - if (storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion())) { - status = Status::Converged; + if (this->hasRelevantValues()) { + status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status; + } else { + status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status; } // Update environment variables. diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 7d46584d7..5b4a2172d 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/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(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(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()); + if (this->hasRelevantValues()) { + converged = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()); + } else { + converged = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()); + } if (lowerStep) { terminate |= this->terminateNow(*lowerX, SolverGuarantee::LessOrEqual); } diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h index c6f95151d..cd058b656 100644 --- a/src/storm/solver/SolveGoal.h +++ b/src/storm/solver/SolveGoal.h @@ -96,7 +96,11 @@ namespace storm { std::unique_ptr> solver = factory.create(std::forward(matrix)); solver->setOptimizationDirection(goal.direction()); if (goal.isBounded()) { - solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); + if (goal.boundIsALowerBound()) { + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), true)); + } else { + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), false)); + } } else if (goal.hasRelevantValues()) { solver->setRelevantValues(std::move(goal.relevantValues())); } diff --git a/src/storm/solver/TerminationCondition.cpp b/src/storm/solver/TerminationCondition.cpp index fbacfbe56..e074eaaa2 100644 --- a/src/storm/solver/TerminationCondition.cpp +++ b/src/storm/solver/TerminationCondition.cpp @@ -46,7 +46,7 @@ namespace storm { } template - TerminateIfFilteredExtremumBelowThreshold::TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold(filter, threshold, strict), useMinimum(useMinimum) { + TerminateIfFilteredExtremumBelowThreshold::TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold(filter, threshold, strict), useMinimum(useMinimum) { // Intentionally left empty. } diff --git a/src/storm/solver/TerminationCondition.h b/src/storm/solver/TerminationCondition.h index 529618443..7c364989c 100644 --- a/src/storm/solver/TerminationCondition.h +++ b/src/storm/solver/TerminationCondition.h @@ -1,5 +1,4 @@ -#ifndef ALLOWEARLYTERMINATIONCONDITION_H -#define ALLOWEARLYTERMINATIONCONDITION_H +#pragma once #include @@ -50,7 +49,7 @@ namespace storm { template class TerminateIfFilteredExtremumBelowThreshold : public TerminateIfFilteredSumExceedsThreshold{ 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 const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const; @@ -59,10 +58,3 @@ namespace storm { }; } } - - - - - -#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ - diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 17a9d1295..ff60d5946 100644 --- a/src/storm/utility/vector.h +++ b/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 + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector 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