diff --git a/src/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp index 6747d2ab5..35c7149b0 100644 --- a/src/logic/AtomicExpressionFormula.cpp +++ b/src/logic/AtomicExpressionFormula.cpp @@ -13,6 +13,10 @@ namespace storm { bool AtomicExpressionFormula::isPctlStateFormula() const { return true; } + + bool AtomicExpressionFormula::isPctlWithConditionalStateFormula() const { + return true; + } bool AtomicExpressionFormula::isLtlFormula() const { return true; diff --git a/src/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h index f054c9e42..2b2e36dd5 100644 --- a/src/logic/AtomicExpressionFormula.h +++ b/src/logic/AtomicExpressionFormula.h @@ -16,6 +16,7 @@ namespace storm { virtual bool isAtomicExpressionFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isLtlFormula() const override; virtual bool isPropositionalFormula() const override; diff --git a/src/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp index 0555ff56a..36c00eb23 100644 --- a/src/logic/AtomicLabelFormula.cpp +++ b/src/logic/AtomicLabelFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return true; } + bool AtomicLabelFormula::isPctlWithConditionalStateFormula() const { + return true; + } + bool AtomicLabelFormula::isLtlFormula() const { return true; } diff --git a/src/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h index 8cd2f51f1..3d326c211 100644 --- a/src/logic/AtomicLabelFormula.h +++ b/src/logic/AtomicLabelFormula.h @@ -18,6 +18,7 @@ namespace storm { virtual bool isAtomicLabelFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isLtlFormula() const override; virtual bool isPropositionalFormula() const override; diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index 949dbf378..5075894c4 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); } + bool BinaryPathFormula::isPctlWithConditionalPathFormula() const { + return this->getLeftSubformula().isPctlWithConditionalPathFormula() && this->getRightSubformula().isPctlWithConditionalPathFormula(); + } + bool BinaryPathFormula::isCslPathFormula() const { return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); } diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index 928d21728..14d162926 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -18,6 +18,7 @@ namespace storm { virtual bool isBinaryPathFormula() const override; virtual bool isPctlPathFormula() const override; + virtual bool isPctlWithConditionalPathFormula() const override; virtual bool isCslPathFormula() const override; virtual bool isLtlFormula() const override; virtual bool containsBoundedUntilFormula() const override; diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index 6993707ad..bcaa2d39b 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -13,6 +13,10 @@ namespace storm { bool BinaryStateFormula::isPctlStateFormula() const { return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); } + + bool BinaryStateFormula::isPctlWithConditionalStateFormula() const { + return this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula(); + } bool BinaryStateFormula::isCslStateFormula() const { return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index a0fcbc9d1..c259aa759 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -16,6 +16,7 @@ namespace storm { virtual bool isBinaryStateFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isCslStateFormula() const override; virtual bool isLtlFormula() const override; virtual bool containsBoundedUntilFormula() const override; diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp index aa78a6772..d021bbc64 100644 --- a/src/logic/BooleanLiteralFormula.cpp +++ b/src/logic/BooleanLiteralFormula.cpp @@ -18,6 +18,10 @@ namespace storm { return true; } + bool BooleanLiteralFormula::isPctlWithConditionalStateFormula() const { + return true; + } + bool BooleanLiteralFormula::isLtlFormula() const { return true; } diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h index d8df08651..1283fde71 100644 --- a/src/logic/BooleanLiteralFormula.h +++ b/src/logic/BooleanLiteralFormula.h @@ -18,6 +18,7 @@ namespace storm { virtual bool isFalseFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isLtlFormula() const override; virtual bool isPropositionalFormula() const override; diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp index 7c29c579b..9a1f867e1 100644 --- a/src/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -38,6 +38,10 @@ namespace storm { return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); } + bool BoundedUntilFormula::isPctlWithConditionalPathFormula() const { + return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula(); + } + bool BoundedUntilFormula::isCslPathFormula() const { return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); } diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h index 7da7e70f6..bc14d8def 100644 --- a/src/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -23,6 +23,7 @@ namespace storm { uint_fast64_t getDiscreteTimeBound() const; virtual bool isValidProbabilityPathFormula() const override; + virtual bool isPctlWithConditionalPathFormula() 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 8ef461e35..676a83185 100644 --- a/src/logic/ConditionalPathFormula.cpp +++ b/src/logic/ConditionalPathFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { + ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, bool isRewardFormula) : BinaryPathFormula(leftSubformula, rightSubformula), isRewardFormula(isRewardFormula) { // Intentionally left empty. } @@ -14,6 +14,18 @@ namespace storm { return true; } + bool ConditionalPathFormula::isPctlWithConditionalPathFormula() const { + return this->getLeftSubformula().isPctlPathFormula() && this->getRightSubformula().isPctlPathFormula(); + } + + bool ConditionalPathFormula::isRewardPathFormula() const { + return this->isRewardFormula && this->isValidRewardPathFormula(); + } + + bool ConditionalPathFormula::isValidRewardPathFormula() const { + return this->getLeftSubformula().isRewardPathFormula() && !this->getLeftSubformula().isConditionalPathFormula() && this->getRightSubformula().isPctlPathFormula(); + } + std::shared_ptr<Formula> ConditionalPathFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const { return std::make_shared<ConditionalPathFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution)); } diff --git a/src/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h index a3e12e20f..94053606b 100644 --- a/src/logic/ConditionalPathFormula.h +++ b/src/logic/ConditionalPathFormula.h @@ -7,18 +7,24 @@ namespace storm { namespace logic { class ConditionalPathFormula : public BinaryPathFormula { public: - ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula); + ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, bool isRewardFormula = false); virtual ~ConditionalPathFormula() { // Intentionally left empty. } + virtual bool isPctlWithConditionalPathFormula() const override; + virtual bool isRewardPathFormula() const override; virtual bool isConditionalPathFormula() 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<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override; + + private: + bool isRewardFormula; }; } } diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp index 3f53c2e9d..2a00c04f3 100644 --- a/src/logic/CumulativeRewardFormula.cpp +++ b/src/logic/CumulativeRewardFormula.cpp @@ -10,6 +10,10 @@ namespace storm { // Intentionally left empty. } + bool CumulativeRewardFormula::isRewardPathFormula() const { + return true; + } + bool CumulativeRewardFormula::isCumulativeRewardFormula() const { return true; } diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h index 4ebf08cd4..0192a8a49 100644 --- a/src/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -17,6 +17,7 @@ namespace storm { // Intentionally left empty. } + virtual bool isRewardPathFormula() const override; virtual bool isCumulativeRewardFormula() const override; virtual bool isValidRewardPathFormula() const override; diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index a25d12b33..8b09281cd 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) { + EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula) : UnaryPathFormula(subformula), isRewardFormula(isRewardFormula) { // Intentionally left empty. } @@ -10,12 +10,16 @@ namespace storm { return true; } + bool EventuallyFormula::isRewardPathFormula() const { + return isRewardFormula; + } + bool EventuallyFormula::isValidProbabilityPathFormula() const { - return true; + return !isRewardFormula; } bool EventuallyFormula::isValidRewardPathFormula() const { - return true; + return isRewardFormula; } std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const { diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index a488eb443..3b121d320 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -7,13 +7,14 @@ namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { public: - EventuallyFormula(std::shared_ptr<Formula const> const& subformula); + EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula = false); virtual ~EventuallyFormula() { // Intentionally left empty. } virtual bool isEventuallyFormula() const override; + virtual bool isRewardPathFormula() const override; virtual bool isValidProbabilityPathFormula() const override; virtual bool isValidRewardPathFormula() const override; @@ -21,6 +22,8 @@ namespace storm { virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override; + private: + bool isRewardFormula; }; } } diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index ed21be228..8165710a1 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -26,6 +26,10 @@ namespace storm { return this->getSubformula().isPctlStateFormula(); } + bool ExpectedTimeOperatorFormula::isPctlWithConditionalStateFormula() const { + return this->getSubformula().isPctlWithConditionalStateFormula(); + } + bool ExpectedTimeOperatorFormula::containsProbabilityOperator() const { return this->getSubformula().containsProbabilityOperator(); } diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index 5702610c2..162fb39f8 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -20,6 +20,7 @@ namespace storm { virtual bool isExpectedTimeOperatorFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index e3fa84c74..9f9151b84 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -111,6 +111,22 @@ namespace storm { return false; } + bool Formula::isPctlFormula() const { + return this->isPctlStateFormula() || this->isPctlPathFormula(); + } + + bool Formula::isPctlWithConditionalFormula() const { + return this->isPctlWithConditionalStateFormula() || this->isPctlWithConditionalPathFormula(); + } + + bool Formula::isRewardFormula() const { + return this->isRewardStateFormula() || this->isRewardPathFormula(); + } + + bool Formula::isCslFormula() const { + return this->isCslStateFormula() || this->isCslPathFormula(); + } + bool Formula::isPctlPathFormula() const { return false; } @@ -119,6 +135,14 @@ namespace storm { return false; } + bool Formula::isPctlWithConditionalPathFormula() const { + return false; + } + + bool Formula::isPctlWithConditionalStateFormula() const { + return false; + } + bool Formula::isCslPathFormula() const { return this->isPctlPathFormula(); } @@ -127,6 +151,14 @@ namespace storm { return this->isPctlStateFormula(); } + bool Formula::isRewardPathFormula() const { + return false; + } + + bool Formula::isRewardStateFormula() const { + return false; + } + bool Formula::isPltlFormula() const { return false; } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 2ea234449..cf4333eb4 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -79,10 +79,18 @@ namespace storm { virtual bool isRewardOperatorFormula() const; virtual bool isOperatorFormula() const; + bool isPctlFormula() const; + bool isPctlWithConditionalFormula() const; + bool isRewardFormula() const; + bool isCslFormula() const; virtual bool isPctlPathFormula() const; virtual bool isPctlStateFormula() const; + virtual bool isPctlWithConditionalPathFormula() const; + virtual bool isPctlWithConditionalStateFormula() const; virtual bool isCslPathFormula() const; virtual bool isCslStateFormula() const; + virtual bool isRewardPathFormula() const; + virtual bool isRewardStateFormula() const; virtual bool isPltlFormula() const; virtual bool isLtlFormula() const; virtual bool isPropositionalFormula() const; diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp index 77efb5705..7289f18e9 100644 --- a/src/logic/InstantaneousRewardFormula.cpp +++ b/src/logic/InstantaneousRewardFormula.cpp @@ -18,6 +18,10 @@ namespace storm { return true; } + bool InstantaneousRewardFormula::isRewardPathFormula() const { + return true; + } + bool InstantaneousRewardFormula::hasDiscreteTimeBound() const { return timeBound.which() == 0; } diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h index c895c5b39..967f03a2b 100644 --- a/src/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -17,6 +17,7 @@ namespace storm { // Intentionally left empty. } + virtual bool isRewardPathFormula() const override; virtual bool isInstantaneousRewardFormula() const override; virtual bool isValidRewardPathFormula() const override; diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index cfeb30692..1563dc67e 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -26,6 +26,10 @@ namespace storm { return this->getSubformula().isPctlStateFormula(); } + bool LongRunAverageOperatorFormula::isPctlWithConditionalStateFormula() const { + return this->getSubformula().isPctlWithConditionalStateFormula(); + } + bool LongRunAverageOperatorFormula::containsProbabilityOperator() const { return this->getSubformula().containsProbabilityOperator(); } diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 89e119f48..85eb9f969 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -20,6 +20,7 @@ namespace storm { virtual bool isLongRunAverageOperatorFormula() const override; virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; diff --git a/src/logic/LongRunAverageRewardFormula.cpp b/src/logic/LongRunAverageRewardFormula.cpp index 7bc064c1e..9d9dc898d 100644 --- a/src/logic/LongRunAverageRewardFormula.cpp +++ b/src/logic/LongRunAverageRewardFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return true; } + bool LongRunAverageRewardFormula::isRewardPathFormula() const { + return true; + } + std::shared_ptr<Formula> LongRunAverageRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const { return std::shared_ptr<Formula>(new LongRunAverageRewardFormula()); } diff --git a/src/logic/LongRunAverageRewardFormula.h b/src/logic/LongRunAverageRewardFormula.h index aa4d3f424..929a6f3c8 100644 --- a/src/logic/LongRunAverageRewardFormula.h +++ b/src/logic/LongRunAverageRewardFormula.h @@ -13,6 +13,7 @@ namespace storm { // Intentionally left empty. } + virtual bool isRewardPathFormula() const override; virtual bool isLongRunAverageRewardFormula() const override; virtual bool isValidRewardPathFormula() const override; diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index 1f4615556..cb584b034 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -26,6 +26,10 @@ namespace storm { return this->getSubformula().isPctlPathFormula(); } + bool ProbabilityOperatorFormula::isPctlWithConditionalStateFormula() const { + return this->getSubformula().isPctlWithConditionalPathFormula(); + } + bool ProbabilityOperatorFormula::isCslStateFormula() const { return this->getSubformula().isCslPathFormula(); } diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 8bae11548..163e05f58 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -18,6 +18,7 @@ namespace storm { } virtual bool isPctlStateFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isCslStateFormula() const override; virtual bool isPltlFormula() const override; virtual bool containsProbabilityOperator() const override; diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 1e5390830..0eea0eedc 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -22,9 +22,8 @@ namespace storm { return true; } - bool RewardOperatorFormula::isPctlStateFormula() const { - Formula const& subformula = this->getSubformula(); - return subformula.isEventuallyFormula() || subformula.isCumulativeRewardFormula() || subformula.isInstantaneousRewardFormula(); + bool RewardOperatorFormula::isRewardStateFormula() const { + return this->getSubformula().isRewardPathFormula(); } bool RewardOperatorFormula::containsRewardOperator() const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 9e90ef01f..0cbfe955e 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -19,8 +19,8 @@ namespace storm { } virtual bool isRewardOperatorFormula() const override; + virtual bool isRewardStateFormula() const override; - virtual bool isPctlStateFormula() const override; virtual bool containsRewardOperator() const override; virtual bool containsNestedRewardOperators() const override; diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index d961f1612..01ccadde8 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -14,6 +14,10 @@ namespace storm { return this->getSubformula().isPctlStateFormula(); } + bool UnaryPathFormula::isPctlWithConditionalPathFormula() const { + return this->getSubformula().isPctlWithConditionalStateFormula(); + } + bool UnaryPathFormula::isLtlFormula() const { return this->getSubformula().isLtlFormula(); } diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index 8d168585c..be60edbd9 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -18,6 +18,7 @@ namespace storm { virtual bool isUnaryPathFormula() const override; virtual bool isPctlPathFormula() const override; + virtual bool isPctlWithConditionalPathFormula() const override; virtual bool isLtlFormula() const override; virtual bool containsBoundedUntilFormula() const override; virtual bool containsNextFormula() const override; diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index 4bf651aa1..a57b86b1e 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -18,6 +18,10 @@ namespace storm { return this->getSubformula().isPctlStateFormula(); } + bool UnaryStateFormula::isPctlWithConditionalStateFormula() const { + return this->getSubformula().isPctlWithConditionalStateFormula(); + } + bool UnaryStateFormula::isLtlFormula() const { return this->getSubformula().isLtlFormula(); } diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 745687e6b..8b5539a88 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -16,6 +16,7 @@ namespace storm { virtual bool isUnaryStateFormula() const override; virtual bool isPropositionalFormula() const override; + virtual bool isPctlWithConditionalStateFormula() const override; virtual bool isPctlStateFormula() const override; virtual bool isLtlFormula() const override; virtual bool containsBoundedUntilFormula() const override; diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 412ab836c..c6b7c9d1e 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -25,7 +25,7 @@ namespace storm { template<storm::dd::DdType DdType, class ValueType> bool HybridCtmcCslModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula(); + return formula.isCslFormula() || formula.isRewardFormula(); } template<storm::dd::DdType DdType, class ValueType> diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 4bf036e4f..1298b3fa2 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -120,8 +120,8 @@ namespace storm { qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expressionFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula; - qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> conditionalFormula; - qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> eventuallyFormula; + qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(bool), Skipper> conditionalFormula; + qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(bool), Skipper> eventuallyFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> nextFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> globallyFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> untilFormula; @@ -142,11 +142,11 @@ namespace storm { std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const; std::shared_ptr<storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& subformula) const; + std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr<storm::logic::Formula> const& subformula) const; std::shared_ptr<storm::logic::Formula> createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const; std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const; std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula); - std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const; + std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, bool reward) const; std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const; std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const; std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const; @@ -253,7 +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"); - rewardPathFormula = eventuallyFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula; + rewardPathFormula = eventuallyFormula(true) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(true); rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -277,7 +277,7 @@ namespace storm { notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; notStateFormula.name("negation formula"); - eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; @@ -286,19 +286,19 @@ namespace storm { nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - pathFormulaWithoutUntil = eventuallyFormula | globallyFormula | nextFormula | stateFormula; + pathFormulaWithoutUntil = eventuallyFormula(false) | globallyFormula | nextFormula | stateFormula; pathFormulaWithoutUntil.name("path formula"); untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); - conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)]; + conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; timeBound.name("time bound"); - pathFormula = conditionalFormula; + pathFormula = conditionalFormula(false); 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::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; @@ -313,7 +313,7 @@ namespace storm { rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; rewardOperator.name("reward operator"); - expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(true) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; expectedTimeOperator.name("expected time operator"); probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -422,7 +422,7 @@ namespace storm { return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& subformula) const { + std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr<storm::logic::Formula> const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get()); @@ -431,7 +431,7 @@ namespace storm { return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get())))); } } else { - return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula)); + return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula, reward)); } } @@ -456,8 +456,8 @@ namespace storm { } } - std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const { - return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); + std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, bool reward) const { + return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula, reward)); } std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {