From 6b715792aa36f9afd6de38d8de80b85b10baa2cc Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 19 Aug 2020 11:54:46 +0200 Subject: [PATCH] added player related helpers --- src/storm/generator/Choice.cpp | 21 +++++++-- src/storm/generator/Choice.h | 66 +++++++++++++++++++---------- src/storm/storage/prism/Player.cpp | 6 +-- src/storm/storage/prism/Player.h | 10 ++--- src/storm/storage/prism/Program.cpp | 11 +++++ src/storm/storage/prism/Program.h | 35 +++++++++++---- 6 files changed, 107 insertions(+), 42 deletions(-) diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 5d69c98ab..517dffd6c 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -81,17 +81,32 @@ namespace storm { labels = newLabels; } } - + template bool Choice::hasLabels() const { return labels.is_initialized(); } - + template std::set const& Choice::getLabels() const { return labels.get(); } - + + template + void Choice::setPlayerIndex(uint_fast32_t playerIndex) { + this->playerIndex = playerIndex; + } + + template + bool Choice::hasPlayerIndex() const { + return playerIndex.is_initialized(); + } + + template + uint_fast32_t const& Choice::getPlayerIndex() const { + return playerIndex.get(); + } + template void Choice::addOriginData(boost::any const& data) { if (!this->originData || this->originData->empty()) { diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 1dbc41760..80f8f7031 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -64,118 +64,140 @@ namespace storm { */ template friend std::ostream& operator<<(std::ostream& out, Choice const& choice); - + /*! * Adds the given label to the labels associated with this choice. * * @param label The label to associate with this choice. */ void addLabel(std::string const& label); - + /*! * Adds the given label set to the labels associated with this choice. * * @param labelSet The label set to associate with this choice. */ void addLabels(std::set const& labels); - + /*! * Returns whether there are labels defined for this choice */ bool hasLabels() const; - + /*! * Retrieves the set of labels associated with this choice. * * @return The set of labels associated with this choice. */ std::set const& getLabels() const; - + + /*! + * Sets the players index + * + * @param The player index associated with this choice. + */ + void setPlayerIndex(uint_fast32_t playerIndex); + + /*! + * Returns whether there is an index for the player defined for this choice. + */ + bool hasPlayerIndex() const; + + /*! + * Retrieves the players index associated with this choice + * + * @return The player index associated with this choice. + */ + uint_fast32_t const& getPlayerIndex() const; + /*! * Adds the given data that specifies the origin of this choice w.r.t. the model specification */ void addOriginData(boost::any const& data); - + /*! * Returns whether there is origin data defined for this choice */ bool hasOriginData() const; - + /*! * Returns the origin data associated with this choice. */ boost::any const& getOriginData() const; - + /*! * Retrieves the index of the action of this choice. * * @return The index of the action of this choice. */ uint_fast64_t getActionIndex() const; - + /*! * Retrieves the total mass of this choice. * * @return The total mass. */ ValueType getTotalMass() const; - + /*! * Adds the given probability value to the given state in the underlying distribution. */ void addProbability(StateType const& state, ValueType const& value); - + /*! * Adds the given value to the reward associated with this choice. */ void addReward(ValueType const& value); - + /*! * Adds the given choices rewards to this choice. */ void addRewards(std::vector&& values); - + /*! * Retrieves the rewards for this choice under selected reward models. */ std::vector const& getRewards() const; - + /*! * Retrieves whether the choice is Markovian. */ bool isMarkovian() const; - + /*! * Retrieves the size of the distribution associated with this choice. */ std::size_t size() const; - + /*! * If the size is already known, reserves space in the underlying distribution. */ void reserve(std::size_t const& size); - + private: // A flag indicating whether this choice is Markovian or not. bool markovian; // The action index associated with this choice. uint_fast64_t actionIndex; - + // The distribution that is associated with the choice. storm::storage::Distribution distribution; - + // The total probability mass (or rates) of this choice. ValueType totalMass; - + // The reward values associated with this choice. std::vector rewards; - + // The data that stores what part of the model specification induced this choice boost::optional originData; - + // The labels of this choice boost::optional> labels; + + // The playerIndex of this choice + boost::optional playerIndex = boost::none; }; template diff --git a/src/storm/storage/prism/Player.cpp b/src/storm/storage/prism/Player.cpp index 4cc05a719..f2e30d3ad 100644 --- a/src/storm/storage/prism/Player.cpp +++ b/src/storm/storage/prism/Player.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - Player::Player(std::string const& playerName, std::map const& controlledModules, std::map const& controlledCommands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledCommands(controlledCommands) { + Player::Player(std::string const& playerName, std::map const& controlledModules, std::map const& controlledCommands, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledCommands(controlledCommands) { // Nothing to do here. } @@ -10,11 +10,11 @@ namespace storm { return this->playerName; } - std::map const& Player::getModules() const { + std::map const& Player::getModules() const { return this->controlledModules; } - std::map const& Player::getCommands() const { + std::map const& Player::getCommands() const { return this->controlledCommands; } diff --git a/src/storm/storage/prism/Player.h b/src/storm/storage/prism/Player.h index 1098cd75f..7d9437f7f 100644 --- a/src/storm/storage/prism/Player.h +++ b/src/storm/storage/prism/Player.h @@ -24,7 +24,7 @@ namespace storm { * @param filename The filename in which the player is defined. * @param lineNumber The line number in which the player is defined. */ - Player(std::string const& playerName, std::map const& controlledModules, std::map const& controlledCommands, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Player(std::string const& playerName, std::map const& controlledModules, std::map const& controlledCommands, std::string const& filename = "", uint_fast32_t lineNumber = 0); // Create default implementations of constructors/assignment. Player() = default; @@ -45,14 +45,14 @@ namespace storm { * * @return The modules controlled by the player. */ - std::map const& getModules() const; // TODO + std::map const& getModules() const; // TODO /*! * Retrieves all controlled Commands of the player. * * @return The commands controlled by the player. */ - std::map const& getCommands() const; + std::map const& getCommands() const; friend std::ostream& operator<<(std::ostream& stream, Player const& player); private: @@ -60,10 +60,10 @@ namespace storm { std::string playerName; // The modules associated with this player. - std::map controlledModules; + std::map controlledModules; // The commands associated with this player. - std::map controlledCommands; + std::map controlledCommands; }; } // namespace prism diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 4b0840bb1..3acef442e 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -491,6 +491,10 @@ namespace storm { return this->getModules().size(); } + std::size_t Program::getNumberOfPlayers() const { + return this->getPlayers().size(); + } + storm::prism::Module const& Program::getModule(uint_fast64_t index) const { return this->modules[index]; } @@ -509,6 +513,10 @@ namespace storm { return this->modules; } + uint_fast32_t const& Program::getIndexOfPlayer(std::string playerName) const { + return this->playerToIndexMap.at(playerName); + } + std::map const& Program::getActionNameToIndexMapping() const { return actionToIndexMap; } @@ -805,6 +813,9 @@ namespace storm { for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex; } + for (uint_fast64_t playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) { + this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex; + } for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) { this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex; } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index d35705fe6..095f164ff 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -275,13 +275,6 @@ namespace storm { */ std::vector const& getFormulas() const; - /*! - * Retrieves the players of the program. - * - * @return The players of the program. - */ - std::vector const& getPlayers() const; - /*! * Retrieves the number of formulas in the program. * @@ -326,6 +319,27 @@ namespace storm { */ std::vector const& getModules() const; + /*! + * Retrieves the players of the program. + * + * @return The players of the program. + */ + std::vector const& getPlayers() const; + + /*! + * Retrieves the number of players in the program. + * + * @return The number of players in the program. + */ + std::size_t getNumberOfPlayers() const; + + /*! + * Retrieves the index of the player in the program. + * + * @return The index of the player in the program. + */ + uint_fast32_t const& getIndexOfPlayer(std::string playerName) const; + /*! * Retrieves the mapping of action names to their indices. * @@ -746,11 +760,14 @@ namespace storm { // The modules associated with the program. std::vector modules; + // A mapping of module names to their indices. + std::map moduleToIndexMap; + // The players associated with the program. std::vector players; - // A mapping of module names to their indices. - std::map moduleToIndexMap; + // A mapping of player names to their indices. + std::map playerToIndexMap; // The reward models associated with the program. std::vector rewardModels;