From 5427702376dfab4c8d46e133f5bb4c4c193aa7bb Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:05 +0200 Subject: [PATCH] WIP:needed? Boolean path formulas: allow storing context --- src/storm/logic/BinaryBooleanPathFormula.cpp | 11 ++++++++++- src/storm/logic/BinaryBooleanPathFormula.h | 7 ++++++- src/storm/logic/UnaryBooleanPathFormula.cpp | 11 ++++++++++- src/storm/logic/UnaryBooleanPathFormula.h | 7 ++++++- 4 files changed, 32 insertions(+), 4 deletions(-) diff --git a/src/storm/logic/BinaryBooleanPathFormula.cpp b/src/storm/logic/BinaryBooleanPathFormula.cpp index aa84f23f7..b759db23b 100644 --- a/src/storm/logic/BinaryBooleanPathFormula.cpp +++ b/src/storm/logic/BinaryBooleanPathFormula.cpp @@ -7,15 +7,24 @@ namespace storm { namespace logic { - BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula), operatorType(operatorType) { + BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, FormulaContext context) : BinaryPathFormula(leftSubformula, rightSubformula), operatorType(operatorType), context(context) { STORM_LOG_THROW(this->getLeftSubformula().isStateFormula() || this->getLeftSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); STORM_LOG_THROW(this->getRightSubformula().isStateFormula() || this->getRightSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); + STORM_LOG_THROW(context == FormulaContext::Probability, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); } + FormulaContext const& BinaryBooleanPathFormula::getContext() const { + return context; + } + bool BinaryBooleanPathFormula::isBinaryBooleanPathFormula() const { return true; } + bool BinaryBooleanPathFormula::isProbabilityPathFormula() const { + return true; + } + boost::any BinaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/BinaryBooleanPathFormula.h b/src/storm/logic/BinaryBooleanPathFormula.h index 6f60f06f4..10286f23f 100644 --- a/src/storm/logic/BinaryBooleanPathFormula.h +++ b/src/storm/logic/BinaryBooleanPathFormula.h @@ -5,6 +5,7 @@ #include "storm/logic/BinaryPathFormula.h" #include "storm/logic/BinaryBooleanOperatorType.h" +#include "storm/logic/FormulaContext.h" namespace storm { namespace logic { @@ -12,13 +13,16 @@ namespace storm { public: typedef storm::logic::BinaryBooleanOperatorType OperatorType; - BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, FormulaContext context = FormulaContext::Probability); virtual ~BinaryBooleanPathFormula() { // Intentionally left empty. }; + FormulaContext const& getContext() const; + virtual bool isBinaryBooleanPathFormula() const override; + virtual bool isProbabilityPathFormula() const override; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; @@ -31,6 +35,7 @@ namespace storm { private: OperatorType operatorType; + FormulaContext context; }; } } diff --git a/src/storm/logic/UnaryBooleanPathFormula.cpp b/src/storm/logic/UnaryBooleanPathFormula.cpp index 61b699d55..7613032b6 100644 --- a/src/storm/logic/UnaryBooleanPathFormula.cpp +++ b/src/storm/logic/UnaryBooleanPathFormula.cpp @@ -7,14 +7,23 @@ namespace storm { namespace logic { - UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryPathFormula(subformula), operatorType(operatorType) { + UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula, FormulaContext context) : UnaryPathFormula(subformula), operatorType(operatorType), context(context) { STORM_LOG_THROW(this->getSubformula().isStateFormula() || this->getSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); + STORM_LOG_THROW(context == FormulaContext::Probability, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); } + FormulaContext const& UnaryBooleanPathFormula::getContext() const { + return context; + } + bool UnaryBooleanPathFormula::isUnaryBooleanPathFormula() const { return true; } + bool UnaryBooleanPathFormula::isProbabilityPathFormula() const { + return true; + } + boost::any UnaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/UnaryBooleanPathFormula.h b/src/storm/logic/UnaryBooleanPathFormula.h index bbef7aeac..3323f6949 100644 --- a/src/storm/logic/UnaryBooleanPathFormula.h +++ b/src/storm/logic/UnaryBooleanPathFormula.h @@ -3,6 +3,7 @@ #include "storm/logic/UnaryPathFormula.h" #include "storm/logic/UnaryBooleanOperatorType.h" +#include "storm/logic/FormulaContext.h" namespace storm { namespace logic { @@ -10,13 +11,16 @@ namespace storm { public: typedef storm::logic::UnaryBooleanOperatorType OperatorType; - UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula); + UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability); virtual ~UnaryBooleanPathFormula() { // Intentionally left empty. }; + FormulaContext const& getContext() const; + virtual bool isUnaryBooleanPathFormula() const override; + virtual bool isProbabilityPathFormula() const override; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; @@ -28,6 +32,7 @@ namespace storm { private: OperatorType operatorType; + FormulaContext context; }; } }