(LTL) Refactor unary/boolean state formulas to allow path formulas as well

Previously, the formula parser only supported AND, OR and NOT over state formulas. For LTL, we need those over path formulas. We tweak the grammar, the AST types and visitors, to also handle UnaryBooleanPathFormula and BinaryBooleanPathformula. During parsing, we determine on-demand whether to generate the path or state formula variant by looking at the subformulas - if they are state formulas, the boolean operator will be a state formula as well. Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.cpp src/storm/logic/Formula.h src/storm/logic/FragmentChecker.cpp src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/storage/jani/JSONExporter.cpp
5 years ago · 5482a32b8a
29 changed files with 351 additions and 27 deletions
--- a/src/storm-parsers/parser/FormulaParserGrammar.cpp
+++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp
@ -52,13 +52,13 @@ namespace storm {
            operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator;
            operatorFormula.name("operator formulas");

-            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
+            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula;
            atomicStateFormula.name("atomic state formula");

-            atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
+            atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula;
            atomicStateFormula.name("atomic state formula without expression");

-            notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1];
+            notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula(qi::_r1)[qi::_val = qi::_1];
            notStateFormula.name("negation formula");

            eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
@ -70,7 +70,7 @@ namespace storm {
            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
            nextFormula.name("next formula");

-            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
+            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula(qi::_r1);
            pathFormulaWithoutUntil.name("path formula");

            untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
@ -78,7 +78,7 @@ namespace storm {

            hoaPathFormula = qi::lit("HOA:") > qi::lit("{")
                > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)]
-                >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)]
+                >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula(qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)]
                > qi::lit("}");

            basicPathFormula = (hoaPathFormula(qi::_r1)[qi::_val = qi::_1]) | untilFormula(qi::_r1)[qi::_val = qi::_1];
@ -112,7 +112,7 @@ namespace storm {
            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
            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 > qi::lit("[") > stateFormula(storm::logic::FormulaContext::LongRunAverage) > 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("\"}");
@ -127,13 +127,13 @@ namespace storm {
            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.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)];
+            andStateFormula = notStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
            andStateFormula.name("and state formula");

-            orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
+            orStateFormula = andStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
            orStateFormula.name("or state formula");

-            multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)];
+            multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula(storm::logic::FormulaContext::Probability)) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)];
            multiFormula.name("Multi formula");

            identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]];
@ -141,7 +141,7 @@ namespace storm {

            quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a,  qi::_1)];
            quantileBoundVariable.name("quantile bound variable");
-            quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)];
            quantileFormula.name("Quantile formula");

            playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)];
@ -166,7 +166,7 @@ namespace storm {
                                 qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
            shieldComparison.name("shield comparison type");

-            stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
+            stateFormula = (orStateFormula(qi::_r1) | multiFormula | quantileFormula);
            stateFormula.name("state formula");

            quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]];
@ -183,7 +183,7 @@ namespace storm {
 #pragma clang diagnostic push
 #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"

-            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
+            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
            filterProperty.name("filter property");

 #pragma clang diagnostic pop
@ -452,6 +452,34 @@ namespace storm {
            }
        }

+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType) {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanPathFormula(operatorType, leftSubformula, rightSubformula));
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanPathFormula::OperatorType> const& operatorType) {
+            if (operatorType) {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanPathFormula(operatorType.get(), subformula));
+            } else {
+                return subformula;
+            }
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType) {
+            if (leftSubformula->isStateFormula() && rightSubformula->isStateFormula()) {
+                return createBinaryBooleanStateFormula(leftSubformula, rightSubformula, operatorType);
+            } else {
+                return createBinaryBooleanPathFormula(leftSubformula, rightSubformula, operatorType);
+            }
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanOperatorType> const& operatorType) {
+            if (subformula->isStateFormula()) {
+                return createUnaryBooleanStateFormula(subformula, operatorType);
+            } else {
+                return createUnaryBooleanPathFormula(subformula, operatorType);
+            }
+        }
+
        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
            bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty();
            for (auto const& subformula : subformulas) {
--- a/src/storm-parsers/parser/FormulaParserGrammar.h
+++ b/src/storm-parsers/parser/FormulaParserGrammar.h
@ -165,19 +165,19 @@ namespace storm {

            qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> stateFormula;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simplePathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormulaWithoutExpression;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> atomicStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> atomicStateFormulaWithoutExpression;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
            qi::rule<Iterator, std::string(), Skipper> label;
            qi::rule<Iterator, std::string(), Skipper> rewardModelName;

-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> andStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> orStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> notStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> andStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> orStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> notStateFormula;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> labelFormula;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> expressionFormula;
            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
@ -250,7 +250,11 @@ namespace storm {
            std::shared_ptr<storm::logic::Formula const> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
            std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
+            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType);
+            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType);
            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanPathFormula::OperatorType> const& operatorType);
