From 5482a32b8a177e444d1bcca00908a8f0247053e0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:00 +0200 Subject: [PATCH] (LTL) Refactor unary/boolean state formulas to allow path formulas as well Previously, the formula parser only supported AND, OR and NOT over state formulas. For LTL, we need those over path formulas. We tweak the grammar, the AST types and visitors, to also handle UnaryBooleanPathFormula and BinaryBooleanPathformula. During parsing, we determine on-demand whether to generate the path or state formula variant by looking at the subformulas - if they are state formulas, the boolean operator will be a state formula as well. Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.cpp src/storm/logic/Formula.h src/storm/logic/FragmentChecker.cpp src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/storage/jani/JSONExporter.cpp --- .../parser/FormulaParserGrammar.cpp | 52 ++++++++++++++----- .../parser/FormulaParserGrammar.h | 16 +++--- src/storm/logic/BinaryBooleanOperatorType.h | 7 +++ src/storm/logic/BinaryBooleanPathFormula.cpp | 47 +++++++++++++++++ src/storm/logic/BinaryBooleanPathFormula.h | 38 ++++++++++++++ src/storm/logic/BinaryBooleanStateFormula.h | 3 +- src/storm/logic/CloneVisitor.cpp | 11 ++++ src/storm/logic/CloneVisitor.h | 2 + src/storm/logic/Formula.cpp | 8 +++ src/storm/logic/Formula.h | 3 ++ src/storm/logic/FormulaInformationVisitor.cpp | 12 ++++- src/storm/logic/FormulaInformationVisitor.h | 2 + src/storm/logic/FormulaVisitor.h | 2 + src/storm/logic/Formulas.h | 2 + src/storm/logic/FormulasForwardDeclarations.h | 2 + src/storm/logic/FragmentChecker.cpp | 15 ++++++ src/storm/logic/FragmentChecker.h | 2 + src/storm/logic/FragmentSpecification.cpp | 19 +++++-- src/storm/logic/FragmentSpecification.h | 8 +++ .../LiftableTransitionRewardsVisitor.cpp | 10 ++++ .../logic/LiftableTransitionRewardsVisitor.h | 2 + src/storm/logic/ToExpressionVisitor.cpp | 10 +++- src/storm/logic/ToExpressionVisitor.h | 2 + src/storm/logic/UnaryBooleanOperatorType.h | 7 +++ src/storm/logic/UnaryBooleanPathFormula.cpp | 39 ++++++++++++++ src/storm/logic/UnaryBooleanPathFormula.h | 35 +++++++++++++ src/storm/logic/UnaryBooleanStateFormula.h | 3 +- src/storm/storage/jani/JSONExporter.cpp | 17 ++++++ src/storm/storage/jani/JSONExporter.h | 2 + 29 files changed, 351 insertions(+), 27 deletions(-) create mode 100644 src/storm/logic/BinaryBooleanOperatorType.h create mode 100644 src/storm/logic/BinaryBooleanPathFormula.cpp create mode 100644 src/storm/logic/BinaryBooleanPathFormula.h create mode 100644 src/storm/logic/UnaryBooleanOperatorType.h create mode 100644 src/storm/logic/UnaryBooleanPathFormula.cpp create mode 100644 src/storm/logic/UnaryBooleanPathFormula.h diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 95a27d70c..d768fab9b 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -52,13 +52,13 @@ namespace storm { operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator; operatorFormula.name("operator formulas"); - atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; + atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula"); - atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; + atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula without expression"); - notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1]; + notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula(qi::_r1)[qi::_val = qi::_1]; notStateFormula.name("negation formula"); eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; @@ -70,7 +70,7 @@ namespace storm { nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula; + pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula(qi::_r1); pathFormulaWithoutUntil.name("path formula"); untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; @@ -78,7 +78,7 @@ namespace storm { hoaPathFormula = qi::lit("HOA:") > qi::lit("{") > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] - >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] + >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula(qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] > qi::lit("}"); basicPathFormula = (hoaPathFormula(qi::_r1)[qi::_val = qi::_1]) | untilFormula(qi::_r1)[qi::_val = qi::_1]; @@ -112,7 +112,7 @@ namespace storm { operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); - longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula(storm::logic::FormulaContext::LongRunAverage) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; longRunAverageOperator.name("long-run average operator"); rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); @@ -127,13 +127,13 @@ namespace storm { probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; probabilityOperator.name("probability operator"); - andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; + andStateFormula = notStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; andStateFormula.name("and state formula"); - orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; + orStateFormula = andStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula.name("or state formula"); - multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)]; + multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula(storm::logic::FormulaContext::Probability)) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)]; multiFormula.name("Multi formula"); identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; @@ -141,7 +141,7 @@ namespace storm { quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a, qi::_1)]; quantileBoundVariable.name("quantile bound variable"); - quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; quantileFormula.name("Quantile formula"); playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)]; @@ -166,7 +166,7 @@ namespace storm { qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; shieldComparison.name("shield comparison type"); - stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); + stateFormula = (orStateFormula(qi::_r1) | multiFormula | quantileFormula); stateFormula.name("state formula"); quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]]; @@ -183,7 +183,7 @@ namespace storm { #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -452,6 +452,34 @@ namespace storm { } } + std::shared_ptr FormulaParserGrammar::createBinaryBooleanPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType) { + return std::shared_ptr(new storm::logic::BinaryBooleanPathFormula(operatorType, leftSubformula, rightSubformula)); + } + + std::shared_ptr FormulaParserGrammar::createUnaryBooleanPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + if (operatorType) { + return std::shared_ptr(new storm::logic::UnaryBooleanPathFormula(operatorType.get(), subformula)); + } else { + return subformula; + } + } + + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateOrPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType) { + if (leftSubformula->isStateFormula() && rightSubformula->isStateFormula()) { + return createBinaryBooleanStateFormula(leftSubformula, rightSubformula, operatorType); + } else { + return createBinaryBooleanPathFormula(leftSubformula, rightSubformula, operatorType); + } + } + + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateOrPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + if (subformula->isStateFormula()) { + return createUnaryBooleanStateFormula(subformula, operatorType); + } else { + return createUnaryBooleanPathFormula(subformula, operatorType); + } + } + std::shared_ptr FormulaParserGrammar::createMultiFormula(std::vector> const& subformulas) { bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty(); for (auto const& subformula : subformulas) { diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index c40842532..2bba99c73 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -165,19 +165,19 @@ namespace storm { qi::rule filterProperty; qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> stateFormula; qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; qi::rule(), Skipper> simplePathFormula; - qi::rule(), Skipper> atomicStateFormula; - qi::rule(), Skipper> atomicStateFormulaWithoutExpression; + qi::rule(storm::logic::FormulaContext), Skipper> atomicStateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> atomicStateFormulaWithoutExpression; qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; - qi::rule(), Skipper> andStateFormula; - qi::rule(), Skipper> orStateFormula; - qi::rule(), Skipper> notStateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> andStateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> orStateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> notStateFormula; qi::rule(), Skipper> labelFormula; qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; @@ -250,7 +250,11 @@ namespace storm { std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + std::shared_ptr createBinaryBooleanPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType); + std::shared_ptr createBinaryBooleanStateOrPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + std::shared_ptr createUnaryBooleanPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + std::shared_ptr createUnaryBooleanStateOrPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiFormula(std::vector> const& subformulas); storm::expressions::Variable createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName); std::shared_ptr createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula); diff --git a/src/storm/logic/BinaryBooleanOperatorType.h b/src/storm/logic/BinaryBooleanOperatorType.h new file mode 100644 index 000000000..8c4c141a4 --- /dev/null +++ b/src/storm/logic/BinaryBooleanOperatorType.h @@ -0,0 +1,7 @@ +#pragma once + +namespace storm { + namespace logic { + enum class BinaryBooleanOperatorType {And, Or}; + } +} diff --git a/src/storm/logic/BinaryBooleanPathFormula.cpp b/src/storm/logic/BinaryBooleanPathFormula.cpp new file mode 100644 index 000000000..aa84f23f7 --- /dev/null +++ b/src/storm/logic/BinaryBooleanPathFormula.cpp @@ -0,0 +1,47 @@ +#include "storm/logic/BinaryBooleanPathFormula.h" + +#include "storm/logic/FormulaVisitor.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace logic { + BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula), operatorType(operatorType) { + STORM_LOG_THROW(this->getLeftSubformula().isStateFormula() || this->getLeftSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); + STORM_LOG_THROW(this->getRightSubformula().isStateFormula() || this->getRightSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); + } + + bool BinaryBooleanPathFormula::isBinaryBooleanPathFormula() const { + return true; + } + + boost::any BinaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + BinaryBooleanPathFormula::OperatorType BinaryBooleanPathFormula::getOperator() const { + return operatorType; + } + + bool BinaryBooleanPathFormula::isAnd() const { + return this->getOperator() == OperatorType::And; + } + + bool BinaryBooleanPathFormula::isOr() const { + return this->getOperator() == OperatorType::Or; + } + + std::ostream& BinaryBooleanPathFormula::writeToStream(std::ostream& out) const { + out << "("; + this->getLeftSubformula().writeToStream(out); + switch (operatorType) { + case OperatorType::And: out << " & "; break; + case OperatorType::Or: out << " | "; break; + } + this->getRightSubformula().writeToStream(out); + out << ")"; + return out; + } + } +} diff --git a/src/storm/logic/BinaryBooleanPathFormula.h b/src/storm/logic/BinaryBooleanPathFormula.h new file mode 100644 index 000000000..6f60f06f4 --- /dev/null +++ b/src/storm/logic/BinaryBooleanPathFormula.h @@ -0,0 +1,38 @@ +#ifndef STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_ +#define STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_ + +#include + +#include "storm/logic/BinaryPathFormula.h" +#include "storm/logic/BinaryBooleanOperatorType.h" + +namespace storm { + namespace logic { + class BinaryBooleanPathFormula : public BinaryPathFormula { + public: + typedef storm::logic::BinaryBooleanOperatorType OperatorType; + + BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + + virtual ~BinaryBooleanPathFormula() { + // Intentionally left empty. + }; + + virtual bool isBinaryBooleanPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + + OperatorType getOperator() const; + + virtual bool isAnd() const; + virtual bool isOr() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + private: + OperatorType operatorType; + }; + } +} + +#endif /* STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_ */ diff --git a/src/storm/logic/BinaryBooleanStateFormula.h b/src/storm/logic/BinaryBooleanStateFormula.h index 9a884e60a..085b4fb24 100644 --- a/src/storm/logic/BinaryBooleanStateFormula.h +++ b/src/storm/logic/BinaryBooleanStateFormula.h @@ -4,12 +4,13 @@ #include #include "storm/logic/BinaryStateFormula.h" +#include "storm/logic/BinaryBooleanOperatorType.h" namespace storm { namespace logic { class BinaryBooleanStateFormula : public BinaryStateFormula { public: - enum class OperatorType {And, Or}; + typedef storm::logic::BinaryBooleanOperatorType OperatorType; BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 15499c9d9..ca1af66d9 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -24,6 +24,12 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getOperator(), left, right)); } + boost::any CloneVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { + std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); + std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(f.getOperator(), left, right)); + } + boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -170,6 +176,11 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getOperator(), subformula)); } + boost::any CloneVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(f.getOperator(), subformula)); + } + boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h index 954d46db4..3b5bc1054 100644 --- a/src/storm/logic/CloneVisitor.h +++ b/src/storm/logic/CloneVisitor.h @@ -15,6 +15,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -34,6 +35,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; }; diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 553e15b89..202116dff 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -43,6 +43,14 @@ namespace storm { return false; } + bool Formula::isBinaryBooleanPathFormula() const { + return false; + } + + bool Formula::isUnaryBooleanPathFormula() const { + return false; + } + bool Formula::isBooleanLiteralFormula() const { return false; } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 0014baef4..e4fec35c6 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -47,6 +47,9 @@ namespace storm { virtual bool isBinaryBooleanStateFormula() const; virtual bool isUnaryBooleanStateFormula() const; + virtual bool isBinaryBooleanPathFormula() const; + virtual bool isUnaryBooleanPathFormula() const; + virtual bool isMultiObjectiveFormula() const; virtual bool isQuantileFormula() const; diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 471503e2a..e42bb2cbb 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -17,10 +17,14 @@ namespace storm { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { - return FormulaInformation(); + boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); } + 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))); + } + boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -130,6 +134,10 @@ namespace storm { return f.getSubformula().accept(*this, data); } + boost::any FormulaInformationVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const { return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); } diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index a1f3a3fb0..11ba3e80b 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/src/storm/logic/FormulaInformationVisitor.h @@ -14,6 +14,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -33,6 +34,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; }; diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index b1c6db105..def8cf722 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/src/storm/logic/FormulaVisitor.h @@ -15,6 +15,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0; @@ -34,6 +35,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const = 0; }; diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h index 47ceae22a..82c44604e 100644 --- a/src/storm/logic/Formulas.h +++ b/src/storm/logic/Formulas.h @@ -2,6 +2,7 @@ #include "storm/logic/AtomicExpressionFormula.h" #include "storm/logic/AtomicLabelFormula.h" #include "storm/logic/BinaryBooleanStateFormula.h" +#include "storm/logic/BinaryBooleanPathFormula.h" #include "storm/logic/BinaryPathFormula.h" #include "storm/logic/BinaryStateFormula.h" #include "storm/logic/BooleanLiteralFormula.h" @@ -25,6 +26,7 @@ #include "storm/logic/TimeOperatorFormula.h" #include "storm/logic/TotalRewardFormula.h" #include "storm/logic/UnaryBooleanStateFormula.h" +#include "storm/logic/UnaryBooleanPathFormula.h" #include "storm/logic/UnaryPathFormula.h" #include "storm/logic/UnaryStateFormula.h" #include "storm/logic/UntilFormula.h" diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index 41aca3c3b..0dc68db03 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/src/storm/logic/FormulasForwardDeclarations.h @@ -8,6 +8,7 @@ namespace storm { class AtomicExpressionFormula; class AtomicLabelFormula; class BinaryBooleanStateFormula; + class BinaryBooleanPathFormula; class BinaryPathFormula; class BinaryStateFormula; class BooleanLiteralFormula; @@ -33,6 +34,7 @@ namespace storm { class StateFormula; class TotalRewardFormula; class UnaryBooleanStateFormula; + class UnaryBooleanPathFormula; class UnaryPathFormula; class UnaryStateFormula; class UntilFormula; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 0c76dec44..c40d703c9 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -52,6 +52,14 @@ namespace storm { return result; } + boost::any FragmentChecker::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areBinaryBooleanPathFormulasAllowed(); + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); + return result; + } + boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); @@ -311,6 +319,13 @@ namespace storm { return result; } + boost::any FragmentChecker::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areUnaryBooleanPathFormulasAllowed(); + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; + } + boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areUntilFormulasAllowed(); diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index e027f7c46..3d9f50a2b 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/src/storm/logic/FragmentChecker.h @@ -15,6 +15,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -34,6 +35,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; }; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 445ae0b8c..c00d53cf7 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -175,6 +175,8 @@ namespace storm { booleanLiteralFormula = false; unaryBooleanStateFormula = false; binaryBooleanStateFormula = false; + unaryBooleanPathFormula = false; + binaryBooleanPathFormula = false; cumulativeRewardFormula = false; instantaneousRewardFormula = false; @@ -372,12 +374,21 @@ namespace storm { return *this; } - bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const { - return binaryBooleanStateFormula; + bool FragmentSpecification::areUnaryBooleanPathFormulasAllowed() const { + return unaryBooleanPathFormula; } - FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) { - this->binaryBooleanStateFormula = newValue; + FragmentSpecification& FragmentSpecification::setUnaryBooleanPathFormulasAllowed(bool newValue) { + this->unaryBooleanPathFormula = newValue; + return *this; + } + + bool FragmentSpecification::areBinaryBooleanPathFormulasAllowed() const { + return binaryBooleanPathFormula; + } + + FragmentSpecification& FragmentSpecification::setBinaryBooleanPathFormulasAllowed(bool newValue) { + this->binaryBooleanPathFormula = newValue; return *this; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 5f656695e..07dd5c3da 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -70,9 +70,15 @@ namespace storm { bool areUnaryBooleanStateFormulasAllowed() const; FragmentSpecification& setUnaryBooleanStateFormulasAllowed(bool newValue); + bool areUnaryBooleanPathFormulasAllowed() const; + FragmentSpecification& setUnaryBooleanPathFormulasAllowed(bool newValue); + bool areBinaryBooleanStateFormulasAllowed() const; FragmentSpecification& setBinaryBooleanStateFormulasAllowed(bool newValue); + bool areBinaryBooleanPathFormulasAllowed() const; + FragmentSpecification& setBinaryBooleanPathFormulasAllowed(bool newValue); + bool areCumulativeRewardFormulasAllowed() const; FragmentSpecification& setCumulativeRewardFormulasAllowed(bool newValue); @@ -190,6 +196,8 @@ namespace storm { bool booleanLiteralFormula; bool unaryBooleanStateFormula; bool binaryBooleanStateFormula; + bool unaryBooleanPathFormula; + bool binaryBooleanPathFormula; bool cumulativeRewardFormula; bool instantaneousRewardFormula; diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index 5a0219242..fbb215440 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -23,9 +23,15 @@ namespace storm { } boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { + // TODO joachim: is this correct? return true; } + boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this)); + } + + boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return true; } @@ -143,6 +149,10 @@ namespace storm { return f.getSubformula().accept(*this, data); } + boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const { return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this)); } diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h index db5530cad..bf2b6a4f5 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.h +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h @@ -21,6 +21,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -40,6 +41,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index 41688ad8e..ff1025fca 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -37,6 +37,10 @@ namespace storm { return boost::any(); } + boost::any ToExpressionVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { storm::expressions::Expression result; if (f.isTrueFormula()) { @@ -124,7 +128,11 @@ namespace storm { } return boost::any(); } - + + boost::any ToExpressionVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(UntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h index eb7e261f2..a97a9a4b0 100644 --- a/src/storm/logic/ToExpressionVisitor.h +++ b/src/storm/logic/ToExpressionVisitor.h @@ -15,6 +15,7 @@ namespace storm { virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -34,6 +35,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; }; diff --git a/src/storm/logic/UnaryBooleanOperatorType.h b/src/storm/logic/UnaryBooleanOperatorType.h new file mode 100644 index 000000000..915a11f8a --- /dev/null +++ b/src/storm/logic/UnaryBooleanOperatorType.h @@ -0,0 +1,7 @@ +#pragma once + +namespace storm { + namespace logic { + enum class UnaryBooleanOperatorType {Not}; + } +} diff --git a/src/storm/logic/UnaryBooleanPathFormula.cpp b/src/storm/logic/UnaryBooleanPathFormula.cpp new file mode 100644 index 000000000..61b699d55 --- /dev/null +++ b/src/storm/logic/UnaryBooleanPathFormula.cpp @@ -0,0 +1,39 @@ +#include "storm/logic/UnaryBooleanPathFormula.h" + +#include "storm/logic/FormulaVisitor.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace logic { + UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryPathFormula(subformula), operatorType(operatorType) { + STORM_LOG_THROW(this->getSubformula().isStateFormula() || this->getSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas"); + } + + bool UnaryBooleanPathFormula::isUnaryBooleanPathFormula() const { + return true; + } + + boost::any UnaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + UnaryBooleanPathFormula::OperatorType UnaryBooleanPathFormula::getOperator() const { + return operatorType; + } + + bool UnaryBooleanPathFormula::isNot() const { + return this->getOperator() == OperatorType::Not; + } + + std::ostream& UnaryBooleanPathFormula::writeToStream(std::ostream& out) const { + switch (operatorType) { + case OperatorType::Not: out << "!("; break; + } + this->getSubformula().writeToStream(out); + out << ")"; + return out; + } + } +} diff --git a/src/storm/logic/UnaryBooleanPathFormula.h b/src/storm/logic/UnaryBooleanPathFormula.h new file mode 100644 index 000000000..bbef7aeac --- /dev/null +++ b/src/storm/logic/UnaryBooleanPathFormula.h @@ -0,0 +1,35 @@ +#ifndef STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_ +#define STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_ + +#include "storm/logic/UnaryPathFormula.h" +#include "storm/logic/UnaryBooleanOperatorType.h" + +namespace storm { + namespace logic { + class UnaryBooleanPathFormula : public UnaryPathFormula { + public: + typedef storm::logic::UnaryBooleanOperatorType OperatorType; + + UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr const& subformula); + + virtual ~UnaryBooleanPathFormula() { + // Intentionally left empty. + }; + + virtual bool isUnaryBooleanPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + + OperatorType getOperator() const; + + virtual bool isNot() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + private: + OperatorType operatorType; + }; + } +} + +#endif /* STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_ */ diff --git a/src/storm/logic/UnaryBooleanStateFormula.h b/src/storm/logic/UnaryBooleanStateFormula.h index 19420ec16..4c3cd3c17 100644 --- a/src/storm/logic/UnaryBooleanStateFormula.h +++ b/src/storm/logic/UnaryBooleanStateFormula.h @@ -2,12 +2,13 @@ #define STORM_LOGIC_UNARYBOOLEANSTATEFORMULA_H_ #include "storm/logic/UnaryStateFormula.h" +#include "storm/logic/UnaryBooleanOperatorType.h" namespace storm { namespace logic { class UnaryBooleanStateFormula : public UnaryStateFormula { public: - enum class OperatorType { Not }; + typedef storm::logic::UnaryBooleanOperatorType OperatorType; UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index f89e1cab5..5706618c6 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -208,6 +208,14 @@ namespace storm { opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); return opDecl; } + boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const{ + ExportJsonType opDecl; + storm::logic::BinaryBooleanPathFormula::OperatorType op = f.getOperator(); + opDecl["op"] = op == storm::logic::BinaryBooleanPathFormula::OperatorType::And ? "∧" : "∨"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, data)); + return opDecl; + } boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const { ExportJsonType opDecl(f.isTrueFormula() ? true : false); return opDecl; @@ -588,6 +596,15 @@ namespace storm { return opDecl; } + boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanPathFormula const& f, boost::any const& data) const { + ExportJsonType opDecl; + storm::logic::UnaryBooleanPathFormula::OperatorType op = f.getOperator(); + assert(op == storm::logic::UnaryBooleanPathFormula::OperatorType::Not); + opDecl["op"] = "¬"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { ExportJsonType opDecl; opDecl["op"] = "U"; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index c14524f69..a00088cb1 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -52,6 +52,7 @@ namespace storm { virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; @@ -71,6 +72,7 @@ namespace storm { virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::TotalRewardFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::UnaryBooleanPathFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::HOAPathFormula const& f, boost::any const& data) const;