* 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

@@ -93,7 +93,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void Choice<ValueType, StateType>::setPlayerIndex(uint_fast32_t playerIndex) {
+        void Choice<ValueType, StateType>::setPlayerIndex(storm::storage::PlayerIndex playerIndex) {
             this->playerIndex = playerIndex;
         }
 
@@ -103,7 +103,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        uint_fast32_t const& Choice<ValueType, StateType>::getPlayerIndex() const {
+        storm::storage::PlayerIndex const& Choice<ValueType, StateType>::getPlayerIndex() const {
             return playerIndex.get();
         }
 

src/storm/generator/Choice.h

@@ -9,6 +9,7 @@
 #include <boost/any.hpp>
 
 #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<std::set<std::string>> labels;
 
             // The playerIndex of this choice
-            boost::optional<uint_fast32_t> playerIndex = boost::none;
+            boost::optional<storm::storage::PlayerIndex> playerIndex;
         };
 
         template<typename ValueType, typename StateType>

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<ValueType>& 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.

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<storm::prism::PlayerIndex> moduleIndexToPlayerIndexMap;
-            std::map<uint_fast64_t, storm::prism::PlayerIndex> actionIndexToPlayerIndexMap;
+            // Mappings from module/action indices to the programs players
+            std::vector<storm::storage::PlayerIndex> moduleIndexToPlayerIndexMap;
+            std::map<uint_fast64_t, storm::storage::PlayerIndex> actionIndexToPlayerIndexMap;
         };
 
     }

src/storm/storage/PlayerIndex.h

@@ -0,0 +1,11 @@
+#pragma once
+
+#include <limits>
+
+namespace storm {
+    namespace storage {
+        
+        typedef uint_fast64_t PlayerIndex;
+        PlayerIndex const INVALID_PLAYER_INDEX = std::numeric_limits<PlayerIndex>::max();
+    }
+}

src/storm/storage/prism/Player.cpp

@@ -1,4 +1,5 @@
 #include "storm/storage/prism/Player.h"
+#include <ostream>
 
 namespace storm {
     namespace prism {

src/storm/storage/prism/Player.h

@@ -3,19 +3,11 @@
 #include <string>
 #include <unordered_set>
 
-#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<PlayerIndex>::max();
-        
         class Player : public LocatedInformation {
         public:
             /*!

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<std::string, PlayerIndex> const& Program::getPlayerNameToIndexMapping() const {
+        std::map<std::string, storm::storage::PlayerIndex> const& Program::getPlayerNameToIndexMapping() const {
             return playerToIndexMap;
         }
         
-        std::vector<PlayerIndex> Program::buildModuleIndexToPlayerIndexMap() const {
-            std::vector<PlayerIndex> result(this->getModules().size(), INVALID_PLAYER_INDEX);
-            for (PlayerIndex i = 0; i < this->getPlayers().size(); ++i) {
+        std::vector<storm::storage::PlayerIndex> Program::buildModuleIndexToPlayerIndexMap() const {
+            std::vector<storm::storage::PlayerIndex> 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<uint64_t, PlayerIndex> Program::buildActionIndexToPlayerIndexMap() const {
-            std::map<uint64_t, PlayerIndex> result;
+        std::map<uint64_t, storm::storage::PlayerIndex> Program::buildActionIndexToPlayerIndexMap() const {
+            std::map<uint64_t, storm::storage::PlayerIndex> 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) {

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<std::string, PlayerIndex> const& getPlayerNameToIndexMapping() const;
+            std::map<std::string, storm::storage::PlayerIndex> 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<PlayerIndex> buildModuleIndexToPlayerIndexMap() const;
+            std::vector<storm::storage::PlayerIndex> 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<uint_fast64_t, PlayerIndex> buildActionIndexToPlayerIndexMap() const;
+            std::map<uint_fast64_t, storm::storage::PlayerIndex> buildActionIndexToPlayerIndexMap() const;
             
             /*!
              * Retrieves the mapping of action names to their indices.
@@ -778,7 +779,7 @@ namespace storm {
             std::vector<Player> players;
 
             // A mapping of player names to their indices.
-            std::map<std::string, PlayerIndex> playerToIndexMap;
+            std::map<std::string, storm::storage::PlayerIndex> playerToIndexMap;
 
             // The modules associated with the program.
             std::vector<Module> modules;