Polished SMG model

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<typename ValueType, typename RewardModelType>

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 <typename ValueType, typename RewardModelType>
-            Smg<ValueType, RewardModelType>::Smg(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
-                                  std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
-                    : Smg<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels), type) {
-                // Intentionally left empty
+            Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components) : NondeterministicModel<ValueType, RewardModelType>(ModelType::Smg, components), statePlayerIndications(components.statePlayerIndications.get()) {
+                if (components.playerNameToIndexMap) {
+                    playerNameToIndexMap = components.playerNameToIndexMap.get();
+                }
+                // Otherwise the map remains empty.
+            }
+
+            template <typename ValueType, typename RewardModelType>
+            Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) : NondeterministicModel<ValueType, RewardModelType>(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 <typename ValueType, typename RewardModelType>
-            Smg<ValueType, RewardModelType>::Smg(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
-                                  std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
-                    : Smg<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)), type) {
-                // Intentionally left empty
+            std::vector<storm::storage::PlayerIndex> const& Smg<ValueType, RewardModelType>::getStatePlayerIndications() const {
+                return statePlayerIndications;
             }
 
             template <typename ValueType, typename RewardModelType>
-            Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type)
-                    : NondeterministicModel<ValueType, RewardModelType>(type, components) {
-                assert(type == storm::models::ModelType::Smg);
-                // Intentionally left empty
+            storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerOfState(uint64_t stateIndex) const {
+                STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << ".");
+                return statePlayerIndications[stateIndex];
             }
 
-           template <typename ValueType, typename RewardModelType>
-            Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type)
-                    : NondeterministicModel<ValueType, RewardModelType>(type, std::move(components)) {
-               assert(type == storm::models::ModelType::Smg);
-                // Intentionally left empty
+            template <typename ValueType, typename RewardModelType>
+            storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
+            storm::storage::BitVector Smg<ValueType, RewardModelType>::computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const {
+                // Create a set and a bit vector encoding the coalition for faster access
+                std::set<storm::storage::PlayerIndex> coalitionAsIndexSet;
+                for (auto const& player : coalition.getPlayers()) {
+                    if (player.type() == typeid(std::string)) {
+                        coalitionAsIndexSet.insert(getPlayerIndex(boost::get<std::string>(player)));
+                    } else {
+                        STORM_LOG_ASSERT(player.type() == typeid(storm::storage::PlayerIndex), "Player identifier has unexpected type.");
+                        coalitionAsIndexSet.insert(boost::get<storm::storage::PlayerIndex>(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<double>;

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 ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
             class Smg : public NondeterministicModel<ValueType, RewardModelType> {
             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<ValueType> const& transitionMatrix,
-                    storm::models::sparse::StateLabeling const& stateLabeling,
-                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(), 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<ValueType>&& transitionMatrix,
-                    storm::models::sparse::StateLabeling&& stateLabeling,
-                    std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Smg);
-
                 /*!
                  * Constructs a model from the given data.
                  *
                  * @param components The components for this model.
                  */
-                Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type = ModelType::Smg);
-                Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type = ModelType::Smg);
+                Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
+                Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
 
                 Smg(Smg<ValueType, RewardModelType> const& other) = default;
                 Smg& operator=(Smg<ValueType, RewardModelType> const& other) = default;
 
                 Smg(Smg<ValueType, RewardModelType>&& other) = default;
                 Smg& operator=(Smg<ValueType, RewardModelType>&& other) = default;
+
+                std::vector<storm::storage::PlayerIndex> 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<storm::storage::PlayerIndex> statePlayerIndications;
+                // A mapping of player names to player indices.
+                std::map<std::string, storm::storage::PlayerIndex> playerNameToIndexMap;
             };
 
         } // namespace sparse