+            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanOperatorType> const& operatorType);
            std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
            storm::expressions::Variable createQuantileBoundVariables(boost::optional<storm::solver::OptimizationDirection> const& dir, std::string const& variableName);
            std::shared_ptr<storm::logic::Formula const> createQuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula);
--- a/src/storm/logic/BinaryBooleanOperatorType.h
+++ b/src/storm/logic/BinaryBooleanOperatorType.h
@ -0,0 +1,7 @@
+#pragma once
+
+namespace storm {
+    namespace logic {
+        enum class BinaryBooleanOperatorType {And, Or};
+    }
+}
--- a/src/storm/logic/BinaryBooleanPathFormula.cpp
+++ b/src/storm/logic/BinaryBooleanPathFormula.cpp
@ -0,0 +1,47 @@
+#include "storm/logic/BinaryBooleanPathFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+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) {
+            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");
+        }
+        
+        bool BinaryBooleanPathFormula::isBinaryBooleanPathFormula() const {
+            return true;
+        }
+        
+        boost::any BinaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        BinaryBooleanPathFormula::OperatorType BinaryBooleanPathFormula::getOperator() const {
+            return operatorType;
+        }
+        
+        bool BinaryBooleanPathFormula::isAnd() const {
+            return this->getOperator() == OperatorType::And;
+        }
+        
+        bool BinaryBooleanPathFormula::isOr() const {
+            return this->getOperator() == OperatorType::Or;
+        }
+                
+        std::ostream& BinaryBooleanPathFormula::writeToStream(std::ostream& out) const {
+            out << "(";
+            this->getLeftSubformula().writeToStream(out);
+            switch (operatorType) {
+                case OperatorType::And: out << " & "; break;
+                case OperatorType::Or: out << " | "; break;
+            }
+            this->getRightSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}
--- a/src/storm/logic/BinaryBooleanPathFormula.h
+++ b/src/storm/logic/BinaryBooleanPathFormula.h
@ -0,0 +1,38 @@
+#ifndef STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_
+#define STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_
+
+#include <map>
+
+#include "storm/logic/BinaryPathFormula.h"
+#include "storm/logic/BinaryBooleanOperatorType.h"
+
+namespace storm {
+    namespace logic {
+        class BinaryBooleanPathFormula : public BinaryPathFormula {
+        public:
+            typedef storm::logic::BinaryBooleanOperatorType OperatorType;
+
+            BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
+            
+            virtual ~BinaryBooleanPathFormula() {
+                // Intentionally left empty.
+            };
+            
+            virtual bool isBinaryBooleanPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
+            OperatorType getOperator() const;
+            
+            virtual bool isAnd() const;
+            virtual bool isOr() const;
+                        
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            OperatorType operatorType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_ */
--- a/src/storm/logic/BinaryBooleanStateFormula.h
+++ b/src/storm/logic/BinaryBooleanStateFormula.h
@ -4,12 +4,13 @@
 #include <map>

 #include "storm/logic/BinaryStateFormula.h"
+#include "storm/logic/BinaryBooleanOperatorType.h"

 namespace storm {
    namespace logic {
        class BinaryBooleanStateFormula : public BinaryStateFormula {
        public:
-            enum class OperatorType {And, Or};
+            typedef storm::logic::BinaryBooleanOperatorType OperatorType;

            BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
            
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/src/storm/logic/CloneVisitor.cpp
@ -24,6 +24,12 @@ namespace storm {
            return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanStateFormula>(f.getOperator(), left, right));
        }

+        boost::any CloneVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanPathFormula>(f.getOperator(), left, right));
+        }
+
        boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
            return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
        }
@ -170,6 +176,11 @@ namespace storm {
            return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula));
        }

