WIP:needed? Boolean path formulas: allow storing context

src/storm/logic/BinaryBooleanPathFormula.cpp

@@ -7,15 +7,24 @@
 
 namespace storm {
     namespace logic {
-        BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
+        BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> 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);
         }

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<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
+            BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> 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;
         };
     }
 }

src/storm/logic/UnaryBooleanPathFormula.cpp

@@ -7,14 +7,23 @@
 
 namespace storm {
     namespace logic {
-        UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula), operatorType(operatorType) {
+        UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> 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);
         }

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<Formula const> const& subformula);
+            UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> 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;
         };
     }
 }