From 487eb13a243f01e7b57863b31e4e8eff3f2895c0 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Thu, 19 Nov 2020 18:23:32 +0100
Subject: [PATCH] WIP added grammar rules for gameFormula

Does not compile at this stage! This commit will be squashed asap.
---
 .../parser/FormulaParserGrammar.cpp           | 22 +++++++++++++++++--
 .../parser/FormulaParserGrammar.h             | 10 +++++++--
 2 files changed, 28 insertions(+), 4 deletions(-)

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<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));
+        }
     }
 }
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<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardOperator;
             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);