diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 63de57930..87fe8edc9 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -134,10 +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"); - 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"); + playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)]; + playerCoalition.name("player coalition"); - gameFormula = (qi::lit("<<") > coalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + gameFormula = (qi::lit("<<") > playerCoalition > 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); @@ -478,11 +478,11 @@ namespace storm { } } - storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector> const& playerIds) const { - return storm::logic::Coalition(playerIds); + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { + return storm::logic::PlayerCoalition(playerIds); } - std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::Coalition const& coalition, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 4e3ea1646..e709366cd 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -163,7 +163,7 @@ namespace storm { qi::rule(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; - qi::rule>>, Skipper> coalition; + qi::rule>>, Skipper> playerCoalition; qi::rule filterProperty; qi::rule(), 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> strict_double; - storm::logic::Coalition createCoalition(std::vector> const& playerIds) const; - std::shared_ptr createGameFormula(storm::logic::Coalition const& coalition, std::shared_ptr const& subformula) const; + storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; + std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp index ae7c213fa..64fdc60b8 100644 --- a/src/storm/logic/GameFormula.cpp +++ b/src/storm/logic/GameFormula.cpp @@ -4,7 +4,7 @@ namespace storm { namespace logic { - GameFormula::GameFormula(Coalition const& coalition, std::shared_ptr subformula) : UnaryStateFormula(subformula), coalition(coalition) { + GameFormula::GameFormula(PlayerCoalition const& coalition, std::shared_ptr subformula) : UnaryStateFormula(subformula), coalition(coalition) { // Intentionally left empty. } @@ -20,7 +20,7 @@ namespace storm { return this->getSubformula().hasQuantitativeResult(); } - Coalition const& GameFormula::getCoalition() const { + PlayerCoalition const& GameFormula::getCoalition() const { return coalition; } diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h index d34267ebe..bc57583eb 100644 --- a/src/storm/logic/GameFormula.h +++ b/src/storm/logic/GameFormula.h @@ -2,20 +2,20 @@ #define STORM_LOGIC_GAMEFORMULA_H_ #include "storm/logic/UnaryStateFormula.h" -#include "storm/logic/Coalition.h" +#include "storm/logic/PlayerCoalition.h" #include namespace storm { namespace logic { class GameFormula : public UnaryStateFormula { public: - GameFormula(Coalition const& coalition, std::shared_ptr subFormula); + GameFormula(PlayerCoalition const& coalition, std::shared_ptr subFormula); virtual ~GameFormula() { // Intentionally left empty. } - Coalition const& getCoalition() const; + PlayerCoalition const& getCoalition() const; virtual bool isGameFormula() const override; virtual bool hasQualitativeResult() const override; virtual bool hasQuantitativeResult() const override; @@ -25,7 +25,7 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; private: - Coalition coalition; + PlayerCoalition coalition; }; } } diff --git a/src/storm/logic/Coalition.cpp b/src/storm/logic/PlayerCoalition.cpp similarity index 55% rename from src/storm/logic/Coalition.cpp rename to src/storm/logic/PlayerCoalition.cpp index b11093874..0c93092bf 100644 --- a/src/storm/logic/Coalition.cpp +++ b/src/storm/logic/PlayerCoalition.cpp @@ -1,13 +1,13 @@ -#include "storm/logic/Coalition.h" +#include "storm/logic/PlayerCoalition.h" namespace storm { namespace logic { - Coalition::Coalition(std::vector> playerIds) : _playerIds(playerIds) { + PlayerCoalition::PlayerCoalition(std::vector> playerIds) : _playerIds(playerIds) { // Intentionally left empty. } - std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) { + std::ostream& operator<<(std::ostream& stream, PlayerCoalition const& coalition) { bool firstItem = true; for (auto const& id : coalition._playerIds) { if (firstItem) { firstItem = false; } else { stream << ","; } diff --git a/src/storm/logic/Coalition.h b/src/storm/logic/PlayerCoalition.h similarity index 55% rename from src/storm/logic/Coalition.h rename to src/storm/logic/PlayerCoalition.h index 0044dd524..53d82574d 100644 --- a/src/storm/logic/Coalition.h +++ b/src/storm/logic/PlayerCoalition.h @@ -9,13 +9,13 @@ namespace storm { namespace logic { - class Coalition { + class PlayerCoalition { public: - Coalition() = default; - Coalition(std::vector> playerIds); - Coalition(Coalition const& other) = default; + PlayerCoalition() = default; + PlayerCoalition(std::vector> playerIds); + PlayerCoalition(PlayerCoalition const& other) = default; - friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition); + friend std::ostream& operator<<(std::ostream& stream, PlayerCoalition const& playerCoalition); private: std::vector> _playerIds;