Formulas: Added parentheses to formula output to avoid ambiguity

4 years ago · 10e2d85cc4
54 changed files with 168 additions and 81 deletions
--- a/src/storm/logic/AtomicExpressionFormula.cpp
+++ b/src/storm/logic/AtomicExpressionFormula.cpp
@ -28,8 +28,15 @@ namespace storm {
            expression.gatherVariables(usedVariables);
        }
        
-        std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
+        std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            bool parentheses = allowParentheses & (this->expression.isLiteral() || this->expression.isVariable());
+            if (parentheses) {
+                out << "(";
+            }
            out << expression;
+            if (parentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/AtomicExpressionFormula.h
+++ b/src/storm/logic/AtomicExpressionFormula.h
@ -19,7 +19,7 @@ namespace storm {
            
            storm::expressions::Expression const& getExpression() const;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
--- a/src/storm/logic/AtomicLabelFormula.cpp
+++ b/src/storm/logic/AtomicLabelFormula.cpp
@ -25,7 +25,8 @@ namespace storm {
            atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicLabelFormula const>(this->shared_from_this()));
        }
        
-        std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out) const {
+        std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out, bool /*allowParentheses*/) const {
+            // No parentheses necessary
            out << "\"" << label << "\"";
            return out;
        }
--- a/src/storm/logic/AtomicLabelFormula.h
+++ b/src/storm/logic/AtomicLabelFormula.h
@ -23,7 +23,7 @@ namespace storm {
            
            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
                        
        private:
            std::string label;
--- a/src/storm/logic/BinaryBooleanPathFormula.cpp
+++ b/src/storm/logic/BinaryBooleanPathFormula.cpp
@ -41,15 +41,19 @@ namespace storm {
            return this->getOperator() == OperatorType::Or;
        }
                
-        std::ostream& BinaryBooleanPathFormula::writeToStream(std::ostream& out) const {
-            out << "(";
-            this->getLeftSubformula().writeToStream(out);
+        std::ostream& BinaryBooleanPathFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
+            this->getLeftSubformula().writeToStream(out, true);
            switch (operatorType) {
                case OperatorType::And: out << " & "; break;
                case OperatorType::Or: out << " | "; break;
            }
-            this->getRightSubformula().writeToStream(out);
-            out << ")";
+            this->getRightSubformula().writeToStream(out, true);
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/BinaryBooleanPathFormula.h
+++ b/src/storm/logic/BinaryBooleanPathFormula.h
@ -31,7 +31,7 @@ namespace storm {
            virtual bool isAnd() const;
            virtual bool isOr() const;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
        private:
            OperatorType operatorType;
--- a/src/storm/logic/BinaryBooleanStateFormula.cpp
+++ b/src/storm/logic/BinaryBooleanStateFormula.cpp
@ -31,15 +31,19 @@ namespace storm {
            return this->getOperator() == OperatorType::Or;
        }
                
-        std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
-            out << "(";
-            this->getLeftSubformula().writeToStream(out);
+        std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
+            this->getLeftSubformula().writeToStream(out, true);
            switch (operatorType) {
                case OperatorType::And: out << " & "; break;
                case OperatorType::Or: out << " | "; break;
            }
-            this->getRightSubformula().writeToStream(out);
-            out << ")";
+            this->getRightSubformula().writeToStream(out, true);
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/BinaryBooleanStateFormula.h
+++ b/src/storm/logic/BinaryBooleanStateFormula.h
@ -27,7 +27,7 @@ namespace storm {
            virtual bool isAnd() const;
            virtual bool isOr() const;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
        private:
            OperatorType operatorType;
--- a/src/storm/logic/BooleanLiteralFormula.cpp
+++ b/src/storm/logic/BooleanLiteralFormula.cpp
@ -24,7 +24,8 @@ namespace storm {
            return visitor.visit(*this, data);
        }
        
-        std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const {
+        std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out, bool /*allowParentheses */) const {
+            // No parentheses necessary
            if (value) {
                out << "true";
            } else {
--- a/src/storm/logic/BooleanLiteralFormula.h
+++ b/src/storm/logic/BooleanLiteralFormula.h
@ -19,7 +19,7 @@ namespace storm {
            
            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
                        
        private:
            bool value;
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@ -309,7 +309,7 @@ namespace storm {
            return std::make_shared<BoundedUntilFormula const>(getLeftSubformula(i).asSharedPointer(), getRightSubformula(i).asSharedPointer(), lowerBound.at(i), upperBound.at(i), getTimeBoundReference(i));
        }

-        std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
+        std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
            if (hasMultiDimensionalSubformulas()) {
                out << "multi(";
                restrictToDimension(0)->writeToStream(out);
@ -319,8 +319,10 @@ namespace storm {
                }
                out << ")";
            } else {
-                
-                this->getLeftSubformula().writeToStream(out);
+                if (allowParentheses) {
+                    out << "(";
+                }
+                this->getLeftSubformula().writeToStream(out, true);
                
                out << " U";
                if (this->isMultiDimensional()) {
@ -379,7 +381,10 @@ namespace storm {
                    out << "}";
                }
                
-                this->getRightSubformula().writeToStream(out);
+                this->getRightSubformula().writeToStream(out, true);
+                if (allowParentheses) {
+                    out << ")";
+                }
            }
            
            return out;
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@ -67,7 +67,7 @@ namespace storm {

            std::shared_ptr<BoundedUntilFormula const> restrictToDimension(unsigned i) const;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
        private:
            static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
--- a/src/storm/logic/ConditionalFormula.cpp
+++ b/src/storm/logic/ConditionalFormula.cpp
@ -62,10 +62,16 @@ namespace storm {
            return true;
        }
        
-        std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const {
-            this->getSubformula().writeToStream(out);
+        std::ostream& ConditionalFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
+            this->getSubformula().writeToStream(out, true);
            out << " || ";
-            this->getConditionFormula().writeToStream(out);
+            this->getConditionFormula().writeToStream(out, true);
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/ConditionalFormula.h
+++ b/src/storm/logic/ConditionalFormula.h
@ -23,7 +23,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/src/storm/logic/CumulativeRewardFormula.cpp
@ -161,7 +161,8 @@ namespace storm {
            return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i), rewardAccumulation);
        }
        
-        std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
+        std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out, bool /*allowParentheses*/ ) const {
+            // No parentheses necessary
            out << "C";
            if (hasRewardAccumulation()) {
                out << "[" << getRewardAccumulation() << "]";
--- a/src/storm/logic/CumulativeRewardFormula.h
+++ b/src/storm/logic/CumulativeRewardFormula.h
@ -26,7 +26,7 @@ namespace storm {
            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            TimeBoundReference const& getTimeBoundReference() const;
            TimeBoundReference const& getTimeBoundReference(unsigned i) const;
--- a/src/storm/logic/EventuallyFormula.cpp
+++ b/src/storm/logic/EventuallyFormula.cpp
@ -55,12 +55,18 @@ namespace storm {
            return visitor.visit(*this, data);
        }
                
-        std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {
+        std::ostream& EventuallyFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
            out << "F ";
            if (hasRewardAccumulation()) {
                out << "[" << getRewardAccumulation() << "]";
            }
-            this->getSubformula().writeToStream(out);
+            this->getSubformula().writeToStream(out, !this->getSubformula().isUnaryFormula());
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/EventuallyFormula.h
+++ b/src/storm/logic/EventuallyFormula.h
@ -29,7 +29,7 @@ namespace storm {
            
            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            bool hasRewardAccumulation() const;
            RewardAccumulation const& getRewardAccumulation() const;
            
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@ -179,6 +179,10 @@ namespace storm {
        bool Formula::isOperatorFormula() const {
            return false;
        }
+        
+        bool Formula::isUnaryFormula() const {
+            return isUnaryPathFormula() || isUnaryStateFormula();
+        }

        bool Formula::hasQualitativeResult() const {
            return true;
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@ -94,6 +94,7 @@ namespace storm {
            virtual bool isBinaryStateFormula() const;
            virtual bool isUnaryPathFormula() const;
            virtual bool isUnaryStateFormula() const;
+            bool isUnaryFormula() const;

            // Accessors for the return type of a formula.
            virtual bool hasQualitativeResult() const;
@ -236,7 +237,14 @@ namespace storm {
            storm::expressions::Expression toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping = {}) const;

            std::string toString() const;
-            virtual std::ostream& writeToStream(std::ostream& out) const = 0;
+
+            /*!
+             * Writes the forumla to the given output stream
+             * @param allowParenthesis if true, the output is *potentially* surrounded by parentheses depending on whether parentheses are needed to avoid ambiguity when this formula appears as a subformula of some larger formula.
+             * @return
+             */
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const = 0;
+            
            std::string toPrefixString() const;

            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
--- a/src/storm/logic/GameFormula.cpp
+++ b/src/storm/logic/GameFormula.cpp
@ -32,9 +32,10 @@ namespace storm {
            return visitor.visit(*this, data);
        }

-        std::ostream& GameFormula::writeToStream(std::ostream& out) const {
+        std::ostream& GameFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parenthesis necessary
            out << "<<" << coalition << ">> ";
-            this->getSubformula().writeToStream(out);
+            this->getSubformula().writeToStream(out, true);
            return out;
        }
    }
--- a/src/storm/logic/GameFormula.h
+++ b/src/storm/logic/GameFormula.h
@ -24,7 +24,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

        private:
            PlayerCoalition coalition;
--- a/src/storm/logic/GloballyFormula.cpp
+++ b/src/storm/logic/GloballyFormula.cpp
@ -20,9 +20,15 @@ namespace storm {
            return visitor.visit(*this, data);
        }
        
-        std::ostream& GloballyFormula::writeToStream(std::ostream& out) const {
+        std::ostream& GloballyFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
            out << "G ";
-            this->getSubformula().writeToStream(out);
+            this->getSubformula().writeToStream(out, !this->getSubformula().isUnaryFormula());
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/GloballyFormula.h
+++ b/src/storm/logic/GloballyFormula.h
@ -18,7 +18,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        };
    }
 }
--- a/src/storm/logic/HOAPathFormula.cpp
+++ b/src/storm/logic/HOAPathFormula.cpp
@ -76,7 +76,8 @@ namespace storm {
        }


-        std::ostream& HOAPathFormula::writeToStream(std::ostream& out) const {
+        std::ostream& HOAPathFormula::writeToStream(std::ostream& out, bool /* allowParentheses */ ) const {
+            // No parentheses necessary
            out << "HOA: { ";
            out << "\"" <<  automatonFile << "\"";
            for (auto& mapping : apToFormulaMap) {
--- a/src/storm/logic/HOAPathFormula.h
+++ b/src/storm/logic/HOAPathFormula.h
@ -39,7 +39,7 @@ namespace storm {
            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

 	    std::shared_ptr<storm::automata::DeterministicAutomaton> readAutomaton() const;

--- a/src/storm/logic/InstantaneousRewardFormula.cpp
+++ b/src/storm/logic/InstantaneousRewardFormula.cpp
@ -68,7 +68,8 @@ namespace storm {
            STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-instant '" << bound << "' as it contains undefined constants.");
        }
        
-        std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const {
+        std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary.
            out << "I=" << this->getBound();
            return out;
        }
--- a/src/storm/logic/InstantaneousRewardFormula.h
+++ b/src/storm/logic/InstantaneousRewardFormula.h
@ -22,7 +22,7 @@ namespace storm {
            
            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            TimeBoundType const& getTimeBoundType() const;
            bool isStepBounded() const;
--- a/src/storm/logic/LongRunAverageOperatorFormula.cpp
+++ b/src/storm/logic/LongRunAverageOperatorFormula.cpp
@ -18,10 +18,11 @@ namespace storm {
        boost::any LongRunAverageOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
            return visitor.visit(*this, data);
        }
-                
-        std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {
+        
+        std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "LRA";
-            OperatorFormula::writeToStream(out);
+            OperatorFormula::writeToStream(out, false);
            return out;
        }
    }
--- a/src/storm/logic/LongRunAverageOperatorFormula.h
+++ b/src/storm/logic/LongRunAverageOperatorFormula.h
@ -17,7 +17,7 @@ namespace storm {
            
            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        };
    }
 }
--- a/src/storm/logic/LongRunAverageRewardFormula.cpp
+++ b/src/storm/logic/LongRunAverageRewardFormula.cpp
@ -32,7 +32,8 @@ namespace storm {
            return visitor.visit(*this, data);
        }
        
-        std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out) const {
+        std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "LRA";
            if (hasRewardAccumulation()) {
                out << "[" << getRewardAccumulation() << "]";
--- a/src/storm/logic/LongRunAverageRewardFormula.h
+++ b/src/storm/logic/LongRunAverageRewardFormula.h
@ -23,7 +23,7 @@ namespace storm {
            
            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

        private:
            boost::optional<RewardAccumulation> rewardAccumulation;
--- a/src/storm/logic/MultiObjectiveFormula.cpp
+++ b/src/storm/logic/MultiObjectiveFormula.cpp
@ -84,7 +84,8 @@ namespace storm {
            }
        }
        
-        std::ostream& MultiObjectiveFormula::writeToStream(std::ostream &out) const {
+        std::ostream& MultiObjectiveFormula::writeToStream(std::ostream &out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "multi(";
            for(uint_fast64_t index = 0; index < this->getNumberOfSubformulas(); ++index){
                if(index>0){
--- a/src/storm/logic/MultiObjectiveFormula.h
+++ b/src/storm/logic/MultiObjectiveFormula.h
@ -27,7 +27,7 @@ namespace storm {
            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        private:
            std::vector<std::shared_ptr<Formula const>> subformulas;
        };
--- a/src/storm/logic/NextFormula.cpp
+++ b/src/storm/logic/NextFormula.cpp
@ -20,9 +20,15 @@ namespace storm {
            return visitor.visit(*this, data);
        }
                
-        std::ostream& NextFormula::writeToStream(std::ostream& out) const {
+        std::ostream& NextFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
            out << "X ";
-            this->getSubformula().writeToStream(out);
+            this->getSubformula().writeToStream(out, !this->getSubformula().isUnaryFormula());
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/NextFormula.h
+++ b/src/storm/logic/NextFormula.h
@ -18,7 +18,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        };
    }
 }
--- a/src/storm/logic/OperatorFormula.cpp
+++ b/src/storm/logic/OperatorFormula.cpp
@ -104,7 +104,8 @@ namespace storm {
            }
        }
        
-        std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
+        std::ostream& OperatorFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            if (hasOptimalityType()) {
                out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");
            }
--- a/src/storm/logic/OperatorFormula.h
+++ b/src/storm/logic/OperatorFormula.h
@ -56,7 +56,7 @@ namespace storm {
            
            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
        protected:
            OperatorInformation operatorInformation;
--- a/src/storm/logic/ProbabilityOperatorFormula.cpp
+++ b/src/storm/logic/ProbabilityOperatorFormula.cpp
@ -19,9 +19,10 @@ namespace storm {
            return visitor.visit(*this, data);
        }
                
-        std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {
+        std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "P";
-            OperatorFormula::writeToStream(out);
+            OperatorFormula::writeToStream(out, false);
            return out;
        }
    }
--- a/src/storm/logic/ProbabilityOperatorFormula.h
+++ b/src/storm/logic/ProbabilityOperatorFormula.h
@ -17,7 +17,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        };
    }
 }
--- a/src/storm/logic/QuantileFormula.cpp
+++ b/src/storm/logic/QuantileFormula.cpp
@ -73,7 +73,8 @@ namespace storm {
            subformula->gatherReferencedRewardModels(referencedRewardModels);
        }
        
-        std::ostream& QuantileFormula::writeToStream(std::ostream& out) const {
+        std::ostream& QuantileFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "quantile(";
            for (auto const& bv : boundVariables) {
                out << bv.getName() << ", ";
--- a/src/storm/logic/QuantileFormula.h
+++ b/src/storm/logic/QuantileFormula.h
@ -29,7 +29,7 @@ namespace storm {
            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        private:
            std::vector<storm::expressions::Variable> boundVariables;
            std::shared_ptr<Formula const> subformula;
--- a/src/storm/logic/RewardOperatorFormula.cpp
+++ b/src/storm/logic/RewardOperatorFormula.cpp
@ -44,7 +44,8 @@ namespace storm {
            return rewardMeasureType;
        }
        
-        std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {
+        std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "R";
            out << "[" << rewardMeasureType << "]";
            if (this->hasRewardModelName()) {
--- a/src/storm/logic/RewardOperatorFormula.h
+++ b/src/storm/logic/RewardOperatorFormula.h
@ -20,7 +20,7 @@ namespace storm {

            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            /*!
             * Retrieves whether the reward model refers to a specific reward model.
--- a/src/storm/logic/TimeOperatorFormula.cpp
+++ b/src/storm/logic/TimeOperatorFormula.cpp
@ -24,7 +24,8 @@ namespace storm {
            return rewardMeasureType;
        }
        
-        std::ostream& TimeOperatorFormula::writeToStream(std::ostream& out) const {
+        std::ostream& TimeOperatorFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "T";
            out << "[" << rewardMeasureType << "]";
            OperatorFormula::writeToStream(out);
--- a/src/storm/logic/TimeOperatorFormula.h
+++ b/src/storm/logic/TimeOperatorFormula.h
@ -19,7 +19,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
            
            /*!
             * Retrieves the measure type of the operator.
--- a/src/storm/logic/TotalRewardFormula.cpp
+++ b/src/storm/logic/TotalRewardFormula.cpp
@ -32,7 +32,8 @@ namespace storm {
            return visitor.visit(*this, data);
        }

-        std::ostream& TotalRewardFormula::writeToStream(std::ostream& out) const {
+        std::ostream& TotalRewardFormula::writeToStream(std::ostream& out, bool /* allowParentheses */) const {
+            // No parentheses necessary
            out << "C";
            if (hasRewardAccumulation()) {
                out << "[" << getRewardAccumulation() << "]";
--- a/src/storm/logic/TotalRewardFormula.h
+++ b/src/storm/logic/TotalRewardFormula.h
@ -24,7 +24,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;

-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

        private:
            boost::optional<RewardAccumulation> rewardAccumulation;
--- a/src/storm/logic/UnaryBooleanPathFormula.cpp
+++ b/src/storm/logic/UnaryBooleanPathFormula.cpp
@ -36,12 +36,17 @@ namespace storm {
            return this->getOperator() == OperatorType::Not;
        }
                
-        std::ostream& UnaryBooleanPathFormula::writeToStream(std::ostream& out) const {
+        std::ostream& UnaryBooleanPathFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
            switch (operatorType) {
-                case OperatorType::Not: out << "!("; break;
+                case OperatorType::Not: out << "!"; break;
+            }
+            this->getSubformula().writeToStream(out, !this->getSubformula().isUnaryFormula());
+            if (allowParentheses) {
+                out << ")";
            }
-            this->getSubformula().writeToStream(out);
-            out << ")";
            return out;
        }
    }
--- a/src/storm/logic/UnaryBooleanPathFormula.h
+++ b/src/storm/logic/UnaryBooleanPathFormula.h
@ -28,7 +28,7 @@ namespace storm {
            
            virtual bool isNot() const;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

        private:
            OperatorType operatorType;
--- a/src/storm/logic/UnaryBooleanStateFormula.cpp
+++ b/src/storm/logic/UnaryBooleanStateFormula.cpp
@ -27,12 +27,17 @@ namespace storm {
            return this->getOperator() == OperatorType::Not;
        }
                
-        std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const {
+        std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
            switch (operatorType) {
-                case OperatorType::Not: out << "!("; break;
+                case OperatorType::Not: out << "!"; break;
+            }
+            this->getSubformula().writeToStream(out, !this->getSubformula().isUnaryFormula());
+            if (allowParentheses) {
+                out << ")";
            }
-            this->getSubformula().writeToStream(out);
-            out << ")";
            return out;
        }
    }
--- a/src/storm/logic/UnaryBooleanStateFormula.h
+++ b/src/storm/logic/UnaryBooleanStateFormula.h
@ -24,7 +24,7 @@ namespace storm {
            
            virtual bool isNot() const;
            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;

        private:
            OperatorType operatorType;
--- a/src/storm/logic/UntilFormula.cpp
+++ b/src/storm/logic/UntilFormula.cpp
@ -20,10 +20,16 @@ namespace storm {
            return visitor.visit(*this, data);
        }
        
-        std::ostream& UntilFormula::writeToStream(std::ostream& out) const {
-            this->getLeftSubformula().writeToStream(out);
+        std::ostream& UntilFormula::writeToStream(std::ostream& out, bool allowParentheses) const {
+            if (allowParentheses) {
+                out << "(";
+            }
+            this->getLeftSubformula().writeToStream(out, true);
            out << " U ";
-            this->getRightSubformula().writeToStream(out);
+            this->getRightSubformula().writeToStream(out, true);
+            if (allowParentheses) {
+                out << ")";
+            }
            return out;
        }
    }
--- a/src/storm/logic/UntilFormula.h
+++ b/src/storm/logic/UntilFormula.h
@ -18,7 +18,7 @@ namespace storm {

            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
                        
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const override;
        };
    }
 }