diff --git a/src/storm/logic/AtomicExpressionFormula.cpp b/src/storm/logic/AtomicExpressionFormula.cpp
index 6fe7b6fdb..1a8d4caa8 100644
--- 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;
}
}
diff --git a/src/storm/logic/AtomicExpressionFormula.h b/src/storm/logic/AtomicExpressionFormula.h
index 21168493b..8bb0b3018 100644
--- 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;
diff --git a/src/storm/logic/AtomicLabelFormula.cpp b/src/storm/logic/AtomicLabelFormula.cpp
index 15790609a..413617c68 100644
--- 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;
}
diff --git a/src/storm/logic/AtomicLabelFormula.h b/src/storm/logic/AtomicLabelFormula.h
index 1173701a0..8314cdb92 100644
--- 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;
diff --git a/src/storm/logic/BinaryBooleanPathFormula.cpp b/src/storm/logic/BinaryBooleanPathFormula.cpp
index b759db23b..1b1b45bf0 100644
--- 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;
}
}
diff --git a/src/storm/logic/BinaryBooleanPathFormula.h b/src/storm/logic/BinaryBooleanPathFormula.h
index 10286f23f..344aed715 100644
--- 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;
diff --git a/src/storm/logic/BinaryBooleanStateFormula.cpp b/src/storm/logic/BinaryBooleanStateFormula.cpp
index ec630eb59..925a155bf 100644
--- 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;
}
}
diff --git a/src/storm/logic/BinaryBooleanStateFormula.h b/src/storm/logic/BinaryBooleanStateFormula.h
index 085b4fb24..26bb3b717 100644
--- 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;
diff --git a/src/storm/logic/BooleanLiteralFormula.cpp b/src/storm/logic/BooleanLiteralFormula.cpp
index 15f961509..552c048b4 100644
--- 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 {
diff --git a/src/storm/logic/BooleanLiteralFormula.h b/src/storm/logic/BooleanLiteralFormula.h
index 2cc59ea15..ef83b6349 100644
--- 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;
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 572712257..e22b626a0 100644
--- 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;
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index df1ff92b5..65da690da 100644
--- 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);
diff --git a/src/storm/logic/ConditionalFormula.cpp b/src/storm/logic/ConditionalFormula.cpp
index a02af1877..70f82eaec 100644
--- 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;
}
}
diff --git a/src/storm/logic/ConditionalFormula.h b/src/storm/logic/ConditionalFormula.h
index 3a32b3463..1c973085a 100644
--- 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;
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index ccafab82c..482731108 100644
--- 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() << "]";
diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h
index 80924865a..b15b17de8 100644
--- 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;
diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp
index 12a77d49b..dcea3d9e2 100644
--- 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;
}
}
diff --git a/src/storm/logic/EventuallyFormula.h b/src/storm/logic/EventuallyFormula.h
index 5fa30da6d..fdce64eb5 100644
--- 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;
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 752389b36..b71316097 100644
--- 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;
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 72631e2fe..92100326a 100644
--- 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;
diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp
index 8387e38fd..462631c62 100644
--- 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;
}
}
diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h
index a14825cc5..1cadc5f62 100644
--- 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;
diff --git a/src/storm/logic/GloballyFormula.cpp b/src/storm/logic/GloballyFormula.cpp
index af429be92..cb9bac874 100644
--- 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;
}
}
diff --git a/src/storm/logic/GloballyFormula.h b/src/storm/logic/GloballyFormula.h
index 6c44ba2a1..3eaa834c3 100644
--- 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;
};
}
}
diff --git a/src/storm/logic/HOAPathFormula.cpp b/src/storm/logic/HOAPathFormula.cpp
index 915f4f13d..cd17a6a46 100644
--- 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) {
diff --git a/src/storm/logic/HOAPathFormula.h b/src/storm/logic/HOAPathFormula.h
index 81352243e..fd9ba1a93 100644
--- 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;
diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp
index 1ed2c1f66..c5e615515 100644
--- 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;
}
diff --git a/src/storm/logic/InstantaneousRewardFormula.h b/src/storm/logic/InstantaneousRewardFormula.h
index 69e5dd38f..6d6b440f6 100644
--- 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;
diff --git a/src/storm/logic/LongRunAverageOperatorFormula.cpp b/src/storm/logic/LongRunAverageOperatorFormula.cpp
index 6f4c061cb..24997ed73 100644
--- 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;
}
}
diff --git a/src/storm/logic/LongRunAverageOperatorFormula.h b/src/storm/logic/LongRunAverageOperatorFormula.h
index 9cc156408..4774537b9 100644
--- 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;
};
}
}
diff --git a/src/storm/logic/LongRunAverageRewardFormula.cpp b/src/storm/logic/LongRunAverageRewardFormula.cpp
index 294c8de95..4dd7a2a33 100644
--- 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() << "]";
diff --git a/src/storm/logic/LongRunAverageRewardFormula.h b/src/storm/logic/LongRunAverageRewardFormula.h
index 45bbe3de5..03b21b761 100644
--- 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;
diff --git a/src/storm/logic/MultiObjectiveFormula.cpp b/src/storm/logic/MultiObjectiveFormula.cpp
index 0ecf795b0..edae6a1ea 100644
--- 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){
diff --git a/src/storm/logic/MultiObjectiveFormula.h b/src/storm/logic/MultiObjectiveFormula.h
index 9ec5204d9..faf774958 100644
--- 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;
};
diff --git a/src/storm/logic/NextFormula.cpp b/src/storm/logic/NextFormula.cpp
index f38df2ac0..c99d4d35c 100644
--- 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;
}
}
diff --git a/src/storm/logic/NextFormula.h b/src/storm/logic/NextFormula.h
index 2083fee98..e67010de0 100644
--- 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;
};
}
}
diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp
index 890d5476c..7bf7bd55f 100644
--- 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");
}
diff --git a/src/storm/logic/OperatorFormula.h b/src/storm/logic/OperatorFormula.h
index c4d3067fb..807661aa2 100644
--- 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;
diff --git a/src/storm/logic/ProbabilityOperatorFormula.cpp b/src/storm/logic/ProbabilityOperatorFormula.cpp
index 0c36a07a5..25af22871 100644
--- 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;
}
}
diff --git a/src/storm/logic/ProbabilityOperatorFormula.h b/src/storm/logic/ProbabilityOperatorFormula.h
index 37950b3cb..92c8a3e87 100644
--- 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;
};
}
}
diff --git a/src/storm/logic/QuantileFormula.cpp b/src/storm/logic/QuantileFormula.cpp
index 4e1e21aef..679d14d99 100644
--- 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() << ", ";
diff --git a/src/storm/logic/QuantileFormula.h b/src/storm/logic/QuantileFormula.h
index 8765013a7..4bfe0a5a1 100644
--- 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;
diff --git a/src/storm/logic/RewardOperatorFormula.cpp b/src/storm/logic/RewardOperatorFormula.cpp
index 28d1678e5..bdceca897 100644
--- 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()) {
diff --git a/src/storm/logic/RewardOperatorFormula.h b/src/storm/logic/RewardOperatorFormula.h
index af9a09056..77564714b 100644
--- 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.
diff --git a/src/storm/logic/TimeOperatorFormula.cpp b/src/storm/logic/TimeOperatorFormula.cpp
index f32568cdc..5fe746a12 100644
--- 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);
diff --git a/src/storm/logic/TimeOperatorFormula.h b/src/storm/logic/TimeOperatorFormula.h
index 080cec30d..0a52cb879 100644
--- 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.
diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp
index fb6f60873..8bd8e26eb 100644
--- 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() << "]";
diff --git a/src/storm/logic/TotalRewardFormula.h b/src/storm/logic/TotalRewardFormula.h
index 1fa366723..42bce45c8 100644
--- 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;
diff --git a/src/storm/logic/UnaryBooleanPathFormula.cpp b/src/storm/logic/UnaryBooleanPathFormula.cpp
index 7613032b6..707599e0b 100644
--- 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;
}
}
diff --git a/src/storm/logic/UnaryBooleanPathFormula.h b/src/storm/logic/UnaryBooleanPathFormula.h
index 3323f6949..f8a78aed5 100644
--- 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;
diff --git a/src/storm/logic/UnaryBooleanStateFormula.cpp b/src/storm/logic/UnaryBooleanStateFormula.cpp
index ef75a0f9b..5592d4589 100644
--- 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;
}
}
diff --git a/src/storm/logic/UnaryBooleanStateFormula.h b/src/storm/logic/UnaryBooleanStateFormula.h
index 4c3cd3c17..14aef7eb1 100644
--- 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;
diff --git a/src/storm/logic/UntilFormula.cpp b/src/storm/logic/UntilFormula.cpp
index d4b09bd4d..945bb9283 100644
--- 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;
}
}
diff --git a/src/storm/logic/UntilFormula.h b/src/storm/logic/UntilFormula.h
index a26542a38..db8804504 100644
--- 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;
};
}
}