diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index b1e80ab8b..2bdddcbb7 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -58,7 +58,7 @@ namespace storm { STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of rows of transition matrix does not match state count."); STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of columns of transition matrix does not match state count."); STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); - } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton) || this->isOfType(ModelType::Pomdp)) { + } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton) || this->isOfType(ModelType::Pomdp) || this->isOfType(ModelType::Smg)) { STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of row groups (" << this->getTransitionMatrix().getRowGroupCount() << ") of transition matrix does not match state count (" << stateCount << ")."); STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of columns of transition matrix does not match state count."); STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); @@ -67,8 +67,6 @@ namespace storm { STORM_LOG_ASSERT(components.player1Matrix->isProbabilistic(), "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry."); STORM_LOG_THROW(stateCount == components.player1Matrix->getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p1 matrix does not match state count."); STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount() == components.player1Matrix->getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix."); - } else if (this->isOfType(ModelType::Smg)) { - STORM_LOG_DEBUG("Smg parsed"); } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Invalid model type."); } @@ -82,6 +80,17 @@ namespace storm { STORM_LOG_WARN_COND(!components.rateTransitions && !components.exitRates.is_initialized(), "Rates specified for discrete-time model. The rates will be ignored."); } STORM_LOG_WARN_COND(this->isOfType(ModelType::MarkovAutomaton) || !components.markovianStates.is_initialized(), "Markovian states given for a model that is not a Markov automaton (will be ignored)."); + + // Treat stochastic multiplayer games + if (this->isOfType(ModelType::Smg)) { + STORM_LOG_THROW(components.statePlayerIndications.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create stochastic multiplayer game: Missing player indications."); + // playerNameToIndexMap is optional. + STORM_LOG_THROW(stateCount == components.statePlayerIndications->size(), storm::exceptions::IllegalArgumentException, "Size of state player indications (" << components.statePlayerIndications->size() << ") of SMG does not match state count (" << stateCount << ")."); + } else { + STORM_LOG_WARN_COND(!components.statePlayerIndications.is_initialized(), "statePlayerIndications given for a model that is not a stochastic multiplayer game (will be ignored)."); + STORM_LOG_WARN_COND(!components.playerNameToIndexMap.is_initialized(), "playerNameToIndexMap given for a model that is not a stochastic multiplayer game (will be ignored)."); + } + } template diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index e0419844c..a909523c0 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -6,37 +6,72 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace models { namespace sparse { template - Smg::Smg(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, ModelType type) - : Smg(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels), type) { - // Intentionally left empty + Smg::Smg(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::Smg, components), statePlayerIndications(components.statePlayerIndications.get()) { + if (components.playerNameToIndexMap) { + playerNameToIndexMap = components.playerNameToIndexMap.get(); + } + // Otherwise the map remains empty. + } + + template + Smg::Smg(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::Smg, std::move(components)), statePlayerIndications(std::move(components.statePlayerIndications.get())) { + if (components.playerNameToIndexMap) { + playerNameToIndexMap = std::move(components.playerNameToIndexMap.get()); + } + // Otherwise the map remains empty. } template - Smg::Smg(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, ModelType type) - : Smg(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)), type) { - // Intentionally left empty + std::vector const& Smg::getStatePlayerIndications() const { + return statePlayerIndications; } template - Smg::Smg(storm::storage::sparse::ModelComponents const& components, ModelType type) - : NondeterministicModel(type, components) { - assert(type == storm::models::ModelType::Smg); - // Intentionally left empty + storm::storage::PlayerIndex Smg::getPlayerOfState(uint64_t stateIndex) const { + STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << "."); + return statePlayerIndications[stateIndex]; } - template - Smg::Smg(storm::storage::sparse::ModelComponents&& components, ModelType type) - : NondeterministicModel(type, std::move(components)) { - assert(type == storm::models::ModelType::Smg); - // Intentionally left empty + template + storm::storage::PlayerIndex Smg::getPlayerIndex(std::string const& playerName) const { + auto findIt = playerNameToIndexMap.find(playerName); + STORM_LOG_THROW(findIt != playerNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown player name '" << playerName << "'."); + return findIt->second; + } + + template + storm::storage::BitVector Smg::computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const { + // Create a set and a bit vector encoding the coalition for faster access + std::set coalitionAsIndexSet; + for (auto const& player : coalition.getPlayers()) { + if (player.type() == typeid(std::string)) { + coalitionAsIndexSet.insert(getPlayerIndex(boost::get(player))); + } else { + STORM_LOG_ASSERT(player.type() == typeid(storm::storage::PlayerIndex), "Player identifier has unexpected type."); + coalitionAsIndexSet.insert(boost::get(player)); + } + } + storm::storage::BitVector coalitionAsBitVector(*coalitionAsIndexSet.rbegin()+1, false); + for (auto const& pi : coalitionAsIndexSet) { + coalitionAsBitVector.set(pi); + } + + // Now create the actual result + storm::storage::BitVector result(this->getNumberOfStates(), false); + for (uint64_t state = 0; state < this->getNumberOfStates(); ++state) { + if (coalitionAsBitVector.get(statePlayerIndications[state])) { + result.set(state, true); + } + } + + return result; } template class Smg; diff --git a/src/storm/models/sparse/Smg.h b/src/storm/models/sparse/Smg.h index 663817418..b16475c18 100644 --- a/src/storm/models/sparse/Smg.h +++ b/src/storm/models/sparse/Smg.h @@ -2,6 +2,9 @@ #define STORM_MODELS_SPARSE_SMG_H_ #include "storm/models/sparse/NondeterministicModel.h" +#include "storm/storage/PlayerIndex.h" +#include "storm/storage/BitVector.h" +#include "storm/logic/PlayerCoalition.h" namespace storm { namespace models { @@ -13,41 +16,31 @@ namespace storm { template> class Smg : public NondeterministicModel { public: - /*! - * Constructs a model from the given data. - * - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - */ - Smg(storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map(), ModelType type = ModelType::Smg); - - /*! - * Constructs a model by moving the given data. - * - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - */ - Smg(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), ModelType type = ModelType::Smg); - /*! * Constructs a model from the given data. * * @param components The components for this model. */ - Smg(storm::storage::sparse::ModelComponents const& components, ModelType type = ModelType::Smg); - Smg(storm::storage::sparse::ModelComponents&& components, ModelType type = ModelType::Smg); + Smg(storm::storage::sparse::ModelComponents const& components); + Smg(storm::storage::sparse::ModelComponents&& components); Smg(Smg const& other) = default; Smg& operator=(Smg const& other) = default; Smg(Smg&& other) = default; Smg& operator=(Smg&& other) = default; + + std::vector const& getStatePlayerIndications() const; + storm::storage::PlayerIndex getPlayerOfState(uint64_t stateIndex) const; + storm::storage::PlayerIndex getPlayerIndex(std::string const& playerName) const; + storm::storage::BitVector computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const; + + private: + // Assigns the controlling player to each state. + // If a state has storm::storage::INVALID_PLAYER_INDEX, it shall be the case that the choice at that state is unique + std::vector statePlayerIndications; + // A mapping of player names to player indices. + std::map playerNameToIndexMap; }; } // namespace sparse