From 277f802850b9cc017f5f242d01014ceaff592cd5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 12 Jan 2021 13:36:50 +0100 Subject: [PATCH] * PlayerIndex is now declared in a separate file (as this can potentially be independent of PRISM input). * Polished PrismNextStateGenerator, in particular more proper error handling --- src/storm/generator/Choice.cpp | 4 +-- src/storm/generator/Choice.h | 7 +++-- .../generator/PrismNextStateGenerator.cpp | 28 +++++++++++-------- src/storm/generator/PrismNextStateGenerator.h | 7 +++-- src/storm/storage/PlayerIndex.h | 11 ++++++++ src/storm/storage/prism/Player.cpp | 1 + src/storm/storage/prism/Player.h | 10 +------ src/storm/storage/prism/Program.cpp | 20 ++++++------- src/storm/storage/prism/Program.h | 11 ++++---- 9 files changed, 55 insertions(+), 44 deletions(-) create mode 100644 src/storm/storage/PlayerIndex.h diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 517dffd6c..fc1d41999 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -93,7 +93,7 @@ namespace storm { } template - void Choice::setPlayerIndex(uint_fast32_t playerIndex) { + void Choice::setPlayerIndex(storm::storage::PlayerIndex playerIndex) { this->playerIndex = playerIndex; } @@ -103,7 +103,7 @@ namespace storm { } template - uint_fast32_t const& Choice::getPlayerIndex() const { + storm::storage::PlayerIndex const& Choice::getPlayerIndex() const { return playerIndex.get(); } diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 80f8f7031..31842ddee 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -9,6 +9,7 @@ #include #include "storm/storage/Distribution.h" +#include "storm/storage/PlayerIndex.h" namespace storm { namespace generator { @@ -96,7 +97,7 @@ namespace storm { * * @param The player index associated with this choice. */ - void setPlayerIndex(uint_fast32_t playerIndex); + void setPlayerIndex(storm::storage::PlayerIndex playerIndex); /*! * Returns whether there is an index for the player defined for this choice. @@ -108,7 +109,7 @@ namespace storm { * * @return The player index associated with this choice. */ - uint_fast32_t const& getPlayerIndex() const; + storm::storage::PlayerIndex const& getPlayerIndex() const; /*! * Adds the given data that specifies the origin of this choice w.r.t. the model specification @@ -197,7 +198,7 @@ namespace storm { boost::optional> labels; // The playerIndex of this choice - boost::optional playerIndex = boost::none; + boost::optional playerIndex; }; template diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 928f93bd6..ecf7e792d 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -374,16 +374,16 @@ namespace storm { allChoices.push_back(std::move(globalChoice)); } - if (program.getModelType() == storm::prism::Program::ModelType::SMG) { - uint_fast32_t statePlayerIndex = allChoices.at(0).getPlayerIndex(); - 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."); - } else { - STORM_LOG_WARN("State '" << this->stateToString(*this->state) << "' features a choice without player index."); - } + // For SMG we check whether the state has a unique player + if (program.getModelType() == storm::prism::Program::ModelType::SMG && allChoices.size() > 1) { + auto choiceIt = allChoices.begin(); + STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(), "State '" << this->stateToString(*this->state) << "' features a choice without player index."); // This should have been catched while creating the choice already + storm::storage::PlayerIndex statePlayerIndex = choiceIt->getPlayerIndex(); + STORM_LOG_ASSERT(statePlayerIndex != storm::storage::INVALID_PLAYER_INDEX, "State '" << this->stateToString(*this->state) << "' features a choice with invalid player index."); // This should have been catched while creating the choice already + for (++choiceIt; choiceIt != allChoices.end(); ++choiceIt) { + STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(), "State '" << this->stateToString(*this->state) << "' features a choice without player index."); // This should have been catched while creating the choice already + STORM_LOG_ASSERT(choiceIt->getPlayerIndex() != storm::storage::INVALID_PLAYER_INDEX, "State '" << this->stateToString(*this->state) << "' features a choice with invalid player index."); // This should have been catched while creating the choice already + STORM_LOG_THROW(statePlayerIndex == choiceIt->getPlayerIndex(), storm::exceptions::WrongFormatException, "The player for state '" << this->stateToString(*this->state) << "' is not unique. At least one choice is owned by player '" << statePlayerIndex << "' while another is owned by player '" << choiceIt->getPlayerIndex() << "'."); } } @@ -603,7 +603,9 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::SMG) { - choice.setPlayerIndex(moduleIndexToPlayerIndexMap[i]); + storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i); + STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command."); + choice.setPlayerIndex(playerOfModule); } if (this->options.isExplorationChecksSet()) { @@ -669,7 +671,9 @@ namespace storm { Choice& choice = choices.back(); if (program.getModelType() == storm::prism::Program::ModelType::SMG) { - choice.setPlayerIndex(actionIndexToPlayerIndexMap[actionIndex]); + storm::storage::PlayerIndex const& playerOfAction = actionIndexToPlayerIndexMap.at(actionIndex); + STORM_LOG_THROW(playerOfAction != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Action " << program.getActionName(actionIndex) << " is not owned by any player but has at least one enabled, unlabeled (synchronized) command."); + choice.setPlayerIndex(playerOfAction); } // Remember the choice label and origins only if we were asked to. diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 3adb9361b..4e1901134 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -4,6 +4,7 @@ #include "storm/generator/NextStateGenerator.h" #include "storm/storage/prism/Program.h" +#include "storm/storage/PlayerIndex.h" #include "storm/storage/BoostTypes.h" namespace storm { @@ -121,9 +122,9 @@ namespace storm { // A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; - // A mapping from modules/commands to the programs players - std::vector moduleIndexToPlayerIndexMap; - std::map actionIndexToPlayerIndexMap; + // Mappings from module/action indices to the programs players + std::vector moduleIndexToPlayerIndexMap; + std::map actionIndexToPlayerIndexMap; }; } diff --git a/src/storm/storage/PlayerIndex.h b/src/storm/storage/PlayerIndex.h new file mode 100644 index 000000000..7a903192d --- /dev/null +++ b/src/storm/storage/PlayerIndex.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace storage { + + typedef uint_fast64_t PlayerIndex; + PlayerIndex const INVALID_PLAYER_INDEX = std::numeric_limits::max(); + } +} \ No newline at end of file diff --git a/src/storm/storage/prism/Player.cpp b/src/storm/storage/prism/Player.cpp index d2110f7ec..353a2b8da 100644 --- a/src/storm/storage/prism/Player.cpp +++ b/src/storm/storage/prism/Player.cpp @@ -1,4 +1,5 @@ #include "storm/storage/prism/Player.h" +#include namespace storm { namespace prism { diff --git a/src/storm/storage/prism/Player.h b/src/storm/storage/prism/Player.h index 2af5c0be1..c680bf8cc 100644 --- a/src/storm/storage/prism/Player.h +++ b/src/storm/storage/prism/Player.h @@ -3,19 +3,11 @@ #include #include -#include "storm/storage/prism/Module.h" -#include "storm/storage/prism/Command.h" - -// needed? -#include "storm/storage/BoostTypes.h" -#include "storm/utility/OsDetection.h" +#include "storm/storage/prism/LocatedInformation.h" namespace storm { namespace prism { - typedef uint_fast64_t PlayerIndex; - PlayerIndex const INVALID_PLAYER_INDEX = std::numeric_limits::max(); - class Player : public LocatedInformation { public: /*! diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 5c8e2b4ef..98ba19af6 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -488,17 +488,17 @@ namespace storm { return this->getPlayers().size(); } - PlayerIndex const& Program::getIndexOfPlayer(std::string const& playerName) const { + storm::storage::PlayerIndex const& Program::getIndexOfPlayer(std::string const& playerName) const { return this->playerToIndexMap.at(playerName); } - std::map const& Program::getPlayerNameToIndexMapping() const { + std::map const& Program::getPlayerNameToIndexMapping() const { return playerToIndexMap; } - std::vector Program::buildModuleIndexToPlayerIndexMap() const { - std::vector result(this->getModules().size(), INVALID_PLAYER_INDEX); - for (PlayerIndex i = 0; i < this->getPlayers().size(); ++i) { + std::vector Program::buildModuleIndexToPlayerIndexMap() const { + std::vector result(this->getModules().size(), storm::storage::INVALID_PLAYER_INDEX); + for (storm::storage::PlayerIndex i = 0; i < this->getPlayers().size(); ++i) { for (auto const& module : this->getPlayers()[i].getModules()) { STORM_LOG_ASSERT(hasModule(module), "Module " << module << " not found."); STORM_LOG_ASSERT(moduleToIndexMap.at(module) < this->getModules().size(), "module index " << moduleToIndexMap.at(module) << " out of range."); @@ -508,15 +508,15 @@ namespace storm { return result; } - std::map Program::buildActionIndexToPlayerIndexMap() const { - std::map result; + std::map Program::buildActionIndexToPlayerIndexMap() const { + std::map result; // First insert an invalid player index for all available actions for (auto const& action : indexToActionMap) { - result.emplace_hint(result.end(), action.first, INVALID_PLAYER_INDEX); + result.emplace_hint(result.end(), action.first, storm::storage::INVALID_PLAYER_INDEX); } // Now set the actual player indices. // Note that actions that are not assigned to a player will still have INVALID_PLAYER_INDEX afterwards - for (PlayerIndex i = 0; i < this->getPlayers().size(); ++i) { + for (storm::storage::PlayerIndex i = 0; i < this->getPlayers().size(); ++i) { for (auto const& act : this->getPlayers()[i].getActions()) { STORM_LOG_ASSERT(hasAction(act), "Action " << act << " not found."); result.emplace(actionToIndexMap.at(act), i); @@ -847,7 +847,7 @@ namespace storm { for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex; } - for (PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) { + for (storm::storage::PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) { this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex; } for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index b96af20e9..496ac7bf8 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -17,6 +17,7 @@ #include "storm/storage/prism/Composition.h" #include "storm/storage/prism/Player.h" #include "storm/storage/BoostTypes.h" +#include "storm/storage/PlayerIndex.h" #include "storm/utility/solver.h" #include "storm/utility/OsDetection.h" @@ -338,24 +339,24 @@ namespace storm { * * @return The index of the player in the program. */ - PlayerIndex const& getIndexOfPlayer(std::string const& playerName) const; + storm::storage::PlayerIndex const& getIndexOfPlayer(std::string const& playerName) const; /*! * @return Retrieves the mapping of player names to their indices. */ - std::map const& getPlayerNameToIndexMapping() const; + std::map const& getPlayerNameToIndexMapping() const; /*! * Retrieves a vector whose i'th entry corresponds to the player controlling module i. * Modules that are not controlled by any player will get assigned INVALID_PLAYER_INDEX */ - std::vector buildModuleIndexToPlayerIndexMap() const; + std::vector buildModuleIndexToPlayerIndexMap() const; /*! * Retrieves a vector whose i'th entry corresponds to the player controlling action with index i. * Actions that are not controlled by any player (in particular the silent action) will get assigned INVALID_PLAYER_INDEX. */ - std::map buildActionIndexToPlayerIndexMap() const; + std::map buildActionIndexToPlayerIndexMap() const; /*! * Retrieves the mapping of action names to their indices. @@ -778,7 +779,7 @@ namespace storm { std::vector players; // A mapping of player names to their indices. - std::map playerToIndexMap; + std::map playerToIndexMap; // The modules associated with the program. std::vector modules;