+        boost::any CloneVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanPathFormula>(f.getOperator(), subformula));
+        }
+
        boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const {
            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
--- a/src/storm/logic/CloneVisitor.h
+++ b/src/storm/logic/CloneVisitor.h
@ -15,6 +15,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@ -34,6 +35,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
        };
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@ -43,6 +43,14 @@ namespace storm {
            return false;
        }

+        bool Formula::isBinaryBooleanPathFormula() const {
+            return false;
+        }
+
+        bool Formula::isUnaryBooleanPathFormula() const {
+            return false;
+        }
+
        bool Formula::isBooleanLiteralFormula() const {
            return false;
        }
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@ -47,6 +47,9 @@ namespace storm {
            virtual bool isBinaryBooleanStateFormula() const;
            virtual bool isUnaryBooleanStateFormula() const;

+            virtual bool isBinaryBooleanPathFormula() const;
+            virtual bool isUnaryBooleanPathFormula() const;
+
            virtual bool isMultiObjectiveFormula() const;
            virtual bool isQuantileFormula() const;

--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/src/storm/logic/FormulaInformationVisitor.cpp
@ -17,10 +17,14 @@ namespace storm {
            return FormulaInformation();
        }
        
-        boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
-            return FormulaInformation();
+        boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
        }
        
+        boost::any FormulaInformationVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+        }
+
        boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
            return FormulaInformation();
        }
@ -130,6 +134,10 @@ namespace storm {
            return f.getSubformula().accept(*this, data);
        }
        
+        boost::any FormulaInformationVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+
        boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const {
            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
        }
--- a/src/storm/logic/FormulaInformationVisitor.h
+++ b/src/storm/logic/FormulaInformationVisitor.h
@ -14,6 +14,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@ -33,6 +34,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
        };
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@ -15,6 +15,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0;
@ -34,6 +35,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0;
            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const = 0;
        };
--- a/src/storm/logic/Formulas.h
+++ b/src/storm/logic/Formulas.h
@ -2,6 +2,7 @@
 #include "storm/logic/AtomicExpressionFormula.h"
 #include "storm/logic/AtomicLabelFormula.h"
 #include "storm/logic/BinaryBooleanStateFormula.h"
+#include "storm/logic/BinaryBooleanPathFormula.h"
 #include "storm/logic/BinaryPathFormula.h"
 #include "storm/logic/BinaryStateFormula.h"
 #include "storm/logic/BooleanLiteralFormula.h"
@ -25,6 +26,7 @@
 #include "storm/logic/TimeOperatorFormula.h"
 #include "storm/logic/TotalRewardFormula.h"
 #include "storm/logic/UnaryBooleanStateFormula.h"
