From bdcd4b26a3013b9916a653f4e7b40c48d783aa52 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Feb 2016 17:28:59 +0100 Subject: [PATCH] refactoring early termination and solve goals and bounds Former-commit-id: 123835f655dc4a20b38ecf65e6b0b0bce0adba48 --- src/logic/Bound.h | 32 +++++++++ src/logic/BoundInfo.h | 19 ----- src/logic/ExpectedTimeOperatorFormula.cpp | 12 ++-- src/logic/ExpectedTimeOperatorFormula.h | 6 +- src/logic/LongRunAverageOperatorFormula.cpp | 12 ++-- src/logic/LongRunAverageOperatorFormula.h | 6 +- src/logic/OperatorFormula.cpp | 24 ++++--- src/logic/OperatorFormula.h | 19 ++--- src/logic/ProbabilityOperatorFormula.cpp | 12 ++-- src/logic/ProbabilityOperatorFormula.h | 6 +- src/logic/RewardOperatorFormula.cpp | 12 ++-- src/logic/RewardOperatorFormula.h | 6 +- src/modelchecker/AbstractModelChecker.cpp | 8 +-- src/modelchecker/CheckTask.h | 25 ++++--- .../prctl/SparseMdpPrctlModelChecker.h | 2 - src/solver/AbstractEquationSolver.h | 53 ++++++++++++++ src/solver/AllowEarlyTerminationCondition.cpp | 48 ------------- src/solver/AllowEarlyTerminationCondition.h | 52 -------------- src/solver/LinearEquationSolver.h | 18 ++--- src/solver/MinMaxLinearEquationSolver.h | 48 ++++++------- src/solver/SolveGoal.cpp | 24 +++---- src/solver/SolveGoal.h | 19 +++-- src/solver/TerminationCondition.cpp | 41 +++++++++++ src/solver/TerminationCondition.h | 53 ++++++++++++++ src/utility/vector.h | 71 +++++++++++-------- 25 files changed, 346 insertions(+), 282 deletions(-) create mode 100644 src/logic/Bound.h delete mode 100644 src/logic/BoundInfo.h create mode 100644 src/solver/AbstractEquationSolver.h delete mode 100644 src/solver/AllowEarlyTerminationCondition.cpp delete mode 100644 src/solver/AllowEarlyTerminationCondition.h create mode 100644 src/solver/TerminationCondition.cpp create mode 100644 src/solver/TerminationCondition.h diff --git a/src/logic/Bound.h b/src/logic/Bound.h new file mode 100644 index 000000000..58f8b5448 --- /dev/null +++ b/src/logic/Bound.h @@ -0,0 +1,32 @@ +#ifndef STORM_LOGIC_BOUND_H_ +#define STORM_LOGIC_BOUND_H_ + +#include "src/logic/ComparisonType.h" + +namespace storm { + namespace logic { + template + struct Bound { + Bound(ComparisonType comparisonType, ValueType const& threshold) : comparisonType(comparisonType), threshold(threshold) { + // Intentionally left empty. + } + + ComparisonType comparisonType; + ValueType threshold; + + friend std::ostream& operator<<(std::ostream& out, Bound const& bound); + }; + + template + std::ostream& operator<<(std::ostream& out, Bound const& bound) { + out << bound.comparisonType << bound.threshold; + return out; + } + } + + template + using Bound = typename logic::Bound; +} + +#endif /* STORM_LOGIC_BOUND_H_ */ + diff --git a/src/logic/BoundInfo.h b/src/logic/BoundInfo.h deleted file mode 100644 index 453d9eb08..000000000 --- a/src/logic/BoundInfo.h +++ /dev/null @@ -1,19 +0,0 @@ - -#ifndef BOUNDINFO_H -#define BOUNDINFO_H - -#include "ComparisonType.h" - - -namespace storm { - namespace logic { - template - struct BoundInfo { - BT bound; - ComparisonType boundType; - }; - } -} - -#endif /* BOUNDINFO_H */ - diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index 98ed6d8cc..ed21be228 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ExpectedTimeOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index b9b6d57ee..5702610c2 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ExpectedTimeOperatorFormula : public OperatorFormula { public: ExpectedTimeOperatorFormula(std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ExpectedTimeOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index d72317b7d..cfeb30692 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr LongRunAverageOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 161823314..89e119f48 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class LongRunAverageOperatorFormula : public OperatorFormula { public: LongRunAverageOperatorFormula(std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~LongRunAverageOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 768b6b3d0..a9cdc09ae 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { + OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) { // Intentionally left empty. } @@ -11,19 +11,27 @@ namespace storm { } ComparisonType OperatorFormula::getComparisonType() const { - return comparisonType.get(); + return bound.get().comparisonType; } - void OperatorFormula::setComparisonType(ComparisonType t) { - comparisonType = boost::optional(t); + void OperatorFormula::setComparisonType(ComparisonType newComparisonType) { + bound.get().comparisonType = newComparisonType; } - double OperatorFormula::getBound() const { + double OperatorFormula::getThreshold() const { + return bound.get().threshold; + } + + void OperatorFormula::setThreshold(double newThreshold) { + bound.get().threshold = newThreshold; + } + + Bound const& OperatorFormula::getBound() const { return bound.get(); } - void OperatorFormula::setBound(double b) { - bound = boost::optional(b); + void OperatorFormula::setBound(Bound const& newBound) { + bound = newBound; } bool OperatorFormula::hasOptimalityType() const { @@ -43,7 +51,7 @@ namespace storm { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); } if (hasBound()) { - out << getComparisonType() << getBound(); + out << getBound(); } else { out << "=?"; } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 5c120bf2f..7660799a4 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -4,14 +4,14 @@ #include #include "src/logic/UnaryStateFormula.h" +#include "src/logic/Bound.h" #include "src/solver/OptimizationDirection.h" -#include "src/logic/ComparisonType.h" namespace storm { namespace logic { class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~OperatorFormula() { // Intentionally left empty. @@ -19,20 +19,21 @@ namespace storm { bool hasBound() const; ComparisonType getComparisonType() const; - void setComparisonType(ComparisonType); - double getBound() const; - void setBound(double); + void setComparisonType(ComparisonType newComparisonType); + double getThreshold() const; + void setThreshold(double newThreshold); + Bound const& getBound() const; + void setBound(Bound const& newBound); bool hasOptimalityType() const; - OptimizationDirection const& getOptimalityType() const; + storm::solver::OptimizationDirection const& getOptimalityType() const; virtual bool isOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; protected: std::string operatorSymbol; - boost::optional comparisonType; - boost::optional bound; - boost::optional optimalityType; + boost::optional> bound; + boost::optional optimalityType; }; } } diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index e6cde140d..1f4615556 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -42,12 +42,12 @@ namespace storm { return this->getSubformula().containsProbabilityOperator(); } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ProbabilityOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 7f30dd92d..8bae11548 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ProbabilityOperatorFormula : public OperatorFormula { public: ProbabilityOperatorFormula(std::shared_ptr const& subformula); - ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 627263d36..791d1f5cc 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -55,12 +55,12 @@ namespace storm { this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula), rewardModelName(rewardModelName) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) { // Intentionally left empty. } std::shared_ptr RewardOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->rewardModelName, this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 37287c6e8..9e90ef01f 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -9,10 +9,10 @@ namespace storm { class RewardOperatorFormula : public OperatorFormula { public: RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~RewardOperatorFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 764b02427..3b0d55ebf 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -175,7 +175,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold()); } else { return result; } @@ -189,7 +189,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -203,7 +203,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -217,7 +217,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index 959c8f96a..a3646e464 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -41,7 +41,7 @@ namespace storm { if (operatorFormula.hasBound()) { if (onlyInitialStatesRelevant) { - this->bound = std::make_pair(operatorFormula.getComparisonType(), static_cast(operatorFormula.getBound())); + this->bound = operatorFormula.getBound(); } if (!optimizationDirection) { @@ -54,7 +54,7 @@ namespace storm { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); if (probabilityOperatorFormula.hasBound()) { - if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { + if (probabilityOperatorFormula.getThreshold() == storm::utility::zero() || probabilityOperatorFormula.getThreshold() == storm::utility::one()) { this->qualitative = true; } } @@ -63,7 +63,7 @@ namespace storm { this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); if (rewardOperatorFormula.hasBound()) { - if (rewardOperatorFormula.getBound() == storm::utility::zero()) { + if (rewardOperatorFormula.getThreshold() == storm::utility::zero()) { this->qualitative = true; } } @@ -139,21 +139,21 @@ namespace storm { /*! * Retrieves the value of the bound (if set). */ - ValueType const& getBoundValue() const { - return bound.get().second; + ValueType const& getBoundThreshold() const { + return bound.get().threshold; } /*! * Retrieves the comparison type of the bound (if set). */ storm::logic::ComparisonType const& getBoundComparisonType() const { - return bound.get().first; + return bound.get().comparisonType; } /*! - * Retrieves the bound for the initial states (if set). + * Retrieves the bound (if set). */ - std::pair const& getBound() const { + storm::logic::Bound const& getBound() const { return bound.get(); } @@ -181,14 +181,13 @@ namespace storm { * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values * for the initial states. - * @param initialStatesBound The bound with which the initial states will be compared. This may only be set - * together with the flag that indicates only initial states of the model are relevant. + * @param bound The bound with which the states will be compared. * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared * with bounds 0/1. * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } @@ -204,8 +203,8 @@ namespace storm { // If set to true, the model checker may decide to only compute the values for the initial states. bool onlyInitialStatesRelevant; - // The bound with which the initial states will be compared. - boost::optional> bound; + // The bound with which the states will be compared. + boost::optional> bound; // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 340b5f33a..1a0d85b2c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,8 +4,6 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/Mdp.h" #include "src/utility/solver.h" -#include "src/logic/BoundInfo.h" -#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace modelchecker { diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h new file mode 100644 index 000000000..e110318f6 --- /dev/null +++ b/src/solver/AbstractEquationSolver.h @@ -0,0 +1,53 @@ +#ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ +#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ + +#include "src/solver/TerminationCondition.h" + +namespace storm { + namespace solver { + + template + class AbstractEquationSolver { + public: + /*! + * Sets a custom termination condition that is used together with the regular termination condition of the + * solver. + * + * @param terminationCondition An object that can be queried whether to terminate early or not. + */ + void setTerminationCondition(std::unique_ptr> terminationCondition) { + this->terminationCondition = std::move(terminationCondition); + } + + /*! + * Removes a previously set custom termination condition. + */ + void resetTerminationCondition() { + this->terminationCondition = nullptr; + } + + /*! + * Retrieves whether a custom termination condition has been set. + */ + bool hasCustomTerminationCondition() { + return static_cast(this->terminationCondition); + } + + /*! + * Retrieves the custom termination condition (if any was set). + * + * @return The custom termination condition. + */ + TerminationCondition const& getTerminationCondition() const { + return *terminationCondition; + } + + protected: + // A termination condition to be used (can be unset). + std::unique_ptr> terminationCondition; + }; + + } +} + +#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ \ No newline at end of file diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp deleted file mode 100644 index 2236c7c78..000000000 --- a/src/solver/AllowEarlyTerminationCondition.cpp +++ /dev/null @@ -1,48 +0,0 @@ -#include "AllowEarlyTerminationCondition.h" -#include "src/utility/vector.h" - -namespace storm { - namespace solver { - - template - TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold) : - terminationThreshold(threshold), filter(filter) - { - // Intentionally left empty. - } - - template - bool TerminateAfterFilteredSumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { - assert(currentValues.size() >= filter.size()); - ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); - - return currentThreshold >= this->terminationThreshold; - - - } - - template - TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum) : - terminationThreshold(threshold), filter(filter), useMinimumAsExtremum(useMinimum) - { - // Intentionally left empty. - } - - template - bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { - assert(currentValues.size() >= filter.size()); - - ValueType initVal = terminationThreshold - 1; - ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); - - return currentThreshold >= this->terminationThreshold; - - - } - - - template class TerminateAfterFilteredExtremumPassesThresholdValue; - template class TerminateAfterFilteredSumPassesThresholdValue; - - } -} diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h deleted file mode 100644 index be9084c70..000000000 --- a/src/solver/AllowEarlyTerminationCondition.h +++ /dev/null @@ -1,52 +0,0 @@ -#ifndef ALLOWEARLYTERMINATIONCONDITION_H -#define ALLOWEARLYTERMINATIONCONDITION_H - -#include -#include "src/storage/BitVector.h" - - -namespace storm { - namespace solver { - template - class AllowEarlyTerminationCondition { - public: - virtual bool terminateNow(std::vector const& currentValues) const = 0; - }; - - template - class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition { - public: - bool terminateNow(std::vector const& currentValues) const { return false; } - }; - - template - class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition { - public: - TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold); - bool terminateNow(std::vector const& currentValues) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - }; - - template - class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ - public: - TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum); - bool terminateNow(std::vector const& currentValue) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - bool useMinimumAsExtremum; - }; - } -} - - - - - -#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ - diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 512cefbdb..e85fe3cce 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -3,8 +3,9 @@ #include +#include "src/solver/AbstractEquationSolver.h" + #include "src/storage/SparseMatrix.h" -#include "src/solver/AllowEarlyTerminationCondition.h" namespace storm { namespace solver { @@ -13,8 +14,8 @@ namespace storm { * An interface that represents an abstract linear equation solver. In addition to solving a system of linear * equations, the functionality to repeatedly multiply a matrix with a given vector is provided. */ - template - class LinearEquationSolver { + template + class LinearEquationSolver : public AbstractEquationSolver { public: virtual ~LinearEquationSolver() { // Intentionally left empty. @@ -30,7 +31,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -44,14 +45,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; - - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - - // A termination criterion to be used (can be unset). - std::unique_ptr> earlyTermination; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; } // namespace solver diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index cf334c6ee..42963ac29 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -4,11 +4,15 @@ #include #include #include -#include "SolverSelectionOptions.h" + +#include "src/solver/AbstractEquationSolver.h" +#include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "src/solver/AllowEarlyTerminationCondition.h" +#include "src/storage/Scheduler.h" #include "src/solver/OptimizationDirection.h" +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace storage { template class SparseMatrix; @@ -17,15 +21,16 @@ namespace storm { namespace solver { /** - * Abstract base class which provides value-type independent helpers. + * Abstract base class of min-max linea equation solvers. */ - class AbstractMinMaxLinearEquationSolver { + template + class AbstractMinMaxLinearEquationSolver : public AbstractEquationSolver { public: void setSchedulerTracking(bool trackScheduler = true); std::vector getScheduler() const { - STORM_LOG_THROW(scheduler, storm::exceptions::Invali, "Cannot retrieve scheduler, because none was generated."); - reutrn scheduler.get(); + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return scheduler.get(); } void setOptimizationDirection(OptimizationDirection d) { @@ -35,37 +40,30 @@ namespace storm { void resetOptimizationDirection() { direction = OptimizationDirectionSetting::Unset; } - - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - + protected: AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech); - /// The direction in which to optimize, can be unset. + // The direction in which to optimize, can be unset. OptimizationDirectionSetting direction; - /// The required precision for the iterative methods. + // The required precision for the iterative methods. double precision; - /// Sets whether the relative or absolute error is to be considered for convergence detection. + // Sets whether the relative or absolute error is to be considered for convergence detection. bool relative; - /// The maximal number of iterations to do before iteration is aborted. + // The maximal number of iterations to do before iteration is aborted. uint_fast64_t maximalNumberOfIterations; - /// Whether value iteration or policy iteration is to be used. + // Whether value iteration or policy iteration is to be used. bool useValueIteration; - /// Whether we generate a scheduler during solving. + // Whether we generate a scheduler during solving. bool trackScheduler; - /// The scheduler (if it could be successfully generated). - boost::optional scheduler; - - // A termination criterion to be used (can be unset). - std::unique_ptr> earlyTermination; + // The scheduler (if it could be successfully generated). + boost::optional> scheduler; }; /*! @@ -74,11 +72,9 @@ namespace storm { * provided. */ template - class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { + class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { protected: - MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : - AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), - A(matrix), earlyTermination(new NoEarlyTerminationCondition()) { + MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), A(matrix) { // Intentionally left empty. } diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index 4994f8ade..b135fba59 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -14,33 +14,33 @@ namespace storm { namespace solver { template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { std::unique_ptr> p = factory.create(matrix); p->setOptimizationDirection(goal.direction()); - p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); + p->setTerminationCondition(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); return p; } template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { if (goal.isBounded()) { return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); } - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - return p; + std::unique_ptr> solver = factory.create(matrix); + solver->setOptimizationDirection(goal.direction()); + return solver; } template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); - return p; + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> solver = factory.create(matrix); + solver->setOptimizationDirection(goal.direction()); + solver->setTerminationCondition(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); + return solver; } template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { if (goal.isBounded()) { return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index 7a8f9c661..b87fa0837 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -5,7 +5,7 @@ #include "src/solver/OptimizationDirection.h" #include "src/logic/ComparisonType.h" -#include "src/logic/BoundInfo.h" +#include "src/logic/Bound.h" #include "src/storage/BitVector.h" namespace storm { @@ -57,11 +57,11 @@ namespace storm { template class BoundedGoal : public SolveGoal { public: - BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType ct, ValueType const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(optimizationDirection), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) { + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType comparisonType, ValueType const& threshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(comparisonType, threshold), relevantValueVector(relevantValues) { // Intentionally left empty. } - BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::BoundInfo const& boundInfo, storm::storage::BitVector const& relevantColumns) : SolveGoal(optimizationDirection), boundType(boundInfo.boundType), threshold(boundInfo.bound), relevantColumnVector(relevantColumns) { + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::Bound const& bound, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(bound), relevantValueVector(relevantValues) { // Intentionally left empty. } @@ -74,21 +74,20 @@ namespace storm { } bool boundIsALowerBound() const { - return (boundType == storm::logic::ComparisonType::Greater || boundType == storm::logic::ComparisonType::GreaterEqual); + return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual); } ValueType const& thresholdValue() const { - return threshold; + return bound.threshold; } - storm::storage::BitVector const& relevantColumns() const { - return relevantColumnVector; + storm::storage::BitVector const& relevantValues() const { + return relevantValues; } private: - storm::logic::ComparisonType boundType; - ValueType threshold; - storm::storage::BitVector relevantColumnVector; + Bound bound; + storm::storage::BitVector relevantValueVector; }; template diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp new file mode 100644 index 000000000..98434e407 --- /dev/null +++ b/src/solver/TerminationCondition.cpp @@ -0,0 +1,41 @@ +#include "src/solver/TerminationCondition.h" +#include "src/utility/vector.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace solver { + + template + bool NoTerminationCondition::terminateNow(std::vector const& currentValues) const { + return false; + } + + template + TerminateIfFilteredSumExceedsThreshold::TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict) : threshold(threshold), filter(filter), strict(strict) { + // Intentionally left empty. + } + + template + bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + 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; + } + + template + TerminateIfFilteredExtremumExceedsThreshold::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold(filter, threshold, strict), useMinimum(useMinimum) { + // Intentionally left empty. + } + + template + bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(const std::vector& currentValues) const { + STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); + ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, filter) : storm::utility::vector::max_if(currentValues, filter); + return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; + } + + template class TerminateIfFilteredSumExceedsThreshold; + template class TerminateIfFilteredExtremumExceedsThreshold; + } +} diff --git a/src/solver/TerminationCondition.h b/src/solver/TerminationCondition.h new file mode 100644 index 000000000..4ea5f5c3d --- /dev/null +++ b/src/solver/TerminationCondition.h @@ -0,0 +1,53 @@ +#ifndef ALLOWEARLYTERMINATIONCONDITION_H +#define ALLOWEARLYTERMINATIONCONDITION_H + +#include +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template + class TerminationCondition { + public: + virtual bool terminateNow(std::vector const& currentValues) const = 0; + }; + + template + class NoTerminationCondition : public TerminationCondition { + public: + bool terminateNow(std::vector const& currentValues) 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; + + protected: + ValueType threshold; + storm::storage::BitVector filter; + bool strict; + }; + + template + class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold{ + public: + TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum); + bool terminateNow(std::vector const& currentValue) const; + + protected: + ValueType threshold; + storm::storage::BitVector filter; + bool useMinimum; + }; + } +} + + + + + +#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ + diff --git a/src/utility/vector.h b/src/utility/vector.h index 665569645..31b1a5493 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -388,55 +388,64 @@ namespace storm { */ template VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { - assert(values.size() >= filter.size()); + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); VT sum = storm::utility::zero(); - for(uint_fast64_t i : filter) { - sum += values[i]; + for(auto pos : filter) { + sum += values[pos]; } return sum; } /** - * Computes the maximum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param smallestPossibleValue A value which is not larger than any value in values. If the filter is empty, this value is returned. - * @return The maximum over the subset of the values and the smallestPossibleValue. + * Computes the maximum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The maximum over the selected values. */ template - VT max_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& smallestPossibleValue) { - assert(values.size() >= filter.size()); + VT max_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; - VT max = smallestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] > max) { - max = values[i]; + for (; it != ite; ++it) { + if (values[*it] > current) { + current = values[*it]; } - } - return max; + } + return current; } /** - * Computes the minimum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param largestPossibleValue A value which is not smaller than any value in values. If the filter is empty, this value is returned. - * @return The minimum over the subset of the values and the largestPossibleValue. + * Computes the minimum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The minimum over the selected values. */ template - VT min_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& largestPossibleValue) { - assert(values.size() >= filter.size()); - VT min = largestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] < min) { - min = values[i]; + VT min_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; + + for (; it != ite; ++it) { + if (values[*it] < current) { + current = values[*it]; } - } - return min; + } + return current; } - - /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. *