From 45e59848a9711e54e72e148de5a03ca340bac17d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 8 Mar 2016 17:01:17 +0100 Subject: [PATCH] first steps Former-commit-id: 12d930813b1b2856104f9ac32f1b9b1af09a251e --- src/logic/EventuallyFormula.cpp | 8 ++- src/logic/EventuallyFormula.h | 3 +- src/logic/ExpectedTimeOperatorFormula.cpp | 25 +++------ src/logic/ExpectedTimeOperatorFormula.h | 6 +-- src/logic/Formula.cpp | 22 +++++++- src/logic/Formula.h | 11 +++- src/logic/FragmentChecker.cpp | 10 ++-- src/logic/FragmentSpecification.cpp | 22 +++++--- src/logic/FragmentSpecification.h | 10 ++-- src/logic/LongRunAverageOperatorFormula.cpp | 25 +++------ src/logic/LongRunAverageOperatorFormula.h | 6 +-- src/logic/OperatorFormula.cpp | 44 +++++++++++---- src/logic/OperatorFormula.h | 26 +++++++-- src/logic/ProbabilityOperatorFormula.cpp | 25 +++------ src/logic/ProbabilityOperatorFormula.h | 6 +-- src/logic/RewardOperatorFormula.cpp | 25 +++------ src/logic/RewardOperatorFormula.h | 6 +-- src/modelchecker/AbstractModelChecker.cpp | 10 ++-- src/modelchecker/AbstractModelChecker.h | 2 +- src/parser/FormulaParser.cpp | 60 +++++++++++++-------- 20 files changed, 194 insertions(+), 158 deletions(-) diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index 71ff4ac54..67699cfb9 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -11,6 +11,10 @@ namespace storm { } bool EventuallyFormula::isEventuallyFormula() const { + return true; + } + + bool EventuallyFormula::isReachabilityProbabilityFormula() const { return context == FormulaContext::Probability; } @@ -18,7 +22,7 @@ namespace storm { return context == FormulaContext::Reward; } - bool EventuallyFormula::isReachbilityExpectedTimeFormula() const { + bool EventuallyFormula::isReachabilityExpectedTimeFormula() const { return context == FormulaContext::ExpectedTime; } @@ -31,7 +35,7 @@ namespace storm { } bool EventuallyFormula::isExpectedTimePathFormula() const { - return this->isReachbilityExpectedTimeFormula(); + return this->isReachabilityExpectedTimeFormula(); } boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index 5a0070a16..5cca412a9 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -15,8 +15,9 @@ namespace storm { } virtual bool isEventuallyFormula() const override; + virtual bool isReachabilityProbabilityFormula() const override; virtual bool isReachabilityRewardFormula() const override; - virtual bool isReachbilityExpectedTimeFormula() const override; + virtual bool isReachabilityExpectedTimeFormula() const override; virtual bool isProbabilityPathFormula() const override; virtual bool isRewardPathFormula() const override; virtual bool isExpectedTimePathFormula() const override; diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index 5dc8161ae..fb61b8bbd 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -2,22 +2,13 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) { - // Intentionally left empty. - } - - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) { - // Intentionally left empty. - } - - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), bound, subformula) { - // Intentionally left empty. - } - - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { - // Intentionally left empty. + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) { + STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in ET-operator."); } bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const { @@ -28,12 +19,8 @@ namespace storm { return visitor.visit(*this, data); } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { - // Intentionally left empty. - } - std::shared_ptr ExpectedTimeOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), this->operatorInformation); } std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index 5e1925b44..a6e7d3fbd 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -9,11 +9,7 @@ namespace storm { namespace logic { class ExpectedTimeOperatorFormula : public OperatorFormula { public: - ExpectedTimeOperatorFormula(std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation = OperatorInformation()); virtual ~ExpectedTimeOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 6c7084f53..3a14b7db8 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -62,6 +62,10 @@ namespace storm { return false; } + bool Formula::isReachabilityProbabilityFormula() const { + return false; + } + bool Formula::isGloballyFormula() const { return false; } @@ -122,7 +126,7 @@ namespace storm { return false; } - bool Formula::isReachbilityExpectedTimeFormula() const { + bool Formula::isReachabilityExpectedTimeFormula() const { return false; } @@ -264,6 +268,22 @@ namespace storm { return dynamic_cast(*this); } + EventuallyFormula& Formula::asReachabilityProbabilityFormula() { + return dynamic_cast(*this); + } + + EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const { + return dynamic_cast(*this); + } + + EventuallyFormula& Formula::asReachabilityExpectedTimeFormula() { + return dynamic_cast(*this); + } + + EventuallyFormula const& Formula::asReachabilityExpectedTimeFormula() const { + return dynamic_cast(*this); + } + GloballyFormula& Formula::asGloballyFormula() { return dynamic_cast(*this); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 7d77de7b3..f7916f400 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -65,8 +65,9 @@ namespace storm { virtual bool isNextFormula() const; virtual bool isUntilFormula() const; virtual bool isBoundedUntilFormula() const; - virtual bool isEventuallyFormula() const; virtual bool isGloballyFormula() const; + virtual bool isEventuallyFormula() const; + virtual bool isReachabilityProbabilityFormula() const; // Reward formulas. virtual bool isCumulativeRewardFormula() const; @@ -75,7 +76,7 @@ namespace storm { virtual bool isLongRunAverageRewardFormula() const; // Expected time formulas. - virtual bool isReachbilityExpectedTimeFormula() const; + virtual bool isReachabilityExpectedTimeFormula() const; // Type checks for abstract intermediate classes. virtual bool isBinaryPathFormula() const; @@ -126,8 +127,14 @@ namespace storm { EventuallyFormula& asEventuallyFormula(); EventuallyFormula const& asEventuallyFormula() const; + EventuallyFormula& asReachabilityProbabilityFormula(); + EventuallyFormula const& asReachabilityProbabilityFormula() const; + EventuallyFormula& asReachabilityRewardFormula(); EventuallyFormula const& asReachabilityRewardFormula() const; + + EventuallyFormula& asReachabilityExpectedTimeFormula(); + EventuallyFormula const& asReachabilityExpectedTimeFormula() const; GloballyFormula& asGloballyFormula(); GloballyFormula const& asGloballyFormula() const; diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 6bf03ddb7..fb400fc5b 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -73,7 +73,7 @@ namespace storm { } if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) { if (f.isConditionalProbabilityFormula()) { - result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula(); + result = result && f.getSubformula().isReachabilityProbabilityFormula() && f.getConditionFormula().isReachabilityProbabilityFormula(); } else if (f.isConditionalRewardFormula()) { result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula(); } @@ -91,15 +91,15 @@ namespace storm { boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = true; - if (f.isEventuallyFormula()) { - result = inherited.getSpecification().areEventuallyFormulasAllowed(); + if (f.isReachabilityProbabilityFormula()) { + result = inherited.getSpecification().areReachabilityProbabilityFormulasAllowed(); if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { result = result && !f.getSubformula().isPathFormula(); } } else if (f.isReachabilityRewardFormula()) { result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed(); result = result && f.getSubformula().isStateFormula(); - } else if (f.isReachbilityExpectedTimeFormula()) { + } else if (f.isReachabilityExpectedTimeFormula()) { result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed(); result = result && f.getSubformula().isStateFormula(); } @@ -111,6 +111,7 @@ namespace storm { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed(); result = result && f.getSubformula().isExpectedTimePathFormula(); + result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { @@ -177,6 +178,7 @@ namespace storm { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areRewardOperatorsAllowed(); result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); + result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index 378fe3a88..e243562e8 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -22,7 +22,7 @@ namespace storm { pctl.setProbabilityOperatorsAllowed(true); pctl.setGloballyFormulasAllowed(true); - pctl.setEventuallyFormulasAllowed(true); + pctl.setReachabilityProbabilityFormulasAllowed(true); pctl.setNextFormulasAllowed(true); pctl.setUntilFormulasAllowed(true); pctl.setBoundedUntilFormulasAllowed(true); @@ -70,7 +70,7 @@ namespace storm { longRunAverageOperator = false; globallyFormula = false; - eventuallyFormula = false; + reachabilityProbabilityFormula = false; nextFormula = false; untilFormula = false; boundedUntilFormula = false; @@ -96,6 +96,7 @@ namespace storm { onlyEventuallyFormuluasInConditionalFormulas = true; stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; + varianceAsMeasureType = false; } FragmentSpecification FragmentSpecification::copy() const { @@ -147,12 +148,12 @@ namespace storm { return *this; } - bool FragmentSpecification::areEventuallyFormulasAllowed() const { - return eventuallyFormula; + bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const { + return reachabilityProbabilityFormula; } - FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) { - this->eventuallyFormula = newValue; + FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) { + this->reachabilityProbabilityFormula = newValue; return *this; } @@ -355,5 +356,14 @@ namespace storm { return *this; } + bool FragmentSpecification::isVarianceMeasureTypeAllowed() const { + return varianceAsMeasureType; + } + + FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) { + this->varianceAsMeasureType = newValue; + return *this; + } + } } \ No newline at end of file diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index 1bd46f4f7..e850fb172 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -28,8 +28,8 @@ namespace storm { bool areGloballyFormulasAllowed() const; FragmentSpecification& setGloballyFormulasAllowed(bool newValue); - bool areEventuallyFormulasAllowed() const; - FragmentSpecification& setEventuallyFormulasAllowed(bool newValue); + bool areReachabilityProbabilityFormulasAllowed() const; + FragmentSpecification& setReachabilityProbabilityFormulasAllowed(bool newValue); bool areNextFormulasAllowed() const; FragmentSpecification& setNextFormulasAllowed(bool newValue); @@ -91,6 +91,9 @@ namespace storm { bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); + bool isVarianceMeasureTypeAllowed() const; + FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setExpectedTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -103,7 +106,7 @@ namespace storm { bool longRunAverageOperator; bool globallyFormula; - bool eventuallyFormula; + bool reachabilityProbabilityFormula; bool nextFormula; bool untilFormula; bool boundedUntilFormula; @@ -130,6 +133,7 @@ namespace storm { bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; + bool varianceAsMeasureType; }; // Propositional. diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index c9d781905..fe261224c 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -2,24 +2,15 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) { - // Intentionally left empty. - } - - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) { - // Intentionally left empty. - } - - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), bound, subformula) { - // Intentionally left empty. + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) { + STORM_LOG_THROW(this->getMeasureType() == MeasureType::Value, storm::exceptions::InvalidPropertyException, "Invalid measure type in LRA-operator."); } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { - // Intentionally left empty. - } - bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const { return true; } @@ -28,12 +19,8 @@ namespace storm { return visitor.visit(*this, data); } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { - // Intentionally left empty. - } - std::shared_ptr LongRunAverageOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), this->operatorInformation); } std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index d4a785b80..394188b67 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -7,11 +7,7 @@ namespace storm { namespace logic { class LongRunAverageOperatorFormula : public OperatorFormula { public: - LongRunAverageOperatorFormula(std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation = OperatorInformation()); virtual ~LongRunAverageOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index a9cdc09ae..97690d7bf 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,44 +2,67 @@ namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) { + std::ostream& operator<<(std::ostream& out, MeasureType const& type) { + switch (type) { + case MeasureType::Value: + out << "val"; + break; + case MeasureType::Expectation: + out << "exp"; + break; + case MeasureType::Variance: + out << "var"; + break; + } + return out; + } + + OperatorInformation::OperatorInformation(MeasureType const& measureType, boost::optional const& optimizationDirection, boost::optional> const& bound) : measureType(measureType), optimalityType(optimizationDirection), bound(bound) { + // Intentionally left empty. + } + + OperatorFormula::OperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation) : UnaryStateFormula(subformula), operatorInformation(operatorInformation) { // Intentionally left empty. } bool OperatorFormula::hasBound() const { - return static_cast(bound); + return static_cast(operatorInformation.bound); } ComparisonType OperatorFormula::getComparisonType() const { - return bound.get().comparisonType; + return operatorInformation.bound.get().comparisonType; } void OperatorFormula::setComparisonType(ComparisonType newComparisonType) { - bound.get().comparisonType = newComparisonType; + operatorInformation.bound.get().comparisonType = newComparisonType; } double OperatorFormula::getThreshold() const { - return bound.get().threshold; + return operatorInformation.bound.get().threshold; } void OperatorFormula::setThreshold(double newThreshold) { - bound.get().threshold = newThreshold; + operatorInformation.bound.get().threshold = newThreshold; } Bound const& OperatorFormula::getBound() const { - return bound.get(); + return operatorInformation.bound.get(); } void OperatorFormula::setBound(Bound const& newBound) { - bound = newBound; + operatorInformation.bound = newBound; } bool OperatorFormula::hasOptimalityType() const { - return static_cast(optimalityType); + return static_cast(operatorInformation.optimalityType); } OptimizationDirection const& OperatorFormula::getOptimalityType() const { - return optimalityType.get(); + return operatorInformation.optimalityType.get(); + } + + MeasureType OperatorFormula::getMeasureType() const { + return operatorInformation.measureType; } bool OperatorFormula::isOperatorFormula() const { @@ -47,6 +70,7 @@ namespace storm { } std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { + out << "[" << this->operatorInformation.measureType << "]"; if (hasOptimalityType()) { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 7660799a4..43c97ea45 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -9,14 +9,27 @@ namespace storm { namespace logic { + enum class MeasureType { Value, Expectation, Variance }; + + std::ostream& operator<<(std::ostream& out, MeasureType const& type); + + struct OperatorInformation { + OperatorInformation(MeasureType const& measureType = MeasureType::Value, boost::optional const& optimizationDirection = boost::none, boost::optional> const& bound = boost::none); + + MeasureType measureType; + boost::optional optimalityType; + boost::optional> bound; + }; + class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); + OperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation = OperatorInformation()); virtual ~OperatorFormula() { // Intentionally left empty. } - + + // Bound-related accessors. bool hasBound() const; ComparisonType getComparisonType() const; void setComparisonType(ComparisonType newComparisonType); @@ -24,16 +37,19 @@ namespace storm { void setThreshold(double newThreshold); Bound const& getBound() const; void setBound(Bound const& newBound); + + // Optimality-type-related accessors. bool hasOptimalityType() const; storm::solver::OptimizationDirection const& getOptimalityType() const; virtual bool isOperatorFormula() const override; + // Measure-type-related accessors. + MeasureType getMeasureType() const; + virtual std::ostream& writeToStream(std::ostream& out) const override; protected: - std::string operatorSymbol; - boost::optional> bound; - boost::optional optimalityType; + OperatorInformation operatorInformation; }; } } diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index 09680cbc5..b3f7a303c 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -2,22 +2,13 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) { - // Intentionally left empty. - } - - ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) { - // Intentionally left empty. - } - - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), bound, subformula) { - // Intentionally left empty. - } - - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { - // Intentionally left empty. + ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) { + STORM_LOG_THROW(this->getMeasureType() == MeasureType::Value, storm::exceptions::InvalidPropertyException, "Invalid measure type in P-operator."); } bool ProbabilityOperatorFormula::isProbabilityOperatorFormula() const { @@ -27,13 +18,9 @@ namespace storm { boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { - // Intentionally left empty. - } std::shared_ptr ProbabilityOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), this->operatorInformation); } std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 1172247d0..786d58b44 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -7,11 +7,7 @@ namespace storm { namespace logic { class ProbabilityOperatorFormula : public OperatorFormula { public: - ProbabilityOperatorFormula(std::shared_ptr const& subformula); - ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(std::shared_ptr const& subformula, OperatorInformation const& operatorInformation = OperatorInformation()); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 711f78789..cb5a6dc80 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -2,22 +2,13 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) { - // Intentionally left empty. - } - - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) { - // Intentionally left empty. - } - - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), bound, subformula) { - // Intentionally left empty. - } - - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::none, subformula) { - // Intentionally left empty. + RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr const& subformula, boost::optional const& rewardModelName, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation), rewardModelName(rewardModelName) { + STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in R-operator."); } bool RewardOperatorFormula::isRewardOperatorFormula() const { @@ -49,12 +40,8 @@ namespace storm { this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) { - // Intentionally left empty. - } - std::shared_ptr RewardOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), this->rewardModelName, this->operatorInformation); } std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 6bcf015d8..e371ee0b9 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -8,11 +8,7 @@ namespace storm { namespace logic { class RewardOperatorFormula : public OperatorFormula { public: - RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); + RewardOperatorFormula(std::shared_ptr const& subformula, boost::optional const& rewardModelName = boost::none, OperatorInformation const& operatorInformation = OperatorInformation()); virtual ~RewardOperatorFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index ebd760d2e..f79fa373b 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -34,8 +34,8 @@ namespace storm { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula())); - } else if (formula.isEventuallyFormula()) { - return this->computeEventuallyProbabilities(checkTask.substituteFormula(formula.asEventuallyFormula())); + } else if (formula.isReachabilityProbabilityFormula()) { + return this->computeReachabilityProbabilities(checkTask.substituteFormula(formula.asReachabilityProbabilityFormula())); } else if (formula.isGloballyFormula()) { return this->computeGloballyProbabilities(checkTask.substituteFormula(formula.asGloballyFormula())); } else if (formula.isUntilFormula()) { @@ -56,7 +56,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeReachabilityProbabilities(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.substituteFormula(newFormula)); @@ -81,7 +81,7 @@ namespace storm { } else if (rewardFormula.isInstantaneousRewardFormula()) { return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula())); } else if (rewardFormula.isReachabilityRewardFormula()) { - return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula())); + return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula())); } else if (rewardFormula.isLongRunAverageRewardFormula()) { return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); } else if (rewardFormula.isConditionalRewardFormula()) { @@ -205,7 +205,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask const& checkTask) { storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula(); - STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityExpectedTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); std::unique_ptr result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula())); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 90562659b..c63f00a3c 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -38,7 +38,7 @@ namespace storm { virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeEventuallyProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index d8fa100c8..7a78b797b 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -88,6 +88,18 @@ namespace storm { // A parser used for recognizing the optimality operators. optimalityOperatorStruct optimalityOperator_; + struct measureTypeStruct : qi::symbols { + measureTypeStruct() { + add + ("val", storm::logic::MeasureType::Value) + ("exp", storm::logic::MeasureType::Expectation) + ("var", storm::logic::MeasureType::Variance); + } + }; + + // A parser used for recognizing the measure types. + measureTypeStruct measureType_; + // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; @@ -97,7 +109,8 @@ namespace storm { qi::rule>(), Skipper> start; - qi::rule, boost::optional>>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule measureType; qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> expectedTimeOperator; @@ -147,11 +160,11 @@ namespace storm { std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; - std::pair, boost::optional>> createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula); + storm::logic::OperatorInformation createOperatorInformation(storm::logic::MeasureType const& measureType, boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; + std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); @@ -301,22 +314,25 @@ namespace storm { pathFormula = conditionalFormula(qi::_r1); 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)]; + measureType = qi::lit("[") >> measureType_ >> qi::lit("]"); + measureType.name("measure type"); + + operatorInformation = qi::eps[qi::_a = qi::_r1] >> (-measureType[qi::_a = qi::_1] >> -optimalityOperator_[qi::_b = qi::_1] >> ((relationalOperator_[qi::_c = qi::_1] > qi::double_[qi::_d = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)]; operatorInformation.name("operator information"); - longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation(storm::logic::MeasureType::Value) > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; longRunAverageOperator.name("long-run average operator"); rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); rewardModelName.name("reward model name"); - 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 = (qi::lit("R") > -rewardModelName > operatorInformation(storm::logic::MeasureType::Expectation) > 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(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + expectedTimeOperator = (qi::lit("ET") > operatorInformation(storm::logic::MeasureType::Expectation) > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > 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(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + probabilityOperator = (qi::lit("P") > operatorInformation(storm::logic::MeasureType::Value) > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; probabilityOperator.name("probability operator"); andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; @@ -459,28 +475,28 @@ namespace storm { return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); } - std::pair, boost::optional>> FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { + storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(storm::logic::MeasureType const& measureType, boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { - return std::make_pair(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get())); + return storm::logic::OperatorInformation(measureType, optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get())); } else { - return std::make_pair(optimizationDirection, boost::none); + return storm::logic::OperatorInformation(measureType, optimizationDirection, boost::none); } } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula)); + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(subformula, operatorInformation)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); } std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {