Browse Source

store tuples of player name and index

Store this instead of only the index. Needed for easier parsing of the
rpatl formulas (prism allows player indices and names!)
main
Stefan Pranger 5 years ago
parent
commit
c11c49d22b
  1. 10
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 2
      src/storm/builder/ExplicitModelBuilder.h
  3. 12
      src/storm/generator/Choice.cpp
  4. 10
      src/storm/generator/Choice.h
  5. 14
      src/storm/generator/PrismNextStateGenerator.cpp
  6. 6
      src/storm/logic/Coalition.cpp
  7. 6
      src/storm/logic/Coalition.h
  8. 2
      src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
  9. 4
      src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
  10. 2
      src/storm/models/sparse/Smg.cpp
  11. 4
      src/storm/models/sparse/Smg.h
  12. 6
      src/storm/storage/sparse/ModelComponents.h

10
src/storm/builder/ExplicitModelBuilder.cpp

@ -120,7 +120,7 @@ namespace storm {
} }
template <typename ValueType, typename RewardModelType, typename StateType> template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<std::vector<uint_fast32_t>>& playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) { void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<std::vector<std::pair<std::string, uint_fast64_t>>>& playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
// Create markovian states bit vector, if required. // Create markovian states bit vector, if required.
if (generator->getModelType() == storm::generator::ModelType::MA) { if (generator->getModelType() == storm::generator::ModelType::MA) {
@ -130,7 +130,7 @@ namespace storm {
// Create the player indices vector, if required. // Create the player indices vector, if required.
if (generator->getModelType() == storm::generator::ModelType::SMG) { if (generator->getModelType() == storm::generator::ModelType::SMG) {
playerActionIndices = std::vector<uint_fast32_t>{}; playerActionIndices = std::vector<std::pair<std::string, uint_fast64_t>>{};
playerActionIndices.get().reserve(1000); playerActionIndices.get().reserve(1000);
} }
@ -211,7 +211,7 @@ namespace storm {
if (playerActionIndices) { if (playerActionIndices) {
// TODO change this to storm::utility::infinity<ValueType>() ? // TODO change this to storm::utility::infinity<ValueType>() ?
playerActionIndices.get().push_back(-1); playerActionIndices.get().emplace_back("", -1);
} }
++currentRow; ++currentRow;
@ -270,7 +270,7 @@ namespace storm {
} }
if (playerActionIndices) { if (playerActionIndices) {
playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex()); playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayer());
} }
++currentRowGroup; ++currentRowGroup;
} }
@ -350,7 +350,7 @@ namespace storm {
} }
ChoiceInformationBuilder choiceInformationBuilder; ChoiceInformationBuilder choiceInformationBuilder;
boost::optional<storm::storage::BitVector> markovianStates; boost::optional<storm::storage::BitVector> markovianStates;
boost::optional<std::vector<uint_fast32_t>> playerActionIndices; boost::optional<std::vector<std::pair<std::string, uint_fast64_t>>> playerActionIndices;
// If we need to build state valuations, initialize them now. // If we need to build state valuations, initialize them now.
boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder; boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;

2
src/storm/builder/ExplicitModelBuilder.h

@ -131,7 +131,7 @@ namespace storm {
* @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information). * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
* @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
*/ */
void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<std::vector<uint_fast32_t>>& playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder); void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<std::vector<std::pair<std::string, uint_fast64_t>>>& playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
/*! /*!
* Explores the state space of the given program and returns the components of the model as a result. * Explores the state space of the given program and returns the components of the model as a result.

12
src/storm/generator/Choice.cpp

@ -93,18 +93,18 @@ namespace storm {
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::setPlayerIndex(uint_fast32_t playerIndex) { void Choice<ValueType, StateType>::setPlayer(std::pair<std::string, uint_fast64_t> player) {
this->playerIndex = playerIndex; this->player = player;
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
bool Choice<ValueType, StateType>::hasPlayerIndex() const { bool Choice<ValueType, StateType>::hasPlayer() const {
return playerIndex.is_initialized(); return player.is_initialized();
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
uint_fast32_t const& Choice<ValueType, StateType>::getPlayerIndex() const { std::pair<std::string, uint_fast64_t> const& Choice<ValueType, StateType>::getPlayer() const {
return playerIndex.get(); return player.get();
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>

10
src/storm/generator/Choice.h

@ -96,19 +96,19 @@ namespace storm {
* *
* @param The player index associated with this choice. * @param The player index associated with this choice.
*/ */
void setPlayerIndex(uint_fast32_t playerIndex); void setPlayer(std::pair<std::string, uint_fast64_t> player);
/*! /*!
* Returns whether there is an index for the player defined for this choice. * Returns whether there is an index for the player defined for this choice.
*/ */
bool hasPlayerIndex() const; bool hasPlayer() const;
/*! /*!
* Retrieves the players index associated with this choice * Retrieves the players index associated with this choice
* *
* @return The player index associated with this choice. * @return The player index associated with this choice.
*/ */
uint_fast32_t const& getPlayerIndex() const; std::pair<std::string, uint_fast64_t> const& getPlayer() 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
@ -196,8 +196,8 @@ namespace storm {
// 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 // The player of this choice
boost::optional<uint_fast32_t> playerIndex = boost::none; boost::optional<std::pair<std::string, uint_fast64_t>> player = boost::none;
}; };
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>

