diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 139c3e226..f27aa6e00 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -133,8 +133,19 @@ namespace storm { 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.name("Quantile formula"); - - stateFormula = (orStateFormula | multiFormula | quantileFormula); + + coalitionOperator = (qi::lit("<<") + > *( (identifier[phoenix::push_back(qi::_a, qi::_1)] + | qi::int_[phoenix::push_back(qi::_b, qi::_1)]) % ',' + ) + > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a, qi::_b)]; + coalitionOperator.name("coalition operator"); + + // only LRA for now, need to adapt this (beware of cyclic gameFormula pass!) + gameFormula = (coalitionOperator > longRunAverageOperator)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), storm::logic::Coalition({}, {1}), qi::_1)]; + gameFormula.name("game formula"); + + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula.name("state formula"); formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); @@ -472,5 +483,12 @@ namespace storm { } } + storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector const& playerIdentifier, std::vector const& playerIds) const { + return storm::logic::Coalition(playerIdentifier, playerIds); + } + + std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::Coalition coalition, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); + } } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index b60ef27f0..904d8c852 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -160,7 +160,9 @@ namespace storm { qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; - + + qi::rule, std::vector>, Skipper> coalitionOperator; + qi::rule filterProperty; qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; @@ -199,10 +201,14 @@ namespace storm { qi::rule(), Skipper> multiFormula; qi::rule>, Skipper> quantileBoundVariable; qi::rule(), Skipper> quantileFormula; - + qi::rule(), Skipper> gameFormula; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; + storm::logic::Coalition createCoalition(std::vector const& playerIdentifier, std::vector const& playerIds) const; + std::shared_ptr createGameFormula(storm::logic::Coalition coalition, std::shared_ptr const& subformula) const; + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula);