Browse Source

added player related helpers

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
6b715792aa
  1. 21
      src/storm/generator/Choice.cpp
  2. 66
      src/storm/generator/Choice.h
  3. 6
      src/storm/storage/prism/Player.cpp
  4. 10
      src/storm/storage/prism/Player.h
  5. 11
      src/storm/storage/prism/Program.cpp
  6. 35
      src/storm/storage/prism/Program.h

21
src/storm/generator/Choice.cpp

@ -81,17 +81,32 @@ namespace storm {
labels = newLabels; labels = newLabels;
} }
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
bool Choice<ValueType, StateType>::hasLabels() const { bool Choice<ValueType, StateType>::hasLabels() const {
return labels.is_initialized(); return labels.is_initialized();
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
std::set<std::string> const& Choice<ValueType, StateType>::getLabels() const { std::set<std::string> const& Choice<ValueType, StateType>::getLabels() const {
return labels.get(); return labels.get();
} }
template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::setPlayerIndex(uint_fast32_t playerIndex) {
this->playerIndex = playerIndex;
}
template<typename ValueType, typename StateType>
bool Choice<ValueType, StateType>::hasPlayerIndex() const {
return playerIndex.is_initialized();
}
template<typename ValueType, typename StateType>
uint_fast32_t const& Choice<ValueType, StateType>::getPlayerIndex() const {
return playerIndex.get();
}
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::addOriginData(boost::any const& data) { void Choice<ValueType, StateType>::addOriginData(boost::any const& data) {
if (!this->originData || this->originData->empty()) { if (!this->originData || this->originData->empty()) {

66
src/storm/generator/Choice.h

@ -64,118 +64,140 @@ namespace storm {
*/ */
template<typename ValueTypePrime, typename StateTypePrime> template<typename ValueTypePrime, typename StateTypePrime>
friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice); friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice);
/*! /*!
* Adds the given label to the labels associated with this choice. * Adds the given label to the labels associated with this choice.
* *
* @param label The label to associate with this choice. * @param label The label to associate with this choice.
*/ */
void addLabel(std::string const& label); void addLabel(std::string const& label);
/*! /*!
* Adds the given label set to the labels associated with this choice. * Adds the given label set to the labels associated with this choice.
* *
* @param labelSet The label set to associate with this choice. * @param labelSet The label set to associate with this choice.
*/ */
void addLabels(std::set<std::string> const& labels); void addLabels(std::set<std::string> const& labels);
/*! /*!
* Returns whether there are labels defined for this choice * Returns whether there are labels defined for this choice
*/ */
bool hasLabels() const; bool hasLabels() const;
/*! /*!
* Retrieves the set of labels associated with this choice. * Retrieves the set of labels associated with this choice.
* *
* @return The set of labels associated with this choice. * @return The set of labels associated with this choice.
*/ */
std::set<std::string> const& getLabels() const; std::set<std::string> 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 * Adds the given data that specifies the origin of this choice w.r.t. the model specification
*/ */
void addOriginData(boost::any const& data); void addOriginData(boost::any const& data);
/*! /*!
* Returns whether there is origin data defined for this choice * Returns whether there is origin data defined for this choice
*/ */
bool hasOriginData() const; bool hasOriginData() const;
/*! /*!
* Returns the origin data associated with this choice. * Returns the origin data associated with this choice.
*/ */
boost::any const& getOriginData() const; boost::any const& getOriginData() const;
/*! /*!
* Retrieves the index of the action of this choice. * Retrieves the index of the action of this choice.
* *
* @return The index of the action of this choice. * @return The index of the action of this choice.
*/ */
uint_fast64_t getActionIndex() const; uint_fast64_t getActionIndex() const;
/*! /*!
* Retrieves the total mass of this choice. * Retrieves the total mass of this choice.
* *
* @return The total mass. * @return The total mass.
*/ */
ValueType getTotalMass() const; ValueType getTotalMass() const;
/*! /*!
* Adds the given probability value to the given state in the underlying distribution. * Adds the given probability value to the given state in the underlying distribution.
*/ */
void addProbability(StateType const& state, ValueType const& value); void addProbability(StateType const& state, ValueType const& value);
/*! /*!
* Adds the given value to the reward associated with this choice. * Adds the given value to the reward associated with this choice.
*/ */
void addReward(ValueType const& value); void addReward(ValueType const& value);
/*! /*!
* Adds the given choices rewards to this choice. * Adds the given choices rewards to this choice.
*/ */
void addRewards(std::vector<ValueType>&& values); void addRewards(std::vector<ValueType>&& values);
/*! /*!
* Retrieves the rewards for this choice under selected reward models. * Retrieves the rewards for this choice under selected reward models.
*/ */
std::vector<ValueType> const& getRewards() const; std::vector<ValueType> const& getRewards() const;
/*! /*!
* Retrieves whether the choice is Markovian. * Retrieves whether the choice is Markovian.
*/ */
bool isMarkovian() const; bool isMarkovian() const;
/*! /*!
* Retrieves the size of the distribution associated with this choice. * Retrieves the size of the distribution associated with this choice.
*/ */
std::size_t size() const; std::size_t size() const;
/*! /*!
* If the size is already known, reserves space in the underlying distribution. * If the size is already known, reserves space in the underlying distribution.
*/ */
void reserve(std::size_t const& size); void reserve(std::size_t const& size);
private: private:
// A flag indicating whether this choice is Markovian or not. // A flag indicating whether this choice is Markovian or not.
bool markovian; bool markovian;
// The action index associated with this choice. // The action index associated with this choice.
uint_fast64_t actionIndex; uint_fast64_t actionIndex;
// The distribution that is associated with the choice. // The distribution that is associated with the choice.
storm::storage::Distribution<ValueType, StateType> distribution; storm::storage::Distribution<ValueType, StateType> distribution;
// The total probability mass (or rates) of this choice. // The total probability mass (or rates) of this choice.
ValueType totalMass; ValueType totalMass;
// The reward values associated with this choice. // The reward values associated with this choice.
std::vector<ValueType> rewards; std::vector<ValueType> rewards;
// The data that stores what part of the model specification induced this choice // The data that stores what part of the model specification induced this choice
boost::optional<boost::any> originData; boost::optional<boost::any> originData;
// The labels of this choice // The labels of this choice
boost::optional<std::set<std::string>> labels; boost::optional<std::set<std::string>> labels;
// The playerIndex of this choice
boost::optional<uint_fast32_t> playerIndex = boost::none;
}; };
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>

6
src/storm/storage/prism/Player.cpp

@ -2,7 +2,7 @@
namespace storm { namespace storm {
namespace prism { namespace prism {
Player::Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> 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<std::string, uint_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledCommands(controlledCommands) {
// Nothing to do here. // Nothing to do here.
} }
@ -10,11 +10,11 @@ namespace storm {
return this->playerName; return this->playerName;
} }
std::map<std::string, uint_fast64_t> const& Player::getModules() const {
std::map<std::string, uint_fast32_t> const& Player::getModules() const {
return this->controlledModules; return this->controlledModules;
} }
std::map<std::string, uint_fast64_t> const& Player::getCommands() const {
std::map<std::string, uint_fast32_t> const& Player::getCommands() const {
return this->controlledCommands; return this->controlledCommands;
} }

10
src/storm/storage/prism/Player.h

@ -24,7 +24,7 @@ namespace storm {
* @param filename The filename in which the player is defined. * @param filename The filename in which the player is defined.
* @param lineNumber The line number in which the player is defined. * @param lineNumber The line number in which the player is defined.
*/ */
Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> const& controlledCommands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Player(std::string const& playerName, std::map<std::string, uint_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename = "", uint_fast32_t lineNumber = 0);
// Create default implementations of constructors/assignment. // Create default implementations of constructors/assignment.
Player() = default; Player() = default;
@ -45,14 +45,14 @@ namespace storm {
* *
* @return The modules controlled by the player. * @return The modules controlled by the player.
*/ */
std::map<std::string, uint_fast64_t> const& getModules() const; // TODO
std::map<std::string, uint_fast32_t> const& getModules() const; // TODO
/*! /*!
* Retrieves all controlled Commands of the player. * Retrieves all controlled Commands of the player.
* *
* @return The commands controlled by the player. * @return The commands controlled by the player.
*/ */
std::map<std::string, uint_fast64_t> const& getCommands() const;
std::map<std::string, uint_fast32_t> const& getCommands() const;
friend std::ostream& operator<<(std::ostream& stream, Player const& player); friend std::ostream& operator<<(std::ostream& stream, Player const& player);
private: private:
@ -60,10 +60,10 @@ namespace storm {
std::string playerName; std::string playerName;
// The modules associated with this player. // The modules associated with this player.
std::map<std::string, uint_fast64_t> controlledModules;
std::map<std::string, uint_fast32_t> controlledModules;
// The commands associated with this player. // The commands associated with this player.
std::map<std::string, uint_fast64_t> controlledCommands;
std::map<std::string, uint_fast32_t> controlledCommands;
}; };
} // namespace prism } // namespace prism

11
src/storm/storage/prism/Program.cpp

@ -491,6 +491,10 @@ namespace storm {
return this->getModules().size(); 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 { storm::prism::Module const& Program::getModule(uint_fast64_t index) const {
return this->modules[index]; return this->modules[index];
} }
@ -509,6 +513,10 @@ namespace storm {
return this->modules; return this->modules;
} }
uint_fast32_t const& Program::getIndexOfPlayer(std::string playerName) const {
return this->playerToIndexMap.at(playerName);
}
std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const { std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
return actionToIndexMap; return actionToIndexMap;
} }
@ -805,6 +813,9 @@ namespace storm {
for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = 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) { for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex; this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
} }

35
src/storm/storage/prism/Program.h

@ -275,13 +275,6 @@ namespace storm {
*/ */
std::vector<Formula> const& getFormulas() const; std::vector<Formula> const& getFormulas() const;
/*!
* Retrieves the players of the program.
*
* @return The players of the program.
*/
std::vector<Player> const& getPlayers() const;
/*! /*!
* Retrieves the number of formulas in the program. * Retrieves the number of formulas in the program.
* *
@ -326,6 +319,27 @@ namespace storm {
*/ */
std::vector<Module> const& getModules() const; std::vector<Module> const& getModules() const;
/*!
* Retrieves the players of the program.
*
* @return The players of the program.
*/
std::vector<Player> 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. * Retrieves the mapping of action names to their indices.
* *
@ -746,11 +760,14 @@ namespace storm {
// The modules associated with the program. // The modules associated with the program.
std::vector<Module> modules; std::vector<Module> modules;
// A mapping of module names to their indices.
std::map<std::string, uint_fast64_t> moduleToIndexMap;
// The players associated with the program. // The players associated with the program.
std::vector<Player> players; std::vector<Player> players;
// A mapping of module names to their indices.
std::map<std::string, uint_fast64_t> moduleToIndexMap;
// A mapping of player names to their indices.
std::map<std::string, uint_fast64_t> playerToIndexMap;
// The reward models associated with the program. // The reward models associated with the program.
std::vector<RewardModel> rewardModels; std::vector<RewardModel> rewardModels;

Loading…
Cancel
Save