From a9868fd50137ec38ae1432565ba0aaed95fc1fce Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 23 Nov 2020 18:09:24 +0100
Subject: [PATCH] refactor Coalition to use boost variant

---
 src/storm-parsers/parser/FormulaParserGrammar.cpp |  8 ++++----
 src/storm-parsers/parser/FormulaParserGrammar.h   |  6 ++++--
 src/storm/logic/Coalition.cpp                     | 14 ++++++--------
 src/storm/logic/Coalition.h                       |  6 +++---
 4 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp
index f27aa6e00..4984cc929 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.cpp
+++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp
@@ -136,9 +136,9 @@ namespace storm {
 
             coalitionOperator = (qi::lit("<<")
                     > *(    (identifier[phoenix::push_back(qi::_a, qi::_1)]
-                        |    qi::int_[phoenix::push_back(qi::_b, qi::_1)]) % ','
+                        |    qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ','
                         )
-                    > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a, qi::_b)];
+                    > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)];
             coalitionOperator.name("coalition operator");
 
             // only LRA for now, need to adapt this (beware of cyclic gameFormula pass!)
@@ -483,8 +483,8 @@ 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);
+        storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector<boost::variant<std::string, uint64_t>> 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 {
diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h
index 904d8c852..7693019d3 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.h
+++ b/src/storm-parsers/parser/FormulaParserGrammar.h
@@ -3,6 +3,8 @@
 #include <memory>
 #include <fstream>
 
+#include <boost/variant.hpp>
+
 #include "storm-parsers/parser/SpiritErrorHandler.h"
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/storage/jani/Property.h"
@@ -161,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<std::string>, std::vector<uint_fast32_t>>, Skipper> coalitionOperator;
+            qi::rule<Iterator, storm::logic::Coalition(), qi::locals<std::vector<boost::variant<std::string, uint64_t>>>, Skipper> coalitionOperator;
 
             qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
@@ -206,7 +208,7 @@ 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<std::string> const& playerIdentifier, std::vector<uint_fast32_t> const& playerIds) const;
+            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;
 
             bool areConstantDefinitionsAllowed() const;
diff --git a/src/storm/logic/Coalition.cpp b/src/storm/logic/Coalition.cpp
index ff67d735b..0781aaece 100644
--- a/src/storm/logic/Coalition.cpp
+++ b/src/storm/logic/Coalition.cpp
@@ -3,20 +3,18 @@
 namespace storm {
     namespace logic {
 
-        Coalition::Coalition(std::vector<std::string> const& playerNames,
-                             std::vector<uint_fast32_t> const& playerIds) : playerNames(playerNames), playerIds(playerIds) {
+        Coalition::Coalition(std::vector<boost::variant<std::string, uint64_t>> playerIds) : playerIds(playerIds) {
             // Intentionally left empty.
         }
 
         std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) {
+            bool firstItem = true;
             stream << "<<";
-            for (auto const& playerName : coalition.playerNames) {
-                stream << playerName << ", ";
+            for (auto const& id : coalition.playerIds) {
+                if(firstItem) { firstItem = false; } else { stream << ","; }
+                stream << id;
             }
-            for (auto const& playerId : coalition.playerIds) {
-                stream << playerId << ", ";
-            }
-            stream << ">>";
+            stream << ">> ";
             return stream;
         }
     }
diff --git a/src/storm/logic/Coalition.h b/src/storm/logic/Coalition.h
index 108ea53ef..73ea92ac4 100644
--- a/src/storm/logic/Coalition.h
+++ b/src/storm/logic/Coalition.h
@@ -5,6 +5,7 @@
 #include <string>
 
 #include <boost/optional.hpp>
+#include <boost/variant.hpp>
 #include "storm/storage/BoostTypes.h"
 #include "storm/utility/OsDetection.h"
 
@@ -14,14 +15,13 @@ namespace storm {
         class Coalition {
         public:
             Coalition() = default;
-            Coalition(std::vector<std::string> const& playerNames, std::vector<uint_fast32_t> const& playerIds);
+            Coalition(std::vector<boost::variant<std::string, uint64_t>>);
             Coalition(Coalition const& other) = default;
 
             friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition);
 
         private:
-            std::vector<std::string> playerNames;
-            std::vector<uint_fast32_t> playerIds;
+            std::vector<boost::variant<std::string, uint64_t>> playerIds;
         };
     }
 }