14
src/storm/generator/PrismNextStateGenerator.cpp

@ -83,7 +83,7 @@ namespace storm {
if (program.getModelType() == storm::prism::Program::ModelType::SMG) { if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
for (auto const& player : program.getPlayers()) { for (auto const& player : program.getPlayers()) {
uint_fast32_t playerIndex = program.getIndexOfPlayer(player.getName()); uint_fast64_t playerIndex = program.getIndexOfPlayer(player.getName());
for (auto const& moduleIndexPair : player.getModules()) { for (auto const& moduleIndexPair : player.getModules()) {
moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex; moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex;
} }
@ -382,12 +382,12 @@ namespace storm {
} }
if (program.getModelType() == storm::prism::Program::ModelType::SMG) { if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
uint_fast32_t statePlayerIndex = allChoices.at(0).getPlayerIndex(); uint_fast64_t statePlayerIndex = allChoices.at(0).getPlayer().second;
for(auto& choice : allChoices) { for(auto& choice : allChoices) {
if (allChoices.size() == 1) break; if (allChoices.size() == 1) break;
// getPlayerIndex().is_initialized()? // getPlayerIndex().is_initialized()?
if (choice.hasPlayerIndex()) { if (choice.hasPlayer()) {
STORM_LOG_ASSERT(choice.getPlayerIndex() == statePlayerIndex, "State '" << this->stateToString(*this->state) << "' comprises choices for different players."); STORM_LOG_ASSERT(choice.getPlayer().second == statePlayerIndex, "State '" << this->stateToString(*this->state) << "' comprises choices for different players.");
} else { } else {
STORM_LOG_WARN("State '" << this->stateToString(*this->state) << "' features a choice without player index."); STORM_LOG_WARN("State '" << this->stateToString(*this->state) << "' features a choice without player index.");
} }
@ -612,7 +612,8 @@ namespace storm {
if (program.getModelType() == storm::prism::Program::ModelType::SMG) { if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
// Can we trust the model ordering here? // Can we trust the model ordering here?
// I.e. is i the correct moduleIndex set in Program.cpp:805? TODO // I.e. is i the correct moduleIndex set in Program.cpp:805? TODO
choice.setPlayerIndex(moduleIndexToPlayerIndexMap[i]); uint_fast64_t playerIndex = moduleIndexToPlayerIndexMap[i];
choice.setPlayer(std::make_pair(program.getPlayers()[playerIndex].getName(), playerIndex));
} }
if (this->options.isExplorationChecksSet()) { if (this->options.isExplorationChecksSet()) {
@ -678,7 +679,8 @@ namespace storm {
Choice<ValueType>& choice = choices.back(); Choice<ValueType>& choice = choices.back();
if (program.getModelType() == storm::prism::Program::ModelType::SMG) { if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
choice.setPlayerIndex(commandIndexToPlayerIndexMap[actionIndex]); uint_fast64_t playerIndex = commandIndexToPlayerIndexMap[actionIndex];
choice.setPlayer(std::make_pair(program.getPlayers()[playerIndex].getName(), playerIndex));
} }
// Remember the choice label and origins only if we were asked to. // Remember the choice label and origins only if we were asked to.

6
src/storm/logic/Coalition.cpp

@ -3,10 +3,14 @@
namespace storm { namespace storm {
namespace logic { namespace logic {
Coalition::Coalition(std::vector<boost::variant<std::string, uint64_t>> playerIds) : playerIds(playerIds) { Coalition::Coalition(std::vector<boost::variant<std::string, uint_fast64_t>> playerIds) : playerIds(playerIds) {
// Intentionally left empty. // Intentionally left empty.
} }
std::vector<boost::variant<std::string, uint_fast64_t>> Coalition::getPlayerIds() const {
return playerIds;
}
std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) { std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) {
bool firstItem = true; bool firstItem = true;
stream << "<<"; stream << "<<";

6
src/storm/logic/Coalition.h

@ -15,13 +15,15 @@ namespace storm {
class Coalition { class Coalition {
public: public:
Coalition() = default; Coalition() = default;
Coalition(std::vector<boost::variant<std::string, uint64_t>>); Coalition(std::vector<boost::variant<std::string, uint_fast64_t>>);
Coalition(Coalition const& other) = default; Coalition(Coalition const& other) = default;
std::vector<boost::variant<std::string, uint_fast64_t>> getPlayerIds() const;
friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition); friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition);
private: private:
std::vector<boost::variant<std::string, uint64_t>> playerIds; std::vector<boost::variant<std::string, uint_fast64_t>> playerIds;
}; };
} }
} }

2
src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp

@ -22,7 +22,7 @@ namespace storm {
namespace helper { namespace helper {
template <typename ValueType> template <typename ValueType>
SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& coalitionIndices) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), coalitionIndices(coalitionIndices) { SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), player(player) {
// Intentionally left empty. // Intentionally left empty.
} }

4
src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h

@ -27,7 +27,7 @@ namespace storm {
/*! /*!
* Initializes the helper for a discrete time model with different players (i.e. SMG) * Initializes the helper for a discrete time model with different players (i.e. SMG)
*/ */
SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& coalitionIndices); SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player);
/*! /*!
* TODO * TODO
@ -57,7 +57,7 @@ namespace storm {
std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues); std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues);
private: private:
std::vector<uint64_t> coalitionIndices; std::vector<std::pair<std::string, uint_fast64_t>> player;
}; };

2
src/storm/models/sparse/Smg.cpp

@ -39,7 +39,7 @@ namespace storm {
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
std::vector<uint_fast32_t> Smg<ValueType, RewardModelType>::getPlayerActionIndices() const { std::vector<std::pair<std::string, uint_fast64_t>> Smg<ValueType, RewardModelType>::getPlayerActionIndices() const {
return playerActionIndices; return playerActionIndices;
} }

4
src/storm/models/sparse/Smg.h

@ -49,10 +49,10 @@ namespace storm {
Smg(Smg<ValueType, RewardModelType>&& other) = default; Smg(Smg<ValueType, RewardModelType>&& other) = default;
Smg& operator=(Smg<ValueType, RewardModelType>&& other) = default; Smg& operator=(Smg<ValueType, RewardModelType>&& other) = default;
std::vector<uint_fast64_t> getPlayerActionIndices() const; std::vector<std::pair<std::string, uint_fast64_t>> getPlayerActionIndices() const;
private: private:
std::vector<uint_fast64_t> playerActionIndices; std::vector<std::pair<std::string, uint_fast64_t>> playerActionIndices;
}; };
} // namespace sparse } // namespace sparse

6
src/storm/storage/sparse/ModelComponents.h

@ -31,7 +31,7 @@ namespace storm {
bool rateTransitions = false, bool rateTransitions = false,
boost::optional<storm::storage::BitVector> const& markovianStates = boost::none, boost::optional<storm::storage::BitVector> const& markovianStates = boost::none,
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none, boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none,
boost::optional<std::vector<uint_fast32_t>> const& playerActionIndices = boost::none) boost::optional<std::vector<std::pair<std::string, uint_fast32_t>>> const& playerActionIndices = boost::none)
: transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) { : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) {
// Intentionally left empty // Intentionally left empty
} }
@ -42,7 +42,7 @@ namespace storm {
bool rateTransitions = false, bool rateTransitions = false,
boost::optional<storm::storage::BitVector>&& markovianStates = boost::none, boost::optional<storm::storage::BitVector>&& markovianStates = boost::none,
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none, boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none,
boost::optional<std::vector<uint_fast32_t>>&& playerActionIndices = boost::none) boost::optional<std::vector<std::pair<std::string, uint_fast32_t>>>&& playerActionIndices = boost::none)
: transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)), playerActionIndices(std::move(playerActionIndices)) { : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)), playerActionIndices(std::move(playerActionIndices)) {
// Intentionally left empty // Intentionally left empty
} }
@ -85,7 +85,7 @@ namespace storm {
// Stochastic multiplayer game specific components: // Stochastic multiplayer game specific components:
// The vector mapping state choices to players // The vector mapping state choices to players
boost::optional<std::vector<uint_fast32_t>> playerActionIndices; boost::optional<std::vector<std::pair<std::string, uint_fast32_t>>> playerActionIndices;
}; };
} }
} }

|||||||
100:0
Loading…
Cancel
Save