From c11c49d22bec8fd878949ccb15eaac3e4665e006 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 22 Dec 2020 15:58:30 +0100 Subject: [PATCH] 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!) --- src/storm/builder/ExplicitModelBuilder.cpp | 10 +++++----- src/storm/builder/ExplicitModelBuilder.h | 2 +- src/storm/generator/Choice.cpp | 12 ++++++------ src/storm/generator/Choice.h | 10 +++++----- src/storm/generator/PrismNextStateGenerator.cpp | 14 ++++++++------ src/storm/logic/Coalition.cpp | 6 +++++- src/storm/logic/Coalition.h | 6 ++++-- ...seNondeterministicGameInfiniteHorizonHelper.cpp | 2 +- ...arseNondeterministicGameInfiniteHorizonHelper.h | 4 ++-- src/storm/models/sparse/Smg.cpp | 2 +- src/storm/models/sparse/Smg.h | 4 ++-- src/storm/storage/sparse/ModelComponents.h | 6 +++--- 12 files changed, 43 insertions(+), 35 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 754568b38..3e224a419 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -120,7 +120,7 @@ namespace storm { } template - void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional>& playerActionIndices, boost::optional& stateValuationsBuilder) { + void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional>>& playerActionIndices, boost::optional& stateValuationsBuilder) { // Create markovian states bit vector, if required. if (generator->getModelType() == storm::generator::ModelType::MA) { @@ -130,7 +130,7 @@ namespace storm { // Create the player indices vector, if required. if (generator->getModelType() == storm::generator::ModelType::SMG) { - playerActionIndices = std::vector{}; + playerActionIndices = std::vector>{}; playerActionIndices.get().reserve(1000); } @@ -211,7 +211,7 @@ namespace storm { if (playerActionIndices) { // TODO change this to storm::utility::infinity() ? - playerActionIndices.get().push_back(-1); + playerActionIndices.get().emplace_back("", -1); } ++currentRow; @@ -270,7 +270,7 @@ namespace storm { } if (playerActionIndices) { - playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex()); + playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayer()); } ++currentRowGroup; } @@ -350,7 +350,7 @@ namespace storm { } ChoiceInformationBuilder choiceInformationBuilder; boost::optional markovianStates; - boost::optional> playerActionIndices; + boost::optional>> playerActionIndices; // If we need to build state valuations, initialize them now. boost::optional stateValuationsBuilder; diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index ed470ca9d..7b1fee8a8 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/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 stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states */ - void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional>& playerActionIndices, boost::optional& stateValuationsBuilder); + void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional>>& playerActionIndices, boost::optional& stateValuationsBuilder); /*! * Explores the state space of the given program and returns the components of the model as a result. diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 517dffd6c..9abde728b 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -93,18 +93,18 @@ namespace storm { } template - void Choice::setPlayerIndex(uint_fast32_t playerIndex) { - this->playerIndex = playerIndex; + void Choice::setPlayer(std::pair player) { + this->player = player; } template - bool Choice::hasPlayerIndex() const { - return playerIndex.is_initialized(); + bool Choice::hasPlayer() const { + return player.is_initialized(); } template - uint_fast32_t const& Choice::getPlayerIndex() const { - return playerIndex.get(); + std::pair const& Choice::getPlayer() const { + return player.get(); } template diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 80f8f7031..65945b8d1 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -96,19 +96,19 @@ namespace storm { * * @param The player index associated with this choice. */ - void setPlayerIndex(uint_fast32_t playerIndex); + void setPlayer(std::pair player); /*! * 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 * * @return The player index associated with this choice. */ - uint_fast32_t const& getPlayerIndex() const; + std::pair const& getPlayer() const; /*! * 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 boost::optional> labels; - // The playerIndex of this choice - boost::optional playerIndex = boost::none; + // The player of this choice + boost::optional> player = boost::none; }; template diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 03b4975a6..0d8ed6cd5 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -83,7 +83,7 @@ namespace storm { if (program.getModelType() == storm::prism::Program::ModelType::SMG) { 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()) { moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex; } @@ -382,12 +382,12 @@ namespace storm { } 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) { if (allChoices.size() == 1) break; // getPlayerIndex().is_initialized()? - if (choice.hasPlayerIndex()) { - STORM_LOG_ASSERT(choice.getPlayerIndex() == statePlayerIndex, "State '" << this->stateToString(*this->state) << "' comprises choices for different players."); + if (choice.hasPlayer()) { + STORM_LOG_ASSERT(choice.getPlayer().second == statePlayerIndex, "State '" << this->stateToString(*this->state) << "' comprises choices for different players."); } else { 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) { // Can we trust the model ordering here? // 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()) { @@ -678,7 +679,8 @@ namespace storm { Choice& choice = choices.back(); 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. diff --git a/src/storm/logic/Coalition.cpp b/src/storm/logic/Coalition.cpp index 0781aaece..baa0736c4 100644 --- a/src/storm/logic/Coalition.cpp +++ b/src/storm/logic/Coalition.cpp @@ -3,10 +3,14 @@ namespace storm { namespace logic { - Coalition::Coalition(std::vector> playerIds) : playerIds(playerIds) { + Coalition::Coalition(std::vector> playerIds) : playerIds(playerIds) { // Intentionally left empty. } + std::vector> Coalition::getPlayerIds() const { + return playerIds; + } + std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) { bool firstItem = true; stream << "<<"; diff --git a/src/storm/logic/Coalition.h b/src/storm/logic/Coalition.h index 73ea92ac4..9f3966dd1 100644 --- a/src/storm/logic/Coalition.h +++ b/src/storm/logic/Coalition.h @@ -15,13 +15,15 @@ namespace storm { class Coalition { public: Coalition() = default; - Coalition(std::vector>); + Coalition(std::vector>); Coalition(Coalition const& other) = default; + std::vector> getPlayerIds() const; + friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition); private: - std::vector> playerIds; + std::vector> playerIds; }; } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index baaa3782d..03538c2e9 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -22,7 +22,7 @@ namespace storm { namespace helper { template - SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices) : SparseInfiniteHorizonHelper(transitionMatrix), coalitionIndices(coalitionIndices) { + SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player) : SparseInfiniteHorizonHelper(transitionMatrix), player(player) { // Intentionally left empty. } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h index 550d12a47..fd872b807 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h +++ b/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) */ - SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices); + SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player); /*! * TODO @@ -57,7 +57,7 @@ namespace storm { std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues); private: - std::vector coalitionIndices; + std::vector> player; }; diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index e7c20c9fa..f6b75a447 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -39,7 +39,7 @@ namespace storm { } template - std::vector Smg::getPlayerActionIndices() const { + std::vector> Smg::getPlayerActionIndices() const { return playerActionIndices; } diff --git a/src/storm/models/sparse/Smg.h b/src/storm/models/sparse/Smg.h index 2bf7146c8..30334adda 100644 --- a/src/storm/models/sparse/Smg.h +++ b/src/storm/models/sparse/Smg.h @@ -49,10 +49,10 @@ namespace storm { Smg(Smg&& other) = default; Smg& operator=(Smg&& other) = default; - std::vector getPlayerActionIndices() const; + std::vector> getPlayerActionIndices() const; private: - std::vector playerActionIndices; + std::vector> playerActionIndices; }; } // namespace sparse diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index 29ae3d14b..580732380 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -31,7 +31,7 @@ namespace storm { bool rateTransitions = false, boost::optional const& markovianStates = boost::none, boost::optional> const& player1Matrix = boost::none, - boost::optional> const& playerActionIndices = boost::none) + boost::optional>> const& playerActionIndices = boost::none) : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) { // Intentionally left empty } @@ -42,7 +42,7 @@ namespace storm { bool rateTransitions = false, boost::optional&& markovianStates = boost::none, boost::optional>&& player1Matrix = boost::none, - boost::optional>&& playerActionIndices = boost::none) + boost::optional>>&& 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)) { // Intentionally left empty } @@ -85,7 +85,7 @@ namespace storm { // Stochastic multiplayer game specific components: // The vector mapping state choices to players - boost::optional> playerActionIndices; + boost::optional>> playerActionIndices; }; } }