diff --git a/src/logic/BoundInfo.h b/src/logic/BoundInfo.h new file mode 100644 index 000000000..453d9eb08 --- /dev/null +++ b/src/logic/BoundInfo.h @@ -0,0 +1,19 @@ + +#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 ae033b0c1..2b0cdcb70 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::optional(), boost::optional(), boost::optional(), 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(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType 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, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType 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::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -34,7 +34,7 @@ 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 comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index 136de2a4e..8be07520d 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -9,9 +9,9 @@ namespace storm { public: ExpectedTimeOperatorFormula(std::shared_ptr const& subformula); ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double 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); virtual ~ExpectedTimeOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index d3cfa605d..6d2f61880 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -26,5 +26,4 @@ #include "src/logic/ConditionalPathFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/RewardOperatorFormula.h" -#include "src/logic/ComparisonType.h" -#include "src/logic/OptimalityType.h" \ No newline at end of file +#include "src/logic/ComparisonType.h" \ No newline at end of file diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index b20924240..c540c9577 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::optional(), boost::optional(), boost::optional(), 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(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType 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, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType 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::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -34,7 +34,7 @@ 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 comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 4f14f5766..ddc8118a9 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -9,9 +9,9 @@ namespace storm { public: LongRunAverageOperatorFormula(std::shared_ptr const& subformula); LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double 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); virtual ~LongRunAverageOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index d9faaf057..5997c957d 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 comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { // Intentionally left empty. } @@ -22,13 +22,13 @@ namespace storm { return static_cast(optimalityType); } - OptimalityType const& OperatorFormula::getOptimalityType() const { + OptimizationDirection const& OperatorFormula::getOptimalityType() const { return optimalityType.get(); } std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { if (hasOptimalityType()) { - out << getOptimalityType(); + out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); } if (hasBound()) { out << getComparisonType() << getBound(); diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index d1ce2ee78..c849b0a41 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -4,14 +4,14 @@ #include #include "src/logic/UnaryStateFormula.h" -#include "src/logic/OptimalityType.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 comparisonType, boost::optional bound, std::shared_ptr const& subformula); virtual ~OperatorFormula() { // Intentionally left empty. @@ -21,7 +21,7 @@ namespace storm { ComparisonType const& getComparisonType() const; double getBound() const; bool hasOptimalityType() const; - OptimalityType const& getOptimalityType() const; + OptimizationDirection const& getOptimalityType() const; virtual std::ostream& writeToStream(std::ostream& out) const override; @@ -29,7 +29,7 @@ namespace storm { std::string operatorSymbol; boost::optional comparisonType; boost::optional bound; - boost::optional optimalityType; + boost::optional optimalityType; }; } } diff --git a/src/logic/OptimalityType.cpp b/src/logic/OptimalityType.cpp deleted file mode 100644 index 1c44ad0c3..000000000 --- a/src/logic/OptimalityType.cpp +++ /dev/null @@ -1,13 +0,0 @@ -#include "src/logic/OptimalityType.h" - -namespace storm { - namespace logic { - std::ostream& operator<<(std::ostream& out, OptimalityType const& optimalityType) { - switch (optimalityType) { - case Maximize: out << "max"; break; - case Minimize: out << "min"; break; - } - return out; - } - } -} \ No newline at end of file diff --git a/src/logic/OptimalityType.h b/src/logic/OptimalityType.h deleted file mode 100644 index e21a8e58f..000000000 --- a/src/logic/OptimalityType.h +++ /dev/null @@ -1,14 +0,0 @@ -#ifndef STORM_LOGIC_OPTIMALITYTYPE_H_ -#define STORM_LOGIC_OPTIMALITYTYPE_H_ - -#include - -namespace storm { - namespace logic { - enum OptimalityType { Minimize, Maximize }; - - std::ostream& operator<<(std::ostream& out, OptimalityType const& optimalityType); - } -} - -#endif /* STORM_LOGIC_OPTIMALITYTYPE_H_ */ diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index c5e854a80..93426262b 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::optional(), boost::optional(), boost::optional(), 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(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType 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, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType 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::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -42,7 +42,7 @@ 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 comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index a54bf62d3..1ccbb3985 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -9,9 +9,9 @@ namespace storm { public: ProbabilityOperatorFormula(std::shared_ptr const& subformula); ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double 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); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index dac396c69..32899d021 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::optional(), boost::optional(), boost::optional(), 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, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimalityType 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, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimalityType 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::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -55,7 +55,7 @@ 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 comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula), rewardModelName(rewardModelName) { // Intentionally left empty. } diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index b3d63a5a3..82e2d74f0 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -1,6 +1,7 @@ #ifndef STORM_LOGIC_REWARDOPERATORFORMULA_H_ #define STORM_LOGIC_REWARDOPERATORFORMULA_H_ +#include #include "src/logic/OperatorFormula.h" namespace storm { @@ -9,9 +10,9 @@ namespace storm { 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, OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimalityType 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, OptimizationDirection optimalityType, ComparisonType comparisonType, double 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); virtual ~RewardOperatorFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index e7df544b5..e0a4f127b 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -23,7 +23,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { if (pathFormula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), qualitative, optimalityType); } else if (pathFormula.isConditionalPathFormula()) { @@ -40,32 +40,32 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); return this->computeUntilProbabilities(newFormula, qualitative, optimalityType); } - std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { if (rewardPathFormula.isCumulativeRewardFormula()) { return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), rewardModelName, qualitative, optimalityType); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { @@ -76,23 +76,23 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeLongRunAverage(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeLongRunAverage(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages."); } - std::unique_ptr AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times."); } @@ -170,9 +170,9 @@ namespace storm { result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType()); } else if (stateFormula.hasBound()) { if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, storm::logic::OptimalityType::Maximize); + result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Maximize); } else { - result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, storm::logic::OptimalityType::Minimize); + result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Minimize); } } else { result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative); @@ -202,9 +202,9 @@ namespace storm { result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, stateFormula.getOptimalityType()); } else if (stateFormula.hasBound()) { if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, storm::logic::OptimalityType::Maximize); + result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Maximize); } else { - result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, storm::logic::OptimalityType::Minimize); + result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Minimize); } } else { result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative); @@ -234,9 +234,9 @@ namespace storm { result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType()); } else if (stateFormula.hasBound()) { if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, storm::logic::OptimalityType::Maximize); + result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Maximize); } else { - result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, storm::logic::OptimalityType::Minimize); + result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Minimize); } } else { result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative); @@ -258,9 +258,9 @@ namespace storm { result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); } else if (stateFormula.hasBound()) { if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, storm::logic::OptimalityType::Maximize); + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Maximize); } else { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, storm::logic::OptimalityType::Minimize); + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Minimize); } } else { result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 72f29d511..4c1347ea3 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -4,7 +4,7 @@ #include #include "src/logic/Formulas.h" - +#include "src/solver/OptimizationDirection.h" namespace storm { namespace modelchecker { @@ -34,23 +34,23 @@ namespace storm { virtual std::unique_ptr check(storm::logic::Formula const& formula); // The methods to compute probabilities for path formulas. - virtual std::unique_ptr computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); // The methods to compute the long-run average and expected time. - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); // The methods to check state formulas. virtual std::unique_ptr checkStateFormula(storm::logic::StateFormula const& stateFormula); diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 85464f106..04184b6cc 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -28,7 +28,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -38,7 +38,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -51,7 +51,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -59,7 +59,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -78,17 +78,17 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index a1f9cb6d4..c447909b2 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -18,13 +18,13 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Ctmc const& getModel() const override; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 8b3a2d9c5..eb8c6fb2c 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -34,7 +34,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; @@ -54,7 +54,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -62,7 +62,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -72,19 +72,19 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -93,7 +93,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 7cc6289bc..8423cac53 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -21,13 +21,13 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index f2d7463fe..57bfda26f 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -31,54 +31,59 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverage(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverage(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index e93c36dec..1062dd0ec 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -21,11 +21,11 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index ae7a04cd8..c7d1d23b1 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -22,14 +22,16 @@ #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { namespace helper { - template - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + template + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states. @@ -99,7 +101,7 @@ namespace storm { storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); // Now perform the inner value iteration for probabilistic states. - solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); @@ -112,11 +114,12 @@ namespace storm { // After the loop, perform one more step of the value iteration for PS states. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); - solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); } - template - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + template + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // 'Unpack' the bounds to make them more easily accessible. @@ -142,7 +145,7 @@ namespace storm { std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); std::vector vMarkovian(markovianNonGoalStates.getNumberOfSetBits()); - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRateVector, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. if (lowerBound != storm::utility::zero()) { @@ -160,7 +163,7 @@ namespace storm { STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); // Compute the bounded reachability for interval [0, b-a]. - computeBoundedReachabilityProbabilities(minimize, transitionMatrix, exitRateVector, markovianStates, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); // Create the result vector out of vAllProbabilistic and vAllMarkovian and return it. std::vector result(numberOfStates, storm::utility::zero()); @@ -178,20 +181,20 @@ namespace storm { } } - template - std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - return storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); + + template + std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); } template template - std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); - return computeExpectedRewards(minimize, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); + return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); } - - template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // If there are no goal states, we avoid the computation and directly return zero. @@ -229,7 +232,7 @@ namespace storm { } // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(minimize, transitionMatrix, exitRateVector, markovianStates, psiStates, mec)); + lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, mec)); } // For fast transition rewriting, we build some auxiliary data structures. @@ -329,7 +332,7 @@ namespace storm { std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); - solver->solveEquationSystem(minimize, x, b); + solver->solveEquationSystem(dir, x, b); // Prepare result vector. std::vector result(numberOfStates); @@ -346,20 +349,21 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeExpectedTimes(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + std::vector SparseMarkovAutomatonCslHelper::computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); std::vector rewardValues(numberOfStates, storm::utility::zero()); storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one()); - return computeExpectedRewards(minimize, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, rewardValues, minMaxLinearEquationSolverFactory); + return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, rewardValues, minMaxLinearEquationSolverFactory); } template - std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // First, we need to check which states have infinite expected time (by definition). storm::storage::BitVector infinityStates; - if (minimize) { + if (dir ==OptimizationDirection::Minimize) { // If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers, // reach a bottom SCC without a goal state. @@ -423,7 +427,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->solveEquationSystem(minimize, x, b); + solver->solveEquationSystem(dir, x, b); // Create resulting vector. std::vector result(numberOfStates); @@ -436,11 +440,12 @@ namespace storm { return result; } - template - ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); - solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); + solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. std::map stateToVariableMap; @@ -466,7 +471,7 @@ namespace storm { constraint = constraint + solver->getConstant(storm::utility::one() / exitRateVector[state]) * k; storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::one() / exitRateVector[state]) : solver->getConstant(0); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { constraint = constraint >= rightHandSide; @@ -483,7 +488,7 @@ namespace storm { } storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::zero()); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { constraint = constraint >= rightHandSide; @@ -498,7 +503,7 @@ namespace storm { } template class SparseMarkovAutomatonCslHelper; - template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + //template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 4a49c11d2..73534fb6a 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -3,29 +3,31 @@ #include "src/storage/BitVector.h" #include "src/storage/MaximalEndComponent.h" - +#include "src/solver/OptimizationDirection.h" #include "src/utility/solver.h" namespace storm { + namespace modelchecker { namespace helper { template class SparseMarkovAutomatonCslHelper { public: - static std::vector computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + - static std::vector computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeExpectedTimes(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: - static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. @@ -39,7 +41,7 @@ namespace storm { * @param mec The maximal end component to consider for computing the long-run average. * @return The long-run average of being in a goal state for the given MEC. */ - static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); /*! * Computes the expected reward that is gained from each state before entering any of the goal states. @@ -57,7 +59,7 @@ namespace storm { * of the state. * @return A vector that contains the expected reward for each state of the model. */ - static std::vector computeExpectedRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); }; } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index c2d67f7ba..5438d3be7 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -39,7 +39,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -48,14 +48,14 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -65,19 +65,19 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); @@ -89,7 +89,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 36e52eebb..5ccb82bcd 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -18,13 +18,13 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 762c8126d..6cfe603d8 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -35,54 +35,54 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 0b80f7f97..b841d1d65 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -5,7 +5,7 @@ #include "src/utility/solver.h" #include "src/storage/dd/DdType.h" - +#include "src/solver/OptimizationDirection.h" namespace storm { namespace models { @@ -14,6 +14,7 @@ namespace storm { } } + namespace modelchecker { template class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { @@ -23,12 +24,12 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5c3684223..d457a4d50 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -35,7 +35,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -47,7 +47,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -55,7 +55,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -65,21 +65,21 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); @@ -87,7 +87,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 1d9b7efba..f6ec4b0e4 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -20,13 +20,13 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 3c1c3bc4d..553795c6f 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -42,67 +42,87 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType, boost::optional> const& bound) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + if(qualitative | !bound) { + // For qualitative checks, or if the , we use the standard approach. + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + // With a given bound, we only iterate until we pass the bound. + storm::solver::BoundedGoal boundedGoal(optimalityType.get(), bound.get(), this->getModel().getInitialStates() ); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(boundedGoal, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + + } + + template + std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverage(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverage(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 2bd9c091a..14f4462d2 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,6 +4,7 @@ #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 { @@ -15,6 +16,8 @@ namespace storm { class MILPMinimalLabelSetGenerator; } + + namespace modelchecker { template class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker { @@ -30,13 +33,14 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional(), boost::optional> const& bound =boost::optional>()); + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 0dcb52435..79e385bd4 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -35,7 +35,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -45,7 +45,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); @@ -53,7 +53,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -64,21 +64,21 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 761427f5e..117fe8ae6 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -15,12 +15,12 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index a8304af48..b14d0b36d 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -35,54 +35,54 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index bbef7ce0f..e37891724 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -17,12 +17,12 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 22cf9c314..cace7a13b 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -23,11 +23,11 @@ namespace storm { namespace helper { template - std::unique_ptr HybridMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); } else { statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); @@ -76,7 +76,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); - solver->solveEquationSystem(minimize, x, explicitRepresentation.second); + solver->solveEquationSystem(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x)); @@ -87,17 +87,17 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { + std::unique_ptr HybridMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); } template - std::unique_ptr HybridMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); } else { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); @@ -134,7 +134,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); - solver->performMatrixVectorMultiplication(minimize, x, &explicitRepresentation.second, stepBound); + solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.toAdd(), maybeStates, odd, x)); @@ -144,7 +144,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -159,14 +159,14 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); - solver->performMatrixVectorMultiplication(minimize, x, nullptr, stepBound); + solver->performMatrixVectorMultiplication(dir, x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); } template - std::unique_ptr HybridMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -185,14 +185,14 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); - solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); + solver->performMatrixVectorMultiplication(dir, x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); } template - std::unique_ptr HybridMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -200,7 +200,7 @@ namespace storm { // Determine which states have a reward of infinity by definition. storm::dd::Bdd infinityStates; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); @@ -247,7 +247,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); - solver->solveEquationSystem(minimize, x, explicitRepresentation.second); + solver->solveEquationSystem(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity()), maybeStates, odd, x)); diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h index 2658b82f2..87899970f 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h @@ -7,6 +7,7 @@ #include "src/storage/dd/Bdd.h" #include "src/utility/solver.h" +#include "src/solver/OptimizationDirection.h" namespace storm { namespace modelchecker { @@ -20,17 +21,17 @@ namespace storm { public: typedef typename storm::models::symbolic::NondeterministicModel::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 0f32864f6..ef33afe15 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -20,13 +20,14 @@ namespace storm { namespace modelchecker { namespace helper { + template - std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. storm::storage::BitVector maybeStates; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); } else { maybeStates = storm::utility::graph::performProbGreater0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); @@ -44,7 +45,7 @@ namespace storm { std::vector subresult(maybeStates.getNumberOfSetBits()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->performMatrixVectorMultiplication(minimize, subresult, &b, stepBound); + solver->performMatrixVectorMultiplication(dir, subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -54,26 +55,30 @@ namespace storm { return result; } + template - std::vector SparseMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Create the vector with which to multiply and initialize it correctly. std::vector result(transitionMatrix.getRowCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(minimize, result); + solver->performMatrixVectorMultiplication(dir, result); return result; } + template - std::vector SparseMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; - if (minimize) { + if (goal.minimize()) { statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); } else { statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); @@ -88,6 +93,11 @@ namespace storm { // Create resulting vector. std::vector result(numberOfStates); + // Set values of resulting vector that are known exactly. + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + + // Check whether we need to compute exact probabilities for some states. if (qualitative) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. @@ -108,24 +118,29 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits()); // Solve the corresponding system of equations. - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->solveEquationSystem(minimize, x, b); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->solveEquationSystem(goal.direction(), x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); } } - // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - return result; } + + template + std::vector SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + storm::solver::SolveGoal goal(dir); + return computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); + } + + template template - std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -133,14 +148,15 @@ namespace storm { std::vector result(rewardModel.getStateRewardVector()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(minimize, result, nullptr, stepCount); + solver->performMatrixVectorMultiplication(dir, result, nullptr, stepCount); return result; } template template - std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -156,17 +172,18 @@ namespace storm { } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(minimize, result, &totalRewardVector, stepBound); + solver->performMatrixVectorMultiplication(dir, result, &totalRewardVector, stepBound); return result; } + template template - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - // Only compute the result if the reward model is not empty. + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeReachabilityRewardsHelper(minimize, transitionMatrix, backwardTransitions, + return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions, [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); }, @@ -175,29 +192,29 @@ namespace storm { #ifdef STORM_HAVE_CARL template - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the reward model is not empty. STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeReachabilityRewardsHelper(minimize, transitionMatrix, backwardTransitions, + return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions, \ [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result; result.reserve(rowCount); std::vector subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); for (auto const& interval : subIntervalVector) { - result.push_back(minimize ? interval.lower() : interval.upper()); + result.push_back(dir == OptimizationDirection::Minimize ? interval.lower() : interval.upper()); } return result; - }, + }, \ targetStates, qualitative, minMaxLinearEquationSolverFactory); } #endif template - std::vector SparseMdpPrctlHelper::computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates); } else { infinityStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates); @@ -233,7 +250,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->solveEquationSystem(minimize, x, b); + solver->solveEquationSystem(dir, x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -247,7 +264,7 @@ namespace storm { } template - std::vector SparseMdpPrctlHelper::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); if (psiStates.empty()) { @@ -274,7 +291,7 @@ namespace storm { for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; - lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(minimize, transitionMatrix, psiStates, mec); + lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(dir, transitionMatrix, psiStates, mec); // Gather information for later use. for (auto const& stateChoicesPair : mec) { @@ -380,7 +397,7 @@ namespace storm { std::vector sspResult(numberOfStatesNotInMecs + mecDecomposition.size()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); - solver->solveEquationSystem(minimize, sspResult, b); + solver->solveEquationSystem(dir, sspResult, b); // Prepare result vector. std::vector result(numberOfStates, zero); @@ -397,9 +414,9 @@ namespace storm { } template - ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) { + ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) { std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); - solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); + solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. std::map stateToVariableMap; @@ -427,7 +444,7 @@ namespace storm { } constraint = solver->getConstant(r) + constraint; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { constraint = stateToVariableMap.at(state) <= constraint; } else { constraint = stateToVariableMap.at(state) >= constraint; @@ -441,9 +458,9 @@ namespace storm { } template class SparseMdpPrctlHelper; - template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index ef15c88ab..e93c70cde 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -8,6 +8,7 @@ #include "src/storage/MaximalEndComponent.h" #include "src/utility/solver.h" +#include "src/solver/SolveGoal.h" #include "src/adapters/CarlAdapter.h" @@ -25,31 +26,37 @@ namespace storm { template class SparseMdpPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeNextProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template - static std::vector computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static std::vector computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template + static std::vector computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template - static std::vector computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template + static std::vector computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template - static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); #ifdef STORM_HAVE_CARL - static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); #endif - static std::vector computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + - private: - static std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + private: + static std::vector computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + }; } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index d368ce66a..aefc6f023 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -69,7 +69,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -117,7 +117,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); @@ -173,7 +173,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); // Retrieve the appropriate bitvectors by model checking the subformulas. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 0648ad9e5..856fd7536 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -19,9 +19,9 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: class FlexibleSparseMatrix { diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 3aa9820d1..2d3fa0198 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -75,11 +75,11 @@ namespace storm { // A parser used for recognizing the operators at the "unary" precedence level. unaryBooleanOperatorStruct unaryBooleanOperator_; - struct optimalityOperatorStruct : qi::symbols { + struct optimalityOperatorStruct : qi::symbols { optimalityOperatorStruct() { add - ("min", storm::logic::OptimalityType::Minimize) - ("max", storm::logic::OptimalityType::Maximize); + ("min", storm::OptimizationDirection::Minimize) + ("max", storm::OptimizationDirection::Maximize); } }; @@ -111,7 +111,7 @@ namespace storm { qi::rule>(), Skipper> start; - qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> expectedTimeOperator; @@ -161,10 +161,10 @@ namespace storm { std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); }; @@ -304,7 +304,7 @@ namespace storm { pathFormula = conditionalFormula; pathFormula.name("path formula"); - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; + operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -464,19 +464,19 @@ namespace storm { return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp index d58fd1903..2236c7c78 100644 --- a/src/solver/AllowEarlyTerminationCondition.cpp +++ b/src/solver/AllowEarlyTerminationCondition.cpp @@ -5,8 +5,8 @@ namespace storm { namespace solver { template - TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove) : - terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove) + TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold) : + terminationThreshold(threshold), filter(filter) { // Intentionally left empty. } @@ -16,17 +16,14 @@ namespace storm { assert(currentValues.size() >= filter.size()); ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); - if(this->terminateIfAboveThreshold) { - return currentThreshold >= this->terminationThreshold; - } else { - return currentThreshold <= this->terminationThreshold; - } + return currentThreshold >= this->terminationThreshold; + } template - TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove, bool useMinimum) : - terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove), useMinimumAsExtremum(useMinimum) + TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum) : + terminationThreshold(threshold), filter(filter), useMinimumAsExtremum(useMinimum) { // Intentionally left empty. } @@ -35,14 +32,11 @@ namespace storm { bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { assert(currentValues.size() >= filter.size()); - ValueType initVal = terminateIfAboveThreshold ? terminationThreshold - 1 : terminationThreshold + 1; + ValueType initVal = terminationThreshold - 1; ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); - if(this->terminateIfAboveThreshold) { - return currentThreshold >= this->terminationThreshold; - } else { - return currentThreshold <= this->terminationThreshold; - } + return currentThreshold >= this->terminationThreshold; + } diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h index e2e3000b4..be9084c70 100644 --- a/src/solver/AllowEarlyTerminationCondition.h +++ b/src/solver/AllowEarlyTerminationCondition.h @@ -22,25 +22,23 @@ namespace storm { template class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition { public: - TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove); + TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold); bool terminateNow(std::vector const& currentValues) const; protected: ValueType terminationThreshold; storm::storage::BitVector filter; - bool terminateIfAboveThreshold; }; template class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ public: - TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove, bool useMinimum); + 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 terminateIfAboveThreshold; bool useMinimumAsExtremum; }; } diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index f2082e32a..25512fc33 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -19,7 +19,7 @@ #include "src/settings/modules/GlpkSettings.h" namespace storm { namespace solver { - GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { + GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { // Create the LP problem for glpk. lp = glp_create_prob(); @@ -35,15 +35,15 @@ namespace storm { coefficientValues.push_back(0); } - GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, ModelSense::Minimize) { + GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", ModelSense::Minimize) { + GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver(ModelSense const& modelSense) : GlpkLpSolver("", modelSense) { + GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) { // Intentionally left empty. } @@ -191,7 +191,7 @@ namespace storm { this->isUnboundedFlag = false; // Start by setting the model sense. - glp_set_obj_dir(this->lp, this->getModelSense() == LpSolver::ModelSense::Minimize ? GLP_MIN : GLP_MAX); + glp_set_obj_dir(this->lp, this->getOptimizationDirection() == OptimizationDirection::Minimize ? GLP_MIN : GLP_MAX); glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data()); diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h index 4717b5d97..29ff21225 100644 --- a/src/solver/GlpkLpSolver.h +++ b/src/solver/GlpkLpSolver.h @@ -24,14 +24,14 @@ namespace storm { * Constructs a solver with the given name and model sense. * * @param name The name of the LP problem. - * @param modelSense A value indicating whether the value of the objective function is to be minimized or + * @param optDir A value indicating whether the value of the objective function is to be minimized or * maximized. */ - GlpkLpSolver(std::string const& name, ModelSense const& modelSense); + GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir); /*! * Constructs a solver with the given name. By default the objective function is assumed to be minimized, - * but this may be altered later using a call to setModelSense. + * but this may be altered later using a call to setOptimizationDirection. * * @param name The name of the LP problem. */ @@ -40,14 +40,14 @@ namespace storm { /*! * Constructs a solver without a name and the given model sense. * - * @param modelSense A value indicating whether the value of the objective function is to be minimized or + * @param optDir A value indicating whether the value of the objective function is to be minimized or * maximized. */ - GlpkLpSolver(ModelSense const& modelSense); + GlpkLpSolver(OptimizationDirection const& optDir); /*! * Constructs a solver without a name. By default the objective function is assumed to be minimized, - * but this may be altered later using a call to setModelSense. + * but this may be altered later using a call to setOptimizationDirection. */ GlpkLpSolver(); @@ -133,7 +133,7 @@ namespace storm { // If glpk is not available, we provide a stub implementation that emits an error if any of its methods is called. class GlpkLpSolver : public LpSolver { public: - GlpkLpSolver(std::string const& name, ModelSense const& modelSense) { + GlpkLpSolver(std::string const& name, OptimizationDirection const& modelSense) { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } @@ -141,7 +141,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - GlpkLpSolver(ModelSense const& modelSense) : LpSolver(modelSense) { + GlpkLpSolver(OptimizationDirection const& modelSense) : LpSolver(modelSense) { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 11f5171c2..86b8dfa23 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -30,7 +30,7 @@ namespace storm { template - void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; @@ -59,7 +59,7 @@ namespace storm { gmm::add(b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices); // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative); @@ -139,7 +139,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); // Determine whether the method converged. @@ -174,7 +174,7 @@ namespace storm { } template - void GmmxxMinMaxLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void GmmxxMinMaxLinearEquationSolver::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(gmmxxMatrix->nr); @@ -189,7 +189,7 @@ namespace storm { gmm::add(*b, *multiplyResult); } - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, rowGroupIndices); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices); } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index b34f761cb..ed91278bc 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -33,9 +33,9 @@ namespace storm { */ GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy = false); - virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual void performMatrixVectorMultiplication(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; - virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquationSystem(OptimizationDirection d, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: // The (gmm++) matrix associated with this equation solver. diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index c8f97febf..0be57ac34 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -22,7 +22,7 @@ namespace storm { namespace solver { #ifdef STORM_HAVE_GUROBI - GurobiLpSolver::GurobiLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), env(nullptr), model(nullptr), nextVariableIndex(0) { + GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) { // Create the environment. int error = GRBloadenv(&env, ""); if (error || env == nullptr) { @@ -41,15 +41,15 @@ namespace storm { } } - GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, ModelSense::Minimize) { + GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver(ModelSense const& modelSense) : GurobiLpSolver("", modelSense) { + GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", ModelSense::Minimize) { + GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } @@ -195,7 +195,7 @@ namespace storm { this->update(); // Set the most recently set model sense. - int error = GRBsetintattr(model, "ModelSense", this->getModelSense() == ModelSense::Minimize ? 1 : -1); + int error = GRBsetintattr(model, "ModelSense", this->getOptimizationDirection() == OptimizationDirection::Minimize ? 1 : -1); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi model sense (" << GRBgeterrormsg(env) << ", error code " << error << ")."); // Then we actually optimize the model. @@ -353,7 +353,7 @@ namespace storm { } } #else - GurobiLpSolver::GurobiLpSolver(std::string const& name, ModelSense const& modelSense) { + GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& ) { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } @@ -361,7 +361,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - GurobiLpSolver::GurobiLpSolver(ModelSense const& modelSense) { + GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& modelSense) { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } diff --git a/src/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index d060036c8..543bfe81c 100644 --- a/src/solver/GurobiLpSolver.h +++ b/src/solver/GurobiLpSolver.h @@ -31,7 +31,7 @@ namespace storm { * @param modelSense A value indicating whether the value of the objective function is to be minimized or * maximized. */ - GurobiLpSolver(std::string const& name, ModelSense const& modelSense); + GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir); /*! * Constructs a solver with the given name. By default the objective function is assumed to be minimized, @@ -47,7 +47,7 @@ namespace storm { * @param modelSense A value indicating whether the value of the objective function is to be minimized or * maximized. */ - GurobiLpSolver(ModelSense const& modelSense); + GurobiLpSolver(OptimizationDirection const& optDir); /*! * Constructs a solver without a name. By default the objective function is assumed to be minimized, diff --git a/src/solver/LpSolver.cpp b/src/solver/LpSolver.cpp index 29840ac85..b191c9a9a 100644 --- a/src/solver/LpSolver.cpp +++ b/src/solver/LpSolver.cpp @@ -8,11 +8,11 @@ namespace storm { namespace solver { - LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), modelSense(ModelSense::Minimize) { + LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) { // Intentionally left empty. } - LpSolver::LpSolver(ModelSense const& modelSense) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), modelSense(modelSense) { + LpSolver::LpSolver(OptimizationDirection const& optimizationDir) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) { // Intentionally left empty. } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 816b0f097..398169085 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -5,6 +5,8 @@ #include #include #include +#include "OptimizationDirection.h" + namespace storm { namespace expressions { class ExpressionManager; @@ -19,10 +21,7 @@ namespace storm { class LpSolver { public: // An enumeration to represent whether the objective function is to be minimized or maximized. - enum class ModelSense { - Minimize, - Maximize - }; + /*! * Creates an empty LP solver. By default the objective function is assumed to be minimized. @@ -31,10 +30,10 @@ namespace storm { /*! * Creates an empty LP solver with the given model sense. * - * @param modelSense A value indicating whether the objective function of this model is to be minimized or + * @param optDir A value indicating whether the objective function of this model is to be minimized or * maximized. */ - LpSolver(ModelSense const& modelSense); + LpSolver(OptimizationDirection const& optDir); /*! * Registers an upper- and lower-bounded continuous variable, i.e. a variable that may take all real values @@ -232,11 +231,11 @@ namespace storm { * * @param modelSense The model sense to use. */ - void setModelSense(ModelSense const& modelSense) { - if (modelSense != this->modelSense) { + void setOptimizationDirection(OptimizationDirection const& optimizationDirection) { + if (optimizationDirection != this->optimizationDirection) { currentModelHasBeenOptimized = false; } - this->modelSense = modelSense; + this->optimizationDirection = optimizationDirection; } /*! @@ -244,8 +243,8 @@ namespace storm { * * @return A value indicating whether the objective function of this model is to be minimized or maximized. */ - ModelSense getModelSense() const { - return modelSense; + OptimizationDirection getOptimizationDirection() const { + return optimizationDirection; } /*! @@ -266,7 +265,7 @@ namespace storm { private: // A flag that indicates the model sense. - ModelSense modelSense; + OptimizationDirection optimizationDirection; }; } } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index b5d53a68e..57acf7f17 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -6,6 +6,7 @@ #include "SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" #include "AllowEarlyTerminationCondition.h" +#include "OptimizationDirection.h" namespace storm { namespace storage { @@ -13,6 +14,8 @@ namespace storm { } namespace solver { + + /** * Abstract base class which provides value-type independent helpers. */ @@ -23,9 +26,20 @@ namespace storm { std::vector getPolicy() const; + void setOptimizationDirection(OptimizationDirection d) { + direction = convert(d); + } + + void resetOptimizationDirection() { + direction = OptimizationDirectionSetting::Unset; + } + + protected: AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); - + + /// The direction in which to optimize, can be unset. + OptimizationDirectionSetting direction; /// The required precision for the iterative methods. double precision; @@ -70,7 +84,7 @@ namespace storm { * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has * to be given upon construction time of the solver object. * - * @param minimize If set, all the value of a group of rows is the taken as the minimum over all rows and as + * @param d For minimum, all the value of a group of rows is the taken as the minimum over all rows and as * the maximum otherwise. * @param x The solution vector x. The initial values of x represent a guess of the real values to the * solver, but may be ignored. @@ -81,8 +95,16 @@ namespace storm { * vector must be equal to the length of the vector x (and thus to the number of columns of A). * @return The solution vector x of the system of linear equations as the content of the parameter x. */ - virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; + virtual void solveEquationSystem(OptimizationDirection d, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; + /*! + * As solveEquationSystem with an optimization-direction, but this uses the internally set direction. + * Can only be called after the direction has been set. + */ + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const { + assert(isSet(this->direction)); + solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX); + } /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes * x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the @@ -90,7 +112,7 @@ namespace storm { * vector for the next iteration. Note that the matrix A has to be given upon construction time of the * solver object. * - * @param minimize If set, all the value of a group of rows is the taken as the minimum over all rows and as + * @param d For minimum, all the value of a group of rows is the taken as the minimum over all rows and as * the maximum otherwise. * @param x The initial vector that is to be multiplied with the matrix. This is also the output parameter, * i.e. after the method returns, this vector will contain the computed values. @@ -100,16 +122,25 @@ namespace storm { * vector must be equal to the number of rows of A. * @return The result of the repeated matrix-vector multiplication as the content of the vector x. */ - virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + virtual void performMatrixVectorMultiplication(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + /*! + * As performMatrixVectorMultiplication with an optimization-direction, but this uses the internally set direction. + * Can only be called if the internal direction has been set. + */ + virtual void performMatrixVectorMultiplication( std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const { + return performMatrixVectorMultiplication(convert(this->direction), x, b, n, multiplyResult); + } - void setEarlyTerminationCondition(std::unique_ptr> v) { + void setEarlyTerminationCriterion(std::unique_ptr> v) { earlyTermination = std::move(v); } + protected: - std::unique_ptr> earlyTermination; storm::storage::SparseMatrix const& A; + std::unique_ptr> earlyTermination; + }; } // namespace solver diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 4ac37ac3e..1a0881402 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -31,7 +31,7 @@ namespace storm { } template - void NativeMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void NativeMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; @@ -60,7 +60,7 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices()); // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -141,7 +141,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); // Determine whether the method converged. @@ -177,7 +177,7 @@ namespace storm { } template - void NativeMinMaxLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void NativeMinMaxLinearEquationSolver::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; @@ -197,7 +197,7 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices()); } diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index 5e297096a..5fcd76aa9 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -32,9 +32,9 @@ namespace storm { */ NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackPolicy = false); - virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; + virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; - virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; }; } // namespace solver diff --git a/src/solver/OptimizationDirection.cpp b/src/solver/OptimizationDirection.cpp new file mode 100644 index 000000000..cd88657b9 --- /dev/null +++ b/src/solver/OptimizationDirection.cpp @@ -0,0 +1,38 @@ +#include "OptimizationDirection.h" +#include +#include + +namespace storm { + namespace solver { + + bool isSet(OptimizationDirectionSetting s) { + return s != OptimizationDirectionSetting::Unset; + } + + bool minimize(OptimizationDirection d) { + return d == OptimizationDirection::Minimize; + } + + bool maximize(OptimizationDirection d) { + return d == OptimizationDirection::Maximize; + } + + OptimizationDirection convert(OptimizationDirectionSetting s) { + assert(isSet(s)); + return static_cast(s); + } + + OptimizationDirectionSetting convert(OptimizationDirection d) { + return static_cast(d); + } + + OptimizationDirection invert(OptimizationDirection d) { + return d == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } + + std::ostream& operator<<(std::ostream& out, OptimizationDirection d) { + return d == OptimizationDirection::Minimize ? out << "Minimize" : out << "Maximize"; + } + } +} + diff --git a/src/solver/OptimizationDirection.h b/src/solver/OptimizationDirection.h new file mode 100644 index 000000000..82d8abe06 --- /dev/null +++ b/src/solver/OptimizationDirection.h @@ -0,0 +1,31 @@ +#ifndef OPTIMIZATIONDIRECTIONSETTING_H +#define OPTIMIZATIONDIRECTIONSETTING_H + +#include + +namespace storm { + namespace solver { + enum class OptimizationDirection { Minimize = 0, Maximize = 1 }; + enum class OptimizationDirectionSetting { Minimize = 0, Maximize = 1, Unset }; + + bool isSet(OptimizationDirectionSetting s); + + bool minimize(OptimizationDirection d); + + bool maximize(OptimizationDirection d); + + OptimizationDirection convert(OptimizationDirectionSetting s); + + OptimizationDirectionSetting convert(OptimizationDirection d); + + OptimizationDirection invert(OptimizationDirection d); + + std::ostream& operator<<(std::ostream& out, OptimizationDirection d); + } + + using OptimizationDirection = solver::OptimizationDirection; +} + + +#endif /* OPTIMIZATIONDIRECTIONSETTING_H */ + diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp new file mode 100644 index 000000000..7cdf2f238 --- /dev/null +++ b/src/solver/SolveGoal.cpp @@ -0,0 +1,32 @@ +#include "SolveGoal.h" + +#include "src/storage/SparseMatrix.h" +#include "src/utility/solver.h" +#include "src/solver/MinMaxLinearEquationSolver.h" + +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> p = factory.create(matrix); + p->setOptimizationDirection(goal.direction()); + p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.threshold, goal.minimize())); + return p; + } + + template + 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; + } + + template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + } +} diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h new file mode 100644 index 000000000..ab959a032 --- /dev/null +++ b/src/solver/SolveGoal.h @@ -0,0 +1,71 @@ + +#ifndef SOLVEGOAL_H +#define SOLVEGOAL_H + +#include "src/solver/OptimizationDirection.h" +#include "src/logic/ComparisonType.h" +#include "src/logic/BoundInfo.h" +#include "src/storage/BitVector.h" + +namespace storm { + namespace storage { + template class SparseMatrix; + } + namespace utility { + namespace solver { + template class MinMaxLinearEquationSolverFactory; + } + } + + + namespace solver { + template class MinMaxLinearEquationSolver; + + class SolveGoal { + public: + SolveGoal(bool minimize) : optDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) {} + SolveGoal(OptimizationDirection d) : optDirection(d) {} + virtual ~SolveGoal() {} + + bool minimize() const { return optDirection == OptimizationDirection::Minimize; } + OptimizationDirection direction() const { return optDirection; } + virtual bool isBounded() const { return false; } + + private: + OptimizationDirection optDirection; + + }; + + + template + class BoundedGoal : public SolveGoal { + public: + BoundedGoal(OptimizationDirection dir, storm::logic::ComparisonType ct, VT const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) {} + BoundedGoal(OptimizationDirection dir, storm::logic::BoundInfo const& bi, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(bi.boundType), threshold(bi.bound), relevantColumnVector(relColumns) {} + virtual ~BoundedGoal() {} + + bool isBounded() const override { return true; } + + bool boundIsALowerBound() const { + return (boundType == storm::logic::ComparisonType::Greater | + boundType == storm::logic::ComparisonType::GreaterEqual); ; + } + VT thresholdValue() const { return threshold; } + storm::storage::BitVector relevantColumns() const { return relevantColumnVector; } + + storm::logic::ComparisonType boundType; + VT threshold; + storm::storage::BitVector relevantColumnVector; + }; + template + std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + + } +} + + +#endif /* SOLVEGOAL_H */ + diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index d31a02d3e..f16c92a07 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -46,7 +46,7 @@ namespace storm { } template - void TopologicalMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void TopologicalMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { #ifdef GPU_USE_FLOAT #define __FORCE_FLOAT_CALCULATION true @@ -62,7 +62,7 @@ namespace storm { std::vector new_x = storm::utility::vector::toValueType(x); std::vector const new_b = storm::utility::vector::toValueType(b); - newSolver.solveEquationSystem(minimize, new_x, new_b, nullptr, nullptr); + newSolver.solveEquationSystem(dir, new_x, new_b, nullptr, nullptr); for (size_t i = 0, size = new_x.size(); i < size; ++i) { x.at(i) = new_x.at(i); @@ -102,7 +102,7 @@ namespace storm { bool result = false; size_t globalIterations = 0; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { result = __basicValueIteration_mvReduce_minimize(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); } else { result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); @@ -204,7 +204,7 @@ namespace storm { bool result = false; localIterations = 0; - if (minimize) { + if (dir == OptimizationDirection::Minimum) { result = __basicValueIteration_mvReduce_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); } else { result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); @@ -249,12 +249,8 @@ namespace storm { */ // Reduce the vector x' by applying min/max for all non-deterministic choices. - if (minimize) { - storm::utility::vector::reduceVectorMin(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); - } else { - storm::utility::vector::reduceVectorMax(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); - } - + storm::utility::vector::reduceVectorMinOrMax(dir,sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); + // Determine whether the method converged. // TODO: It seems that the equalModuloPrecision call that compares all values should have a higher // running time. In fact, it is faster. This has to be investigated. diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h index be1b844bd..25c325f75 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -22,8 +22,8 @@ namespace storm { * A class that uses SCC Decompositions to solve a min/max linear equation system. */ template - class TopologicalMinMaxLinearEquationSolver : public NativeMinMaxLinearEquationSolver { - public: + class TopologicalMinMaxLinearEquationSolver : public NativeMinMaxLinearEquationSolver { + public: /*! * Constructs a min-max linear equation solver with parameters being set according to the settings * object. @@ -43,7 +43,7 @@ namespace storm { */ TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); - virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: bool enableCuda; diff --git a/src/utility/vector.h b/src/utility/vector.h index 92c4a4265..621c84b2f 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -13,6 +13,7 @@ #include "src/storage/BitVector.h" #include "src/utility/macros.h" +#include "src/solver/OptimizationDirection.h" template std::ostream& operator<<(std::ostream& out, std::vector const& vector); @@ -521,21 +522,22 @@ namespace storm { /*! * Reduces the given source vector by selecting either the smallest or the largest out of each row group. * - * @param minimize If true, select the smallest, else select the largest. + * @param dir If true, select the smallest, else select the largest. * @param source The source vector which is to be reduced. * @param target The target vector into which a single element from each row group is written. * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. * @param choices If non-null, this vector is used to store the choices made during the selection. */ template - void reduceVectorMinOrMax(bool minimize, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - if(minimize) { + void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { + if(dir == storm::solver::OptimizationDirection::Minimize) { reduceVectorMin(source, target, rowGrouping, choices); } else { reduceVectorMax(source, target, rowGrouping, choices); } } + /*! * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag * additionaly specifies whether the error is computed in relative or absolute terms. diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index c19c605a0..21e97bf79 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/test/functional/solver/GlpkLpSolverTest.cpp @@ -11,9 +11,10 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/storage/expressions/Expressions.h" +#include "src/solver/OptimizationDirection.h" TEST(GlpkLpSolver, LPOptimizeMax) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -46,7 +47,7 @@ TEST(GlpkLpSolver, LPOptimizeMax) { } TEST(GlpkLpSolver, LPOptimizeMin) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -79,7 +80,7 @@ TEST(GlpkLpSolver, LPOptimizeMin) { } TEST(GlpkLpSolver, MILPOptimizeMax) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -112,7 +113,7 @@ TEST(GlpkLpSolver, MILPOptimizeMax) { } TEST(GlpkLpSolver, MILPOptimizeMin) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -145,7 +146,7 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { } TEST(GlpkLpSolver, LPInfeasible) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -171,7 +172,7 @@ TEST(GlpkLpSolver, LPInfeasible) { } TEST(GlpkLpSolver, MILPInfeasible) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -197,7 +198,7 @@ TEST(GlpkLpSolver, MILPInfeasible) { } TEST(GlpkLpSolver, LPUnbounded) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -221,7 +222,7 @@ TEST(GlpkLpSolver, LPUnbounded) { } TEST(GlpkLpSolver, MILPUnbounded) { - storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index bc6642e7c..ff91e660a 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -18,10 +18,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { std::vector b = {0.099, 0.5}; storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } @@ -39,17 +39,17 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio double bound = 0.8; storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); - solver.setEarlyTerminationCondition(std::unique_ptr>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector(1, true), bound, true, true))); - ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); bound = 0.6; - solver.setEarlyTerminationCondition(std::unique_ptr>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector(1, true), bound, true, true))); + solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); } @@ -75,23 +75,23 @@ TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { ASSERT_NO_THROW(storm::solver::GmmxxMinMaxLinearEquationSolver solver(A)); storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 1)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::gmmxxEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 2)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 2)); ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::gmmxxEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 20)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, x, nullptr, 1)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, x, nullptr, 20)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } @@ -108,9 +108,9 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); storm::solver::GmmxxMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative); - ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index b8fd4f256..b31070d56 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -11,7 +11,7 @@ #include "src/storage/expressions/Expressions.h" TEST(GurobiLpSolver, LPOptimizeMax) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -44,7 +44,7 @@ TEST(GurobiLpSolver, LPOptimizeMax) { } TEST(GurobiLpSolver, LPOptimizeMin) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -77,7 +77,7 @@ TEST(GurobiLpSolver, LPOptimizeMin) { } TEST(GurobiLpSolver, MILPOptimizeMax) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -110,7 +110,7 @@ TEST(GurobiLpSolver, MILPOptimizeMax) { } TEST(GurobiLpSolver, MILPOptimizeMin) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -143,7 +143,7 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { } TEST(GurobiLpSolver, LPInfeasible) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -173,7 +173,7 @@ TEST(GurobiLpSolver, LPInfeasible) { } TEST(GurobiLpSolver, MILPInfeasible) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -203,7 +203,7 @@ TEST(GurobiLpSolver, MILPInfeasible) { } TEST(GurobiLpSolver, LPUnbounded) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -231,7 +231,7 @@ TEST(GurobiLpSolver, LPUnbounded) { } TEST(GurobiLpSolver, MILPUnbounded) { - storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index b83423ffe..6bb0e0335 100644 --- a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -19,10 +19,10 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { std::vector b = {0.099, 0.5}; storm::solver::NativeMinMaxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::nativeEquationSolverSettings().getPrecision()); } @@ -47,23 +47,23 @@ TEST(NativeMinMaxLinearEquationSolver, MatrixVectorMultiplication) { ASSERT_NO_THROW(storm::solver::NativeMinMaxLinearEquationSolver solver(A)); storm::solver::NativeMinMaxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 1)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::nativeEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 2)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 2)); ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::nativeEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, x, nullptr, 20)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, x, nullptr, 1)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, x, nullptr, 20)); + ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::nativeEquationSolverSettings().getPrecision()); } @@ -81,9 +81,9 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); storm::solver::NativeMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative); - ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::nativeEquationSolverSettings().getPrecision()); } \ No newline at end of file