diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp index 2c7ed2cde..7c29c579b 100644 --- a/src/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -30,6 +30,10 @@ namespace storm { return bounds.which() == 0; } + bool BoundedUntilFormula::isValidProbabilityPathFormula() const { + return true; + } + bool BoundedUntilFormula::isPctlPathFormula() const { return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); } diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h index 4d72abdc1..7da7e70f6 100644 --- a/src/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -22,6 +22,7 @@ namespace storm { std::pair const& getIntervalBounds() const; uint_fast64_t getDiscreteTimeBound() const; + virtual bool isValidProbabilityPathFormula() const override; virtual bool isPctlPathFormula() const override; virtual bool isCslPathFormula() const override; diff --git a/src/logic/ConditionalPathFormula.cpp b/src/logic/ConditionalPathFormula.cpp index b5d8af81d..8ef461e35 100644 --- a/src/logic/ConditionalPathFormula.cpp +++ b/src/logic/ConditionalPathFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + bool ConditionalPathFormula::isValidProbabilityPathFormula() const { + return true; + } + std::shared_ptr ConditionalPathFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution)); } diff --git a/src/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h index bd5f3852c..a3e12e20f 100644 --- a/src/logic/ConditionalPathFormula.h +++ b/src/logic/ConditionalPathFormula.h @@ -14,7 +14,8 @@ namespace storm { } virtual bool isConditionalPathFormula() const override; - + virtual bool isValidProbabilityPathFormula() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp index ed4b18c85..3f53c2e9d 100644 --- a/src/logic/CumulativeRewardFormula.cpp +++ b/src/logic/CumulativeRewardFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return true; } + bool CumulativeRewardFormula::isValidRewardPathFormula() const { + return true; + } + bool CumulativeRewardFormula::hasDiscreteTimeBound() const { return timeBound.which() == 0; } diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h index 8b8692743..4ebf08cd4 100644 --- a/src/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -3,11 +3,11 @@ #include -#include "src/logic/RewardPathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { - class CumulativeRewardFormula : public RewardPathFormula { + class CumulativeRewardFormula : public PathFormula { public: CumulativeRewardFormula(uint_fast64_t timeBound); @@ -18,7 +18,8 @@ namespace storm { } virtual bool isCumulativeRewardFormula() const override; - + virtual bool isValidRewardPathFormula() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; bool hasDiscreteTimeBound() const; diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index b8ea1aa35..a25d12b33 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -10,6 +10,14 @@ namespace storm { return true; } + bool EventuallyFormula::isValidProbabilityPathFormula() const { + return true; + } + + bool EventuallyFormula::isValidRewardPathFormula() const { + return true; + } + std::shared_ptr EventuallyFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getSubformula().substitute(substitution)); } diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index 816f93c82..a488eb443 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -14,7 +14,9 @@ namespace storm { } virtual bool isEventuallyFormula() const override; - + virtual bool isValidProbabilityPathFormula() const override; + virtual bool isValidRewardPathFormula() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 5ba068af9..e3fa84c74 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -87,10 +87,6 @@ namespace storm { return false; } - bool Formula::isRewardPathFormula() const { - return false; - } - bool Formula::isCumulativeRewardFormula() const { return false; } @@ -99,10 +95,6 @@ namespace storm { return false; } - bool Formula::isReachabilityRewardFormula() const { - return false; - } - bool Formula::isLongRunAverageRewardFormula() const { return false; } @@ -147,6 +139,14 @@ namespace storm { return false; } + bool Formula::isValidProbabilityPathFormula() const { + return false; + } + + bool Formula::isValidRewardPathFormula() const { + return false; + } + bool Formula::containsBoundedUntilFormula() const { return false; } @@ -327,14 +327,6 @@ namespace storm { return dynamic_cast(*this); } - RewardPathFormula& Formula::asRewardPathFormula() { - return dynamic_cast(*this); - } - - RewardPathFormula const& Formula::asRewardPathFormula() const { - return dynamic_cast(*this); - } - CumulativeRewardFormula& Formula::asCumulativeRewardFormula() { return dynamic_cast(*this); } @@ -350,15 +342,7 @@ namespace storm { InstantaneousRewardFormula const& Formula::asInstantaneousRewardFormula() const { return dynamic_cast(*this); } - - ReachabilityRewardFormula& Formula::asReachabilityRewardFormula() { - return dynamic_cast(*this); - } - - ReachabilityRewardFormula const& Formula::asReachabilityRewardFormula() const { - return dynamic_cast(*this); - } - + LongRunAverageRewardFormula& Formula::asLongRunAverageRewardFormula() { return dynamic_cast(*this); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 31ee7744a..2ea234449 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -31,10 +31,8 @@ namespace storm { class NextFormula; class LongRunAverageOperatorFormula; class ExpectedTimeOperatorFormula; - class RewardPathFormula; class CumulativeRewardFormula; class InstantaneousRewardFormula; - class ReachabilityRewardFormula; class LongRunAverageRewardFormula; class ProbabilityOperatorFormula; class RewardOperatorFormula; @@ -74,10 +72,8 @@ namespace storm { virtual bool isNextFormula() const; virtual bool isLongRunAverageOperatorFormula() const; virtual bool isExpectedTimeOperatorFormula() const; - virtual bool isRewardPathFormula() const; virtual bool isCumulativeRewardFormula() const; virtual bool isInstantaneousRewardFormula() const; - virtual bool isReachabilityRewardFormula() const; virtual bool isLongRunAverageRewardFormula() const; virtual bool isProbabilityOperatorFormula() const; virtual bool isRewardOperatorFormula() const; @@ -90,6 +86,8 @@ namespace storm { virtual bool isPltlFormula() const; virtual bool isLtlFormula() const; virtual bool isPropositionalFormula() const; + virtual bool isValidProbabilityPathFormula() const; + virtual bool isValidRewardPathFormula() const; virtual bool containsBoundedUntilFormula() const; virtual bool containsNextFormula() const; virtual bool containsProbabilityOperator() const; @@ -156,18 +154,12 @@ namespace storm { ExpectedTimeOperatorFormula& asExpectedTimeOperatorFormula(); ExpectedTimeOperatorFormula const& asExpectedTimeOperatorFormula() const; - RewardPathFormula& asRewardPathFormula(); - RewardPathFormula const& asRewardPathFormula() const; - CumulativeRewardFormula& asCumulativeRewardFormula(); CumulativeRewardFormula const& asCumulativeRewardFormula() const; InstantaneousRewardFormula& asInstantaneousRewardFormula(); InstantaneousRewardFormula const& asInstantaneousRewardFormula() const; - ReachabilityRewardFormula& asReachabilityRewardFormula(); - ReachabilityRewardFormula const& asReachabilityRewardFormula() const; - LongRunAverageRewardFormula& asLongRunAverageRewardFormula(); LongRunAverageRewardFormula const& asLongRunAverageRewardFormula() const; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 3671b2859..7da9321c6 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -12,10 +12,8 @@ #include "src/logic/InstantaneousRewardFormula.h" #include "src/logic/NextFormula.h" #include "src/logic/PathFormula.h" -#include "src/logic/RewardPathFormula.h" #include "src/logic/OperatorFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" -#include "src/logic/ReachabilityRewardFormula.h" #include "src/logic/LongRunAverageRewardFormula.h" #include "src/logic/RewardOperatorFormula.h" #include "src/logic/StateFormula.h" diff --git a/src/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp index 8d2d1c92a..5ddfd8feb 100644 --- a/src/logic/GloballyFormula.cpp +++ b/src/logic/GloballyFormula.cpp @@ -9,7 +9,11 @@ namespace storm { bool GloballyFormula::isGloballyFormula() const { return true; } - + + bool GloballyFormula::isValidProbabilityPathFormula() const { + return true; + } + std::shared_ptr GloballyFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getSubformula().substitute(substitution)); } diff --git a/src/logic/GloballyFormula.h b/src/logic/GloballyFormula.h index 6346200c8..e3fc82f2d 100644 --- a/src/logic/GloballyFormula.h +++ b/src/logic/GloballyFormula.h @@ -14,7 +14,8 @@ namespace storm { } virtual bool isGloballyFormula() const override; - + virtual bool isValidProbabilityPathFormula() const override; + virtual std::shared_ptr substitute(std::map const& substitution) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp index 7d81f1234..77efb5705 100644 --- a/src/logic/InstantaneousRewardFormula.cpp +++ b/src/logic/InstantaneousRewardFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return true; } + bool InstantaneousRewardFormula::isValidRewardPathFormula() const { + return true; + } + bool InstantaneousRewardFormula::hasDiscreteTimeBound() const { return timeBound.which() == 0; } diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h index 8b29fa740..c895c5b39 100644 --- a/src/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -3,11 +3,11 @@ #include -#include "src/logic/RewardPathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { - class InstantaneousRewardFormula : public RewardPathFormula { + class InstantaneousRewardFormula : public PathFormula { public: InstantaneousRewardFormula(uint_fast64_t timeBound); @@ -18,7 +18,8 @@ namespace storm { } virtual bool isInstantaneousRewardFormula() const override; - + virtual bool isValidRewardPathFormula() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; bool hasDiscreteTimeBound() const; diff --git a/src/logic/LongRunAverageRewardFormula.cpp b/src/logic/LongRunAverageRewardFormula.cpp index 896e94a31..7bc064c1e 100644 --- a/src/logic/LongRunAverageRewardFormula.cpp +++ b/src/logic/LongRunAverageRewardFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + bool LongRunAverageRewardFormula::isValidRewardPathFormula() const { + return true; + } + std::shared_ptr LongRunAverageRewardFormula::substitute(std::map const& substitution) const { return std::shared_ptr(new LongRunAverageRewardFormula()); } diff --git a/src/logic/LongRunAverageRewardFormula.h b/src/logic/LongRunAverageRewardFormula.h index 449d5fd0e..aa4d3f424 100644 --- a/src/logic/LongRunAverageRewardFormula.h +++ b/src/logic/LongRunAverageRewardFormula.h @@ -1,14 +1,11 @@ #ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ #define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ -#include - -#include "src/logic/RewardPathFormula.h" - +#include "src/logic/PathFormula.h" namespace storm { namespace logic { - class LongRunAverageRewardFormula : public RewardPathFormula { + class LongRunAverageRewardFormula : public PathFormula { public: LongRunAverageRewardFormula(); @@ -17,7 +14,8 @@ namespace storm { } virtual bool isLongRunAverageRewardFormula() const override; - + virtual bool isValidRewardPathFormula() const override; + virtual std::shared_ptr substitute(std::map const& substitution) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp index b5064253f..b7400eb7d 100644 --- a/src/logic/NextFormula.cpp +++ b/src/logic/NextFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + bool NextFormula::isValidProbabilityPathFormula() const { + return true; + } + bool NextFormula::containsNextFormula() const { return true; } diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h index 2466d0b3d..f0de43cc6 100644 --- a/src/logic/NextFormula.h +++ b/src/logic/NextFormula.h @@ -14,7 +14,8 @@ namespace storm { } virtual bool isNextFormula() const override; - + virtual bool isValidProbabilityPathFormula() const override; + virtual bool containsNextFormula() const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/ReachabilityRewardFormula.cpp b/src/logic/ReachabilityRewardFormula.cpp deleted file mode 100644 index 83ba52f91..000000000 --- a/src/logic/ReachabilityRewardFormula.cpp +++ /dev/null @@ -1,35 +0,0 @@ -#include "src/logic/ReachabilityRewardFormula.h" - -namespace storm { - namespace logic { - ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr const& subformula) : subformula(subformula) { - // Intentionally left empty. - } - - bool ReachabilityRewardFormula::isReachabilityRewardFormula() const { - return true; - } - - Formula const& ReachabilityRewardFormula::getSubformula() const { - return *subformula; - } - - void ReachabilityRewardFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { - this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); - } - - void ReachabilityRewardFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { - this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); - } - - std::shared_ptr ReachabilityRewardFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->getSubformula().substitute(substitution)); - } - - std::ostream& ReachabilityRewardFormula::writeToStream(std::ostream& out) const { - out << "F "; - this->getSubformula().writeToStream(out); - return out; - } - } -} \ No newline at end of file diff --git a/src/logic/ReachabilityRewardFormula.h b/src/logic/ReachabilityRewardFormula.h deleted file mode 100644 index bfef88188..000000000 --- a/src/logic/ReachabilityRewardFormula.h +++ /dev/null @@ -1,36 +0,0 @@ -#ifndef STORM_LOGIC_REACHABILITYREWARDFORMULA_H_ -#define STORM_LOGIC_REACHABILITYREWARDFORMULA_H_ - -#include - -#include "src/logic/RewardPathFormula.h" - - -namespace storm { - namespace logic { - class ReachabilityRewardFormula : public RewardPathFormula { - public: - ReachabilityRewardFormula(std::shared_ptr const& subformula); - - virtual ~ReachabilityRewardFormula() { - // Intentionally left empty. - } - - virtual bool isReachabilityRewardFormula() const override; - - Formula const& getSubformula() const; - - virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; - virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - - virtual std::ostream& writeToStream(std::ostream& out) const override; - - virtual std::shared_ptr substitute(std::map const& substitution) const override; - - private: - std::shared_ptr subformula; - }; - } -} - -#endif /* STORM_LOGIC_REACHABILITYREWARDFORMULA_H_ */ \ No newline at end of file diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 791d1f5cc..1e5390830 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -23,7 +23,8 @@ namespace storm { } bool RewardOperatorFormula::isPctlStateFormula() const { - return this->getSubformula().isRewardPathFormula(); + Formula const& subformula = this->getSubformula(); + return subformula.isEventuallyFormula() || subformula.isCumulativeRewardFormula() || subformula.isInstantaneousRewardFormula(); } bool RewardOperatorFormula::containsRewardOperator() const { diff --git a/src/logic/RewardPathFormula.cpp b/src/logic/RewardPathFormula.cpp deleted file mode 100644 index 3c97acf74..000000000 --- a/src/logic/RewardPathFormula.cpp +++ /dev/null @@ -1,9 +0,0 @@ -#include "src/logic/RewardPathFormula.h" - -namespace storm { - namespace logic { - bool RewardPathFormula::isRewardPathFormula() const { - return true; - } - } -} \ No newline at end of file diff --git a/src/logic/RewardPathFormula.h b/src/logic/RewardPathFormula.h deleted file mode 100644 index 023e76e2d..000000000 --- a/src/logic/RewardPathFormula.h +++ /dev/null @@ -1,19 +0,0 @@ -#ifndef STORM_LOGIC_PATHREWARDFORMULA_H_ -#define STORM_LOGIC_PATHREWARDFORMULA_H_ - -#include "src/logic/PathFormula.h" - -namespace storm { - namespace logic { - class RewardPathFormula : public Formula { - public: - virtual ~RewardPathFormula() { - // Intentionally left empty. - } - - virtual bool isRewardPathFormula() const override; - }; - } -} - -#endif /* STORM_LOGIC_PATHREWARDFORMULA_H_ */ \ No newline at end of file diff --git a/src/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp index 94d7c62a8..b15f3743f 100644 --- a/src/logic/UntilFormula.cpp +++ b/src/logic/UntilFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + bool UntilFormula::isValidProbabilityPathFormula() const { + return true; + } + std::shared_ptr UntilFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution)); } diff --git a/src/logic/UntilFormula.h b/src/logic/UntilFormula.h index 45a721252..87ceef806 100644 --- a/src/logic/UntilFormula.h +++ b/src/logic/UntilFormula.h @@ -14,7 +14,8 @@ namespace storm { } virtual bool isUntilFormula() const override; - + virtual bool isValidProbabilityPathFormula() const override; + virtual std::shared_ptr substitute(std::map const& substitution) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 3b0d55ebf..56a65b39e 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -15,11 +15,13 @@ namespace storm { storm::logic::Formula const& formula = checkTask.getFormula(); STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); if (formula.isStateFormula()) { - return this->checkStateFormula(checkTask.replaceFormula(formula.asStateFormula())); + return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); } else if (formula.isPathFormula()) { - return this->computeProbabilities(checkTask.replaceFormula(formula.asPathFormula())); - } else if (formula.isRewardPathFormula()) { - return this->computeRewards(checkTask.replaceFormula(formula.asRewardPathFormula())); + if (checkTask.computeProbabilities()) { + return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula())); + } else if (checkTask.computeRewards()) { + return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula())); + } } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -27,17 +29,17 @@ namespace storm { std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); if (pathFormula.isBoundedUntilFormula()) { - return this->computeBoundedUntilProbabilities(checkTask.replaceFormula(pathFormula.asBoundedUntilFormula())); + return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(pathFormula.asBoundedUntilFormula())); } else if (pathFormula.isConditionalPathFormula()) { - return this->computeConditionalProbabilities(checkTask.replaceFormula(pathFormula.asConditionalPathFormula())); + return this->computeConditionalProbabilities(checkTask.substituteFormula(pathFormula.asConditionalPathFormula())); } else if (pathFormula.isEventuallyFormula()) { - return this->computeEventuallyProbabilities(checkTask.replaceFormula(pathFormula.asEventuallyFormula())); + return this->computeEventuallyProbabilities(checkTask.substituteFormula(pathFormula.asEventuallyFormula())); } else if (pathFormula.isGloballyFormula()) { - return this->computeGloballyProbabilities(checkTask.replaceFormula(pathFormula.asGloballyFormula())); + return this->computeGloballyProbabilities(checkTask.substituteFormula(pathFormula.asGloballyFormula())); } else if (pathFormula.isUntilFormula()) { - return this->computeUntilProbabilities(checkTask.replaceFormula(pathFormula.asUntilFormula())); + return this->computeUntilProbabilities(checkTask.substituteFormula(pathFormula.asUntilFormula())); } else if (pathFormula.isNextFormula()) { - return this->computeNextProbabilities(checkTask.replaceFormula(pathFormula.asNextFormula())); + return this->computeNextProbabilities(checkTask.substituteFormula(pathFormula.asNextFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); } @@ -53,7 +55,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); - return this->computeUntilProbabilities(checkTask.replaceFormula(newFormula)); + return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula)); } std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { @@ -68,16 +70,16 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { - storm::logic::RewardPathFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { + storm::logic::PathFormula const& rewardPathFormula = checkTask.getFormula(); if (rewardPathFormula.isCumulativeRewardFormula()) { - return this->computeCumulativeRewards(checkTask.replaceFormula(rewardPathFormula.asCumulativeRewardFormula())); + return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula())); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { - return this->computeInstantaneousRewards(checkTask.replaceFormula(rewardPathFormula.asInstantaneousRewardFormula())); - } else if (rewardPathFormula.isReachabilityRewardFormula()) { - return this->computeReachabilityRewards(checkTask.replaceFormula(rewardPathFormula.asReachabilityRewardFormula())); + return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula())); + } else if (rewardPathFormula.isEventuallyFormula()) { + return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula())); } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { - return this->computeLongRunAverageRewards(checkTask.replaceFormula(rewardPathFormula.asLongRunAverageRewardFormula())); + return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } @@ -90,7 +92,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } @@ -109,25 +111,25 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkStateFormula(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isBinaryBooleanStateFormula()) { - return this->checkBinaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asBinaryBooleanStateFormula())); + return this->checkBinaryBooleanStateFormula(checkTask.substituteFormula(stateFormula.asBinaryBooleanStateFormula())); } else if (stateFormula.isUnaryBooleanStateFormula()) { - return this->checkUnaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asUnaryBooleanStateFormula())); + return this->checkUnaryBooleanStateFormula(checkTask.substituteFormula(stateFormula.asUnaryBooleanStateFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula())); + return this->checkBooleanLiteralFormula(checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula())); } else if (stateFormula.isProbabilityOperatorFormula()) { - return this->checkProbabilityOperatorFormula(checkTask.replaceFormula(stateFormula.asProbabilityOperatorFormula())); + return this->checkProbabilityOperatorFormula(checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula())); } else if (stateFormula.isRewardOperatorFormula()) { - return this->checkRewardOperatorFormula(checkTask.replaceFormula(stateFormula.asRewardOperatorFormula())); + return this->checkRewardOperatorFormula(checkTask.substituteFormula(stateFormula.asRewardOperatorFormula())); } else if (stateFormula.isExpectedTimeOperatorFormula()) { - return this->checkExpectedTimeOperatorFormula(checkTask.replaceFormula(stateFormula.asExpectedTimeOperatorFormula())); + return this->checkExpectedTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asExpectedTimeOperatorFormula())); } else if (stateFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(checkTask.replaceFormula(stateFormula.asLongRunAverageOperatorFormula())); + return this->checkLongRunAverageOperatorFormula(checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula())); } else if (stateFormula.isAtomicExpressionFormula()) { - return this->checkAtomicExpressionFormula(checkTask.replaceFormula(stateFormula.asAtomicExpressionFormula())); + return this->checkAtomicExpressionFormula(checkTask.substituteFormula(stateFormula.asAtomicExpressionFormula())); } else if (stateFormula.isAtomicLabelFormula()) { - return this->checkAtomicLabelFormula(checkTask.replaceFormula(stateFormula.asAtomicLabelFormula())); + return this->checkAtomicLabelFormula(checkTask.substituteFormula(stateFormula.asAtomicLabelFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula())); + return this->checkBooleanLiteralFormula(checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } @@ -136,7 +138,7 @@ namespace storm { storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); std::stringstream stream; stream << stateFormula.getExpression(); - return this->checkAtomicLabelFormula(checkTask.replaceFormula(storm::logic::AtomicLabelFormula(stream.str()))); + return this->checkAtomicLabelFormula(checkTask.substituteFormula(storm::logic::AtomicLabelFormula(stream.str()))); } std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { @@ -147,8 +149,8 @@ namespace storm { storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr leftResult = this->check(checkTask.replaceFormula(stateFormula.getLeftSubformula().asStateFormula())); - std::unique_ptr rightResult = this->check(checkTask.replaceFormula(stateFormula.getRightSubformula().asStateFormula())); + std::unique_ptr leftResult = this->check(checkTask.substituteFormula(stateFormula.getLeftSubformula().asStateFormula())); + std::unique_ptr rightResult = this->check(checkTask.substituteFormula(stateFormula.getRightSubformula().asStateFormula())); STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results."); @@ -169,9 +171,9 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); - STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(stateFormula.getSubformula().isValidProbabilityPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asPathFormula())); + std::unique_ptr result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); @@ -183,9 +185,9 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula(); - STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(stateFormula.getSubformula().isValidRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeRewards(checkTask.replaceFormula(stateFormula.getSubformula().asRewardPathFormula())); + std::unique_ptr result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); @@ -199,7 +201,7 @@ namespace storm { storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeExpectedTimes(checkTask.replaceFormula(stateFormula.getSubformula().asEventuallyFormula())); + std::unique_ptr result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula())); if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); @@ -213,7 +215,7 @@ namespace storm { storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeLongRunAverageProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asStateFormula())); + std::unique_ptr result = this->computeLongRunAverageProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asStateFormula())); if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); @@ -225,7 +227,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask const& checkTask) { storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr subResult = this->check(checkTask.replaceFormula(stateFormula.getSubformula())); + std::unique_ptr subResult = this->check(checkTask.substituteFormula(stateFormula.getSubformula())); STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); if (stateFormula.isNot()) { subResult->asQualitativeCheckResult().complement(); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index a4ad1b6ac..f827c99ff 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -44,10 +44,10 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeRewards(CheckTask const& checkTask); virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask); virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask); - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask); virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask); // The methods to compute the long-run average and expected time. diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index be56e29e1..a780ef168 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -16,6 +16,10 @@ namespace storm { namespace modelchecker { + enum class CheckType { + Probabilities, Rewards + }; + /* * This class is used to customize the checking process of a formula. */ @@ -59,6 +63,8 @@ namespace storm { } } } else if (formula.isRewardOperatorFormula()) { + this->checkType = CheckType::Rewards; + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); @@ -75,8 +81,8 @@ namespace storm { * changes the formula type of the check task object. */ template - CheckTask replaceFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); + CheckTask substituteFormula(NewFormulaType const& newFormula) const { + return CheckTask(newFormula, this->checkType, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); } /*! @@ -85,6 +91,27 @@ namespace storm { FormulaType const& getFormula() const { return formula.get(); } + + /*! + * Retrieves whether probabilities are to be computed. + */ + bool computeProbabilities() const { + return checkType == CheckType::Probabilities; + } + + /*! + * Retrieves whether rewards are to be computed. + */ + bool computeRewards() const { + return checkType == CheckType::Rewards; + } + + /*! + * Retrieves the type of this task. + */ + CheckType getCheckType() const { + return checkType; + } /*! * Retrieves whether an optimization direction was set. @@ -184,6 +211,7 @@ namespace storm { * Creates a task object with the given options. * * @param formula The formula to attach to the task. + * @param checkType The type of task: whether to compute probabilities or rewards. * @param optimizationDirection If set, the probabilities will be minimized/maximized. * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values @@ -194,13 +222,16 @@ namespace storm { * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { + CheckTask(std::reference_wrapper const& formula, CheckType checkType, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), checkType(checkType), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } // The formula that is to be checked. std::reference_wrapper formula; + // A type indicating whether probabilities or rewards are to be computed. + CheckType checkType; + // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection; diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index a5eb27b27..412ab836c 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -25,7 +25,7 @@ namespace storm { template bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); + return formula.isCslStateFormula() || formula.isCslPathFormula(); } template @@ -54,9 +54,9 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index ace5b420b..d1e26bcb2 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -23,7 +23,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; protected: diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index b06cc2a54..e91547e81 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -32,7 +32,7 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); + return formula.isCslStateFormula() || formula.isCslPathFormula(); } template @@ -91,9 +91,9 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index d4e36071a..8def83dc7 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -26,7 +26,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index b33b01436..b5966bf4c 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula()); + return formula.isCslStateFormula() || formula.isCslPathFormula(); } template @@ -59,11 +59,11 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), 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()); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index e57f9d3e5..4e4f60850 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -23,7 +23,7 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeExpectedTimes(CheckTask const& checkTask) override; diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index c5e2225aa..b9b0bec0a 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -36,7 +36,7 @@ namespace storm { template bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + return formula.isPctlStateFormula() || formula.isPctlPathFormula(); } template @@ -91,9 +91,9 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 4d64f6f17..b723ea699 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -24,7 +24,7 @@ namespace storm { virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; protected: diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 6dfd0d83b..cd39e8c62 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -30,11 +30,11 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -100,10 +100,10 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), 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()); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 78612a378..ec3ef2955 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -31,7 +31,7 @@ namespace storm { virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) 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 d4bb73950..dce8a8138 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -34,14 +34,14 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { return true; } if (formula.isGloballyFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isConditionalPathFormula()) { storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); @@ -111,9 +111,9 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 77217a3ac..acc7d9283 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -27,7 +27,7 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 710d926a7..a7a56a890 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -39,11 +39,11 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -140,10 +140,10 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), 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()); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *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 1a0d85b2c..37cd6ef5b 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -25,7 +25,7 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 0053d6b77..2394a3176 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -32,11 +32,11 @@ namespace storm { template bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -102,9 +102,9 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index a7968a56a..3472ee1b0 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -21,7 +21,7 @@ namespace storm { virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) 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 30891afdf..9b74594dc 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -32,11 +32,11 @@ namespace storm { template bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -102,10 +102,10 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), 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()); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index 1baca69da..488971353 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -23,7 +23,7 @@ namespace storm { virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 554eba5e3..98afe49a1 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -83,9 +83,9 @@ namespace storm { bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); } else if (formula.isRewardOperatorFormula()) { - return this->canHandle(checkTask.replaceFormula(formula.asRewardOperatorFormula().getSubformula())); + return this->canHandle(checkTask.substituteFormula(formula.asRewardOperatorFormula().getSubformula())); } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { if (formula.isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); @@ -103,11 +103,6 @@ namespace storm { if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) { return true; } - } else if (formula.isReachabilityRewardFormula()) { - storm::logic::ReachabilityRewardFormula const& reachabilityRewardFormula = formula.asReachabilityRewardFormula(); - if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { - return true; - } } else if (formula.isConditionalPathFormula()) { storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { @@ -579,11 +574,11 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. - std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 809522260..af5b464be 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -26,7 +26,7 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index c919280b4..4bf036e4f 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -129,7 +129,6 @@ namespace storm { qi::rule(), Skipper> rewardPathFormula; qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> reachabilityRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; @@ -139,7 +138,6 @@ namespace storm { // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; std::shared_ptr createLongRunAverageRewardFormula() const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; @@ -255,10 +253,7 @@ namespace storm { cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)]; - reachabilityRewardFormula.name("reachability reward formula"); - - rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula; + rewardPathFormula = eventuallyFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula; rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -382,7 +377,6 @@ namespace storm { qi::on_error(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(reachabilityRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } @@ -411,10 +405,6 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { - return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); - } - std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); } diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index c8c47c5a8..902a69288 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -122,11 +122,6 @@ namespace storm { if (rightSubformula->isPropositionalFormula()) { measureDrivenInitialPartition = true; } - } else if (newFormula->isReachabilityRewardFormula()) { - rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer(); - if (rightSubformula->isPropositionalFormula()) { - measureDrivenInitialPartition = true; - } } if (measureDrivenInitialPartition) {