From b04d2723c2e580212463f0c0c3b89353fed4450f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:03 +0200 Subject: [PATCH] (LTL) Add Formula::toPrefixString() Convert a formula into prefix format (LBTT/ltl2dstar-style LTL syntax). Conflicts: src/storm/logic/Formula.h --- src/storm/logic/Formula.cpp | 7 + src/storm/logic/Formula.h | 1 + src/storm/logic/ToPrefixStringVisitor.cpp | 155 ++++++++++++++++++++++ src/storm/logic/ToPrefixStringVisitor.h | 42 ++++++ 4 files changed, 205 insertions(+) create mode 100644 src/storm/logic/ToPrefixStringVisitor.cpp create mode 100644 src/storm/logic/ToPrefixStringVisitor.h diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 7cefa26d1..752389b36 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -8,6 +8,7 @@ #include "storm/logic/LabelSubstitutionVisitor.h" #include "storm/logic/RewardModelNameSubstitutionVisitor.h" #include "storm/logic/ToExpressionVisitor.h" +#include "storm/logic/ToPrefixStringVisitor.h" namespace storm { namespace logic { @@ -567,5 +568,11 @@ namespace storm { std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } + + std::string Formula::toPrefixString() const { + ToPrefixStringVisitor visitor; + return visitor.toPrefixString(*this); + } + } } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 452ef0f73..72631e2fe 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -237,6 +237,7 @@ namespace storm { std::string toString() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; + std::string toPrefixString() const; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const; diff --git a/src/storm/logic/ToPrefixStringVisitor.cpp b/src/storm/logic/ToPrefixStringVisitor.cpp new file mode 100644 index 000000000..a3d55b994 --- /dev/null +++ b/src/storm/logic/ToPrefixStringVisitor.cpp @@ -0,0 +1,155 @@ +#include "storm/logic/ToPrefixStringVisitor.h" + +#include "storm/logic/Formulas.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace logic { + + std::string ToPrefixStringVisitor::toPrefixString(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast(result); + } + + boost::any ToPrefixStringVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { + return std::string("\"" + f.getLabel() + "\""); + } + + boost::any ToPrefixStringVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { + std::string left = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); + switch (f.getOperator()) { + case BinaryBooleanStateFormula::OperatorType::And: + return std::string("& ") + left + " " + right; + break; + case BinaryBooleanStateFormula::OperatorType::Or: + return std::string("| ") + left + " " + right; + break; + } + return boost::any(); + } + + boost::any ToPrefixStringVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { + std::string left = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); + switch (f.getOperator()) { + case BinaryBooleanPathFormula::OperatorType::And: + return std::string("& ") + left + " " + right; + break; + case BinaryBooleanPathFormula::OperatorType::Or: + return std::string("| ") + left + " " + right; + break; + } + return boost::any(); + } + + boost::any ToPrefixStringVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { + storm::expressions::Expression result; + if (f.isTrueFormula()) { + return std::string("t"); + } else { + return std::string("f"); + } + return result; + } + + boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(ConditionalFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { + std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); + return std::string("F ") + subexpression; + } + + boost::any ToPrefixStringVisitor::visit(TimeOperatorFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(GloballyFormula const& f, boost::any const& data) const { + std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); + return std::string("G ") + subexpression; + } + + boost::any ToPrefixStringVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(QuantileFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(NextFormula const& f, boost::any const& data) const { + std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); + return std::string("X ") + subexpression; + } + + boost::any ToPrefixStringVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(RewardOperatorFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(TotalRewardFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { + std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); + switch (f.getOperator()) { + case UnaryBooleanStateFormula::OperatorType::Not: + return std::string("! ") + subexpression; + break; + } + return boost::any(); + } + + boost::any ToPrefixStringVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); + switch (f.getOperator()) { + case UnaryBooleanPathFormula::OperatorType::Not: + return std::string("! ") + subexpression; + break; + } + return boost::any(); + } + + boost::any ToPrefixStringVisitor::visit(UntilFormula const& f, boost::any const& data) const { + std::string left = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); + return std::string("U ") + left + " " + right; + } + + boost::any ToPrefixStringVisitor::visit(HOAPathFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + } +} diff --git a/src/storm/logic/ToPrefixStringVisitor.h b/src/storm/logic/ToPrefixStringVisitor.h new file mode 100644 index 000000000..95d1bc585 --- /dev/null +++ b/src/storm/logic/ToPrefixStringVisitor.h @@ -0,0 +1,42 @@ +#pragma once + +#include "storm/logic/FormulaVisitor.h" + +#include + +namespace storm { + namespace logic { + + class ToPrefixStringVisitor : public FormulaVisitor { + public: + std::string toPrefixString(Formula const& f) const; + + 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(BoundedUntilFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; + virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; + virtual boost::any visit(QuantileFormula const& f, boost::any const& data) const override; + virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; + 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; + }; + + } +} +