WIP added grammar rules for gameFormula

Does not compile at this stage! This commit will be squashed asap.

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -134,7 +134,18 @@ namespace storm {
             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<std::string> const& playerIdentifier, std::vector<uint_fast32_t> const& playerIds) const {
+            return storm::logic::Coalition(playerIdentifier, playerIds);
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGameFormula(storm::logic::Coalition coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GameFormula(coalition, subformula));
+        }
     }
 }

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -161,6 +161,8 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> timeOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageOperator;
 
+            qi::rule<Iterator, storm::logic::Coalition(), qi::locals<std::vector<std::string>, std::vector<uint_fast32_t>>, Skipper> coalitionOperator;
+
             qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
@@ -199,10 +201,14 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiFormula;
             qi::rule<Iterator, storm::expressions::Variable(), qi::locals<boost::optional<storm::solver::OptimizationDirection>>, Skipper> quantileBoundVariable;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> quantileFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> gameFormula;
 
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
             boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
 
+            storm::logic::Coalition createCoalition(std::vector<std::string> const& playerIdentifier, std::vector<uint_fast32_t> const& playerIds) const;
+            std::shared_ptr<storm::logic::Formula const> createGameFormula(storm::logic::Coalition coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
+
             bool areConstantDefinitionsAllowed() const;
             void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
             void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);