From bd0a882cd5b664262fc3e3f4a80d2f65c94b0272 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:01 +0200 Subject: [PATCH] (LTL) FormulaInformation: add containsComplexPathFormula() We want to differentiate between a simple path formula (single G, F, U, X, with negation over state formulas) and complex path formulas (nested temporal operators, conjunction/disjunction, etc). Adapt FormulaInformation and FormulaInformationVisitor accordingly. Additionally, we tweak the FormulaInformationVisitor so that we can optionally prohibit recursing into operator subformulas (e.g., P>0[...]). For PRCTL*, such subformulas are treated just as state subformulas, and we would like to have the ability to get FormulaInformation just for the structure of the "surface-level" formula, without looking into the probability, long-run, reward, ... sub-formulas. refactor FormulaInformationVisitor to support stopping recursion into nested operators and for detecting complex path formulas Conflicts: src/storm/logic/Formula.cpp --- src/storm/logic/Formula.cpp | 5 +- src/storm/logic/Formula.h | 2 +- src/storm/logic/FormulaInformation.cpp | 13 ++- src/storm/logic/FormulaInformation.h | 3 + src/storm/logic/FormulaInformationVisitor.cpp | 80 +++++++++++++++---- src/storm/logic/FormulaInformationVisitor.h | 13 ++- 6 files changed, 93 insertions(+), 23 deletions(-) diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 202116dff..7cefa26d1 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -192,9 +192,8 @@ namespace storm { return checker.conformsToSpecification(*this, fragment); } - FormulaInformation Formula::info() const { - FormulaInformationVisitor visitor; - return visitor.getInformation(*this); + FormulaInformation Formula::info(bool recurseIntoOperators) const { + return FormulaInformationVisitor::getInformation(*this, recurseIntoOperators); } std::shared_ptr Formula::getTrueFormula() { diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index e4fec35c6..452ef0f73 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -100,7 +100,7 @@ namespace storm { virtual bool hasQuantitativeResult() const; bool isInFragment(FragmentSpecification const& fragment) const; - FormulaInformation info() const; + FormulaInformation info(bool recurseIntoOperators = true) const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0; diff --git a/src/storm/logic/FormulaInformation.cpp b/src/storm/logic/FormulaInformation.cpp index 4adae5a3c..23d826fe1 100644 --- a/src/storm/logic/FormulaInformation.cpp +++ b/src/storm/logic/FormulaInformation.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - FormulaInformation::FormulaInformation() : mContainsRewardOperator(false), mContainsNextFormula(false), mContainsBoundedUntilFormula(false), mContainsCumulativeRewardFormula(false), mContainsRewardBoundedFormula(false), mContainsLongRunFormula(false) { + FormulaInformation::FormulaInformation() : mContainsRewardOperator(false), mContainsNextFormula(false), mContainsBoundedUntilFormula(false), mContainsCumulativeRewardFormula(false), mContainsRewardBoundedFormula(false), mContainsLongRunFormula(false), mContainsComplexPathFormula(false) { // Intentionally left empty } @@ -30,6 +30,10 @@ namespace storm { return this->mContainsLongRunFormula; } + bool FormulaInformation::containsComplexPathFormula() const { + return this->mContainsComplexPathFormula; + } + FormulaInformation FormulaInformation::join(FormulaInformation const& other) { FormulaInformation result; result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator(); @@ -38,6 +42,7 @@ namespace storm { result.mContainsCumulativeRewardFormula = this->containsCumulativeRewardFormula() || other.containsCumulativeRewardFormula(); result.mContainsRewardBoundedFormula = this->containsRewardBoundedFormula() || other.containsRewardBoundedFormula(); result.mContainsLongRunFormula = this->containsLongRunFormula() || other.containsLongRunFormula(); + result.mContainsComplexPathFormula = this->containsComplexPathFormula() || other.containsComplexPathFormula(); return result; } @@ -70,5 +75,11 @@ namespace storm { this->mContainsLongRunFormula = newValue; return *this; } + + FormulaInformation& FormulaInformation::setContainsComplexPathFormula(bool newValue) { + this->mContainsComplexPathFormula = newValue; + return *this; + } + } } diff --git a/src/storm/logic/FormulaInformation.h b/src/storm/logic/FormulaInformation.h index 6c2c320b2..280fa5e59 100644 --- a/src/storm/logic/FormulaInformation.h +++ b/src/storm/logic/FormulaInformation.h @@ -18,6 +18,7 @@ namespace storm { bool containsCumulativeRewardFormula() const; bool containsRewardBoundedFormula() const; bool containsLongRunFormula() const; + bool containsComplexPathFormula() const; FormulaInformation join(FormulaInformation const& other); @@ -27,6 +28,7 @@ namespace storm { FormulaInformation& setContainsCumulativeRewardFormula(bool newValue = true); FormulaInformation& setContainsRewardBoundedFormula(bool newValue = true); FormulaInformation& setContainsLongRunFormula(bool newValue = true); + FormulaInformation& setContainsComplexPathFormula(bool newValue = true); private: bool mContainsRewardOperator; @@ -35,6 +37,7 @@ namespace storm { bool mContainsCumulativeRewardFormula; bool mContainsRewardBoundedFormula; bool mContainsLongRunFormula; + bool mContainsComplexPathFormula; }; } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index e42bb2cbb..7a0b95f0c 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -4,11 +4,15 @@ namespace storm { namespace logic { - FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f) const { - boost::any result = f.accept(*this, boost::any()); + FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f, bool recurseIntoOperators) { + FormulaInformationVisitor visitor(recurseIntoOperators); + boost::any result = f.accept(visitor, boost::any()); return boost::any_cast(result); } + FormulaInformationVisitor::FormulaInformationVisitor(bool recurseIntoOperators) : recurseIntoOperators(recurseIntoOperators) { + } + boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -22,7 +26,8 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + FormulaInformation result = boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + return result.setContainsComplexPathFormula(); } boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { @@ -46,10 +51,16 @@ namespace storm { for (unsigned i = 0; i < f.getDimension(); ++i) { result.join(boost::any_cast(f.getLeftSubformula(i).accept(*this, data))); result.join(boost::any_cast(f.getRightSubformula(i).accept(*this, data))); + if (f.getLeftSubformula(i).isPathFormula() || f.getRightSubformula(i).isPathFormula()) { + result.setContainsComplexPathFormula(); + } } } else { result.join(boost::any_cast(f.getLeftSubformula().accept(*this, data))); result.join(boost::any_cast(f.getRightSubformula().accept(*this, data))); + if (f.getLeftSubformula().isPathFormula() || f.getRightSubformula().isPathFormula()) { + result.setContainsComplexPathFormula(); + } } return result; } @@ -70,7 +81,11 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + FormulaInformation result = boost::any_cast(f.getSubformula().accept(*this, data)); + if (f.getSubformula().isPathFormula()) { + result.setContainsComplexPathFormula(); + } + return result; } boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { @@ -78,7 +93,11 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + FormulaInformation result = boost::any_cast(f.getSubformula().accept(*this, data)); + if (f.getSubformula().isPathFormula()) { + result.setContainsComplexPathFormula(); + } + return result; } boost::any FormulaInformationVisitor::visit(GameFormula const& f, boost::any const& data) const { @@ -92,7 +111,9 @@ namespace storm { boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { FormulaInformation result; result.setContainsLongRunFormula(true); - result.join(boost::any_cast(f.getSubformula().accept(*this, data))); + if (recurseIntoOperators) { + result.join(boost::any_cast(f.getSubformula().accept(*this, data))); + } return result; } @@ -104,26 +125,45 @@ namespace storm { boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { FormulaInformation result; - for(auto const& subF : f.getSubformulas()){ - result.join(boost::any_cast(subF->accept(*this, data))); + if (recurseIntoOperators) { + for(auto const& subF : f.getSubformulas()){ + result.join(boost::any_cast(subF->accept(*this, data))); + } } return result; } boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + // TODO (joachim): check is this correct? + if (recurseIntoOperators) { + return f.getSubformula().accept(*this, data); + } else { + return FormulaInformation(); + } } boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsNextFormula(); + FormulaInformation result = boost::any_cast(f.getSubformula().accept(*this, data)).setContainsNextFormula(); + if (f.getSubformula().isPathFormula()) { + result.setContainsComplexPathFormula(); + } + return result; } boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + if (recurseIntoOperators) { + return f.getSubformula().accept(*this, data); + } else { + return FormulaInformation(); + } } boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsRewardOperator(); + if (recurseIntoOperators) { + return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsRewardOperator(); + } else { + return FormulaInformation(); + } } boost::any FormulaInformationVisitor::visit(TotalRewardFormula const&, boost::any const&) const { @@ -135,17 +175,25 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + FormulaInformation result = boost::any_cast(f.getSubformula().accept(*this, data)); + result.setContainsComplexPathFormula(); + return result; } boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + FormulaInformation result = boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + if (f.getLeftSubformula().isPathFormula() || f.getRightSubformula().isPathFormula()) { + result.setContainsComplexPathFormula(); + } + return result; } boost::any FormulaInformationVisitor::visit(HOAPathFormula const& f, boost::any const& data) const { FormulaInformation info; - for (auto& mapped : f.getAPMapping()) { - info = info.join(boost::any_cast(mapped.second->accept(*this, data))); + if (recurseIntoOperators) { + for (auto& mapped : f.getAPMapping()) { + info = info.join(boost::any_cast(mapped.second->accept(*this, data))); + } } return info; } diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index 11ba3e80b..8bf7a25a9 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/src/storm/logic/FormulaInformationVisitor.h @@ -9,8 +9,14 @@ namespace storm { class FormulaInformationVisitor : public FormulaVisitor { public: - FormulaInformation getInformation(Formula const& f) const; - + static FormulaInformation getInformation(Formula const& f, bool recurseIntoOperators = true); + + explicit FormulaInformationVisitor(bool recurseIntoOperators); + FormulaInformationVisitor(FormulaInformationVisitor const& other) = default; + FormulaInformationVisitor(FormulaInformationVisitor&& other) = default; + FormulaInformationVisitor& operator=(FormulaInformationVisitor const& other) = default; + FormulaInformationVisitor& operator=(FormulaInformationVisitor&& other) = default; + 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; @@ -37,6 +43,9 @@ namespace storm { 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; + + private: + bool recurseIntoOperators; }; }