+#include "storm/logic/UnaryBooleanPathFormula.h"
 #include "storm/logic/UnaryPathFormula.h"
 #include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/UntilFormula.h"
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/src/storm/logic/FormulasForwardDeclarations.h
@ -8,6 +8,7 @@ namespace storm {
        class AtomicExpressionFormula;
        class AtomicLabelFormula;
        class BinaryBooleanStateFormula;
+        class BinaryBooleanPathFormula;
        class BinaryPathFormula;
        class BinaryStateFormula;
        class BooleanLiteralFormula;
@ -33,6 +34,7 @@ namespace storm {
        class StateFormula;
        class TotalRewardFormula;
        class UnaryBooleanStateFormula;
+        class UnaryBooleanPathFormula;
        class UnaryPathFormula;
        class UnaryStateFormula;
        class UntilFormula;
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@ -52,6 +52,14 @@ namespace storm {
            return result;
        }

+        boost::any FragmentChecker::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areBinaryBooleanPathFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
+            result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
+            return result;
+        }
+
        boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const {
            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
            return inherited.getSpecification().areBooleanLiteralFormulasAllowed();
@ -311,6 +319,13 @@ namespace storm {
            return result;
        }

+        boost::any FragmentChecker::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areUnaryBooleanPathFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
+        }
+
        boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const {
            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
            bool result = inherited.getSpecification().areUntilFormulasAllowed();
--- a/src/storm/logic/FragmentChecker.h
+++ b/src/storm/logic/FragmentChecker.h
@ -15,6 +15,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@ -34,6 +35,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
        };
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@ -175,6 +175,8 @@ namespace storm {
            booleanLiteralFormula = false;
            unaryBooleanStateFormula = false;
            binaryBooleanStateFormula = false;
+            unaryBooleanPathFormula = false;
+            binaryBooleanPathFormula = false;

            cumulativeRewardFormula = false;
            instantaneousRewardFormula = false;
@ -372,12 +374,21 @@ namespace storm {
            return *this;
        }

-        bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const {
-            return binaryBooleanStateFormula;
+        bool FragmentSpecification::areUnaryBooleanPathFormulasAllowed() const {
+            return unaryBooleanPathFormula;
        }

-        FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) {
-            this->binaryBooleanStateFormula = newValue;
+        FragmentSpecification& FragmentSpecification::setUnaryBooleanPathFormulasAllowed(bool newValue) {
+            this->unaryBooleanPathFormula = newValue;
+            return *this;
+        }
+
+        bool FragmentSpecification::areBinaryBooleanPathFormulasAllowed() const {
+            return binaryBooleanPathFormula;
+        }
+
+        FragmentSpecification& FragmentSpecification::setBinaryBooleanPathFormulasAllowed(bool newValue) {
+            this->binaryBooleanPathFormula = newValue;
            return *this;
        }

--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@ -70,9 +70,15 @@ namespace storm {
            bool areUnaryBooleanStateFormulasAllowed() const;
            FragmentSpecification& setUnaryBooleanStateFormulasAllowed(bool newValue);

+            bool areUnaryBooleanPathFormulasAllowed() const;
+            FragmentSpecification& setUnaryBooleanPathFormulasAllowed(bool newValue);
+
            bool areBinaryBooleanStateFormulasAllowed() const;
            FragmentSpecification& setBinaryBooleanStateFormulasAllowed(bool newValue);

+            bool areBinaryBooleanPathFormulasAllowed() const;
+            FragmentSpecification& setBinaryBooleanPathFormulasAllowed(bool newValue);
+
            bool areCumulativeRewardFormulasAllowed() const;
            FragmentSpecification& setCumulativeRewardFormulasAllowed(bool newValue);

@ -190,6 +196,8 @@ namespace storm {
            bool booleanLiteralFormula;
            bool unaryBooleanStateFormula;
            bool binaryBooleanStateFormula;
+            bool unaryBooleanPathFormula;
+            bool binaryBooleanPathFormula;

            bool cumulativeRewardFormula;
            bool instantaneousRewardFormula;
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
@ -23,9 +23,15 @@ namespace storm {
        }

        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
+	  // TODO joachim: is this correct?
            return true;
        }

+        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
+        }
+
+
        boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
            return true;
        }
@ -143,6 +149,10 @@ namespace storm {
            return f.getSubformula().accept(*this, data);
        }

+        boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+
        boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const {
            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
        }
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.h
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h
@ -21,6 +21,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@ -40,6 +41,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
 	    virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
        
--- a/src/storm/logic/ToExpressionVisitor.cpp
+++ b/src/storm/logic/ToExpressionVisitor.cpp
@ -37,6 +37,10 @@ namespace storm {
            return boost::any();
        }
        
+        boost::any ToExpressionVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+
        boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
            storm::expressions::Expression result;
            if (f.isTrueFormula()) {
@ -124,7 +128,11 @@ namespace storm {
            }
            return boost::any();
        }
-        
+
+        boost::any ToExpressionVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+
        boost::any ToExpressionVisitor::visit(UntilFormula const&, boost::any const&) const {
            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
        }
--- a/src/storm/logic/ToExpressionVisitor.h
+++ b/src/storm/logic/ToExpressionVisitor.h
@ -15,6 +15,7 @@ namespace storm {
            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@ -34,6 +35,7 @@ namespace storm {
            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
        };
--- a/src/storm/logic/UnaryBooleanOperatorType.h
+++ b/src/storm/logic/UnaryBooleanOperatorType.h
@ -0,0 +1,7 @@
+#pragma once
+
+namespace storm {
+    namespace logic {
+        enum class UnaryBooleanOperatorType {Not};
+    }
+}
--- a/src/storm/logic/UnaryBooleanPathFormula.cpp
+++ b/src/storm/logic/UnaryBooleanPathFormula.cpp
@ -0,0 +1,39 @@
+#include "storm/logic/UnaryBooleanPathFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+        UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula), operatorType(operatorType) {
+            STORM_LOG_THROW(this->getSubformula().isStateFormula() || this->getSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas");
+        }
+        
+        bool UnaryBooleanPathFormula::isUnaryBooleanPathFormula() const {
+            return true;
+        }
+
+        boost::any UnaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        UnaryBooleanPathFormula::OperatorType UnaryBooleanPathFormula::getOperator() const {
+            return operatorType;
+        }
+        
+        bool UnaryBooleanPathFormula::isNot() const {
+            return this->getOperator() == OperatorType::Not;
+        }
+                
+        std::ostream& UnaryBooleanPathFormula::writeToStream(std::ostream& out) const {
+            switch (operatorType) {
+                case OperatorType::Not: out << "!("; break;
+            }
+            this->getSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}
--- a/src/storm/logic/UnaryBooleanPathFormula.h
+++ b/src/storm/logic/UnaryBooleanPathFormula.h
@ -0,0 +1,35 @@
+#ifndef STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_
+#define STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_
+
+#include "storm/logic/UnaryPathFormula.h"
+#include "storm/logic/UnaryBooleanOperatorType.h"
+
+namespace storm {
+    namespace logic {
+        class UnaryBooleanPathFormula : public UnaryPathFormula {
+        public:
+            typedef storm::logic::UnaryBooleanOperatorType OperatorType;
+
+            UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula);
+            
+            virtual ~UnaryBooleanPathFormula() {
+                // Intentionally left empty.
+            };
+            
+            virtual bool isUnaryBooleanPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
+            OperatorType getOperator() const;
+            
+            virtual bool isNot() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+        private:
+            OperatorType operatorType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_ */
--- a/src/storm/logic/UnaryBooleanStateFormula.h
+++ b/src/storm/logic/UnaryBooleanStateFormula.h
@ -2,12 +2,13 @@
 #define STORM_LOGIC_UNARYBOOLEANSTATEFORMULA_H_

 #include "storm/logic/UnaryStateFormula.h"
+#include "storm/logic/UnaryBooleanOperatorType.h"

 namespace storm {
    namespace logic {
        class UnaryBooleanStateFormula : public UnaryStateFormula {
        public:
-            enum class OperatorType { Not };
+            typedef storm::logic::UnaryBooleanOperatorType OperatorType;

            UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula);
            
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@ -208,6 +208,14 @@ namespace storm {
            opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
            return opDecl;
        }
+        boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const{
+            ExportJsonType opDecl;
+            storm::logic::BinaryBooleanPathFormula::OperatorType op = f.getOperator();
+            opDecl["op"] = op == storm::logic::BinaryBooleanPathFormula::OperatorType::And ? "∧" : "∨";
+            opDecl["left"] = boost::any_cast<ExportJsonType>(f.getLeftSubformula().accept(*this, data));
+            opDecl["right"] = boost::any_cast<ExportJsonType>(f.getRightSubformula().accept(*this, data));
+            return opDecl;
+        }
        boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const {
            ExportJsonType opDecl(f.isTrueFormula() ? true : false);
            return opDecl;
@ -588,6 +596,15 @@ namespace storm {
            return opDecl;
        }

+        boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            ExportJsonType opDecl;
+            storm::logic::UnaryBooleanPathFormula::OperatorType op = f.getOperator();
+            assert(op == storm::logic::UnaryBooleanPathFormula::OperatorType::Not);
+            opDecl["op"] = "¬";
+            opDecl["exp"] = boost::any_cast<ExportJsonType>(f.getSubformula().accept(*this, data));
+            return opDecl;
+        }
+
        boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
            ExportJsonType opDecl;
            opDecl["op"] = "U";
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@ -52,6 +52,7 @@ namespace storm {
            virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const;
@ -71,6 +72,7 @@ namespace storm {
            virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::TotalRewardFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::UnaryBooleanPathFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
            virtual boost::any visit(storm::logic::HOAPathFormula const& f, boost::any const& data) const;