Polished fragment specification and formula visitors for new GameFormulas

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -134,14 +134,10 @@ 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");
 
-            coalitionOperator = (qi::lit("<<")
-                    > *(    (identifier[phoenix::push_back(qi::_a, qi::_1)]
-                        |    qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ','
-                        )
-                    > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)];
-            coalitionOperator.name("coalition operator");
+            coalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)];
+            coalition.name("coalition");
 
-            gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            gameFormula = (qi::lit("<<") > coalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             gameFormula.name("game formula");
 
             stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
@@ -482,11 +478,11 @@ namespace storm {
             }
         }
 
-        storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector<boost::variant<std::string, uint64_t>> const& playerIds) const {
+        storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const {
             return storm::logic::Coalition(playerIds);
         }
 
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGameFormula(storm::logic::Coalition coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGameFormula(storm::logic::Coalition const& 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

@@ -163,7 +163,7 @@ 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<boost::variant<std::string, uint64_t>>>, Skipper> coalitionOperator;
+            qi::rule<Iterator, storm::logic::Coalition(), qi::locals<std::vector<boost::variant<std::string, storm::storage::PlayerIndex>>>, Skipper> coalition;
 
             qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
@@ -208,8 +208,8 @@ namespace storm {
             // 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<boost::variant<std::string, uint64_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;
+            storm::logic::Coalition createCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const;
+            std::shared_ptr<storm::logic::Formula const> createGameFormula(storm::logic::Coalition const& 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);

src/storm/logic/FragmentChecker.cpp

@@ -191,7 +191,7 @@ namespace storm {
 
         boost::any FragmentChecker::visit(GameFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
-            bool result = inherited.getSpecification().areCoalitionOperatorsAllowed();
+            bool result = inherited.getSpecification().areGameFormulasAllowed();
             return result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
         }
 

src/storm/logic/FragmentSpecification.cpp

@@ -56,9 +56,11 @@ namespace storm {
         FragmentSpecification rpatl() {
             FragmentSpecification rpatl = prctl();
 
-            // TODO disallow operator we currently do not support
-            rpatl.setCoalitionOperatorsAllowed(true);
-
+            // TODO: disallow formulas we currently do not support
+            // TODO: Only allow OperatorFormulas when they are inside of a GameFormula?
+            // TODO: Require that operator formulas are required at the top level of a GameFormula?
+            rpatl.setGameFormulasAllowed(true);
+            
             return rpatl;
         }
 
@@ -175,6 +177,8 @@ namespace storm {
             
             reachabilityTimeFormula = false;
             
+            gameFormula = false;
+            
             nestedOperators = true;
             nestedPathFormulas = false;
             nestedMultiObjectiveFormulas = false;
@@ -629,15 +633,14 @@ namespace storm {
             return *this;
         }
 
-        bool FragmentSpecification::areCoalitionOperatorsAllowed() const {
-            return coalitionOperator;
+        bool FragmentSpecification::areGameFormulasAllowed() const {
+            return gameFormula;
         }
 
-        FragmentSpecification& FragmentSpecification::setCoalitionOperatorsAllowed(bool newValue) {
-            coalitionOperator = newValue;
+        FragmentSpecification& FragmentSpecification::setGameFormulasAllowed(bool newValue) {
+            gameFormula = newValue;
             return *this;
         }
 
-
     }
 }

src/storm/logic/FragmentSpecification.h

@@ -154,10 +154,9 @@ namespace storm {
             bool isRewardAccumulationAllowed() const;
             FragmentSpecification& setRewardAccumulationAllowed(bool newValue);
 
-            bool areCoalitionOperatorsAllowed() const;
-            FragmentSpecification& setCoalitionOperatorsAllowed(bool newValue);
-
-
+            bool areGameFormulasAllowed() const;
+            FragmentSpecification& setGameFormulasAllowed(bool newValue);
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
             FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -195,7 +194,7 @@ namespace storm {
 
             bool reachabilityTimeFormula;
 
-            bool coalitionOperator;
+            bool gameFormula;
 
             // Members that indicate certain restrictions.
             bool nestedOperators;

src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@@ -76,7 +76,9 @@ namespace storm {
         }
 
         boost::any LiftableTransitionRewardsVisitor::visit(GameFormula const& f, boost::any const& data) const {
-            return true;
+            STORM_LOG_WARN("Transitionbranch-based rewards might be reduced to action-based rewards. Be sure that this is correct for your property.");
+            // TODO: Check if this is correct
+            return f.getSubformula().accept(*this, data);
         }
 
         boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {

src/storm/storage/jani/JSONExporter.cpp

@@ -333,7 +333,7 @@ namespace storm {
         }
 
         boost::any FormulaToJaniJson::visit(storm::logic::GameFormula const& f, boost::any const& data) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We currently do not support conversion of game formulas to Jani. (Does jani support games?)");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Conversion of game formulas to Jani is not supported.");
         }
 
         boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const {