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 const& playerIdentifier, std::vector const& playerIds) const { - return storm::logic::Coalition(playerIdentifier, playerIds); + storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector> const& playerIds) const { + return storm::logic::Coalition(playerIds); } std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::Coalition coalition, std::shared_ptr 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 #include +#include + #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(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; - qi::rule, std::vector>, Skipper> coalitionOperator; + qi::rule>>, Skipper> coalitionOperator; qi::rule filterProperty; qi::rule(), 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> strict_double; - storm::logic::Coalition createCoalition(std::vector const& playerIdentifier, std::vector const& playerIds) const; + storm::logic::Coalition createCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::Coalition coalition, std::shared_ptr 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 const& playerNames, - std::vector const& playerIds) : playerNames(playerNames), playerIds(playerIds) { + Coalition::Coalition(std::vector> 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 #include +#include #include "storm/storage/BoostTypes.h" #include "storm/utility/OsDetection.h" @@ -14,14 +15,13 @@ namespace storm { class Coalition { public: Coalition() = default; - Coalition(std::vector const& playerNames, std::vector const& playerIds); + Coalition(std::vector>); Coalition(Coalition const& other) = default; friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition); private: - std::vector playerNames; - std::vector playerIds; + std::vector> playerIds; }; } }