* prism::Player's no longer keep track of module and action indices to reduce redundancies.

* PrismProgram::CheckValidity and PrismProgram::simplify now treat SMGs properly
* PrismProgram is now responsible for moduleIndex->playerIndex and actionIndex->playerIndex assignment
* More defined behavior for actions that don't have a player (work in progress)

src/storm-parsers/parser/PrismParser.cpp

@@ -1,5 +1,6 @@
 #include "storm-parsers/parser/PrismParser.h"
 
+#include <unordered_set>
 #include "storm/storage/prism/Compositions.h"
 
 
@@ -787,23 +788,23 @@ namespace storm {
 
         storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames, std::vector<std::string> const & actionNames) {
             if (this->secondRun) {
-                std::map<std::string, uint_fast64_t> controlledModuleIndices;
-                std::map<std::string, uint_fast64_t> controlledActionIndices;
+                std::unordered_set<std::string> controlledModules;
+                std::unordered_set<std::string> controlledActions;
                 for(auto const& moduleName : moduleNames) {
                     auto moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
                     STORM_LOG_ASSERT(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(),  "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
-                    controlledModuleIndices.insert(*moduleIndexPair);
+                    controlledModules.insert(moduleIndexPair->first);
                     bool moduleNotYetControlled = globalProgramInformation.playerControlledModules.insert(moduleIndexPair->second).second;
                     STORM_LOG_THROW(moduleNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName << "' already controlled by another player.");
                 }
                 for(std::string actionName : actionNames) {
                     auto actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
                     STORM_LOG_ASSERT(actionIndexPair != globalProgramInformation.actionIndices.end(),  "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
-                    controlledActionIndices.insert(*actionIndexPair);
+                    controlledActions.insert(actionIndexPair->first);
                     bool actionNotYetControlled = globalProgramInformation.playerControlledActions.insert(actionIndexPair->second).second;
                     STORM_LOG_THROW(actionNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName << "' already controlled by another player.");
                 }
-                return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices);
+                return storm::prism::Player(playerName, controlledModules, controlledActions);
             } else {
                 return storm::prism::Player();
             }

src/storm/generator/PrismNextStateGenerator.cpp

@@ -82,15 +82,8 @@ namespace storm {
             }
 
             if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
-                for (auto const& player : program.getPlayers()) {
-                    uint_fast32_t playerIndex = program.getIndexOfPlayer(player.getName());
-                    for (auto const& moduleIndexPair : player.getModules()) {
-                        moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex;
-                    }
-                    for (auto const& commandIndexPair : player.getActions()) {
-                        commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex;
-                    }
-                }
+                moduleIndexToPlayerIndexMap = program.buildModuleIndexToPlayerIndexMap();
+                actionIndexToPlayerIndexMap = program.buildActionIndexToPlayerIndexMap();
             }
         }
 
@@ -610,8 +603,6 @@ 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]);
                     }
 
@@ -678,7 +669,7 @@ namespace storm {
                         Choice<ValueType>& choice = choices.back();
 
                         if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
-                            choice.setPlayerIndex(commandIndexToPlayerIndexMap[actionIndex]);
+                            choice.setPlayerIndex(actionIndexToPlayerIndexMap[actionIndex]);
                         }
 
                         // Remember the choice label and origins only if we were asked to.

src/storm/generator/PrismNextStateGenerator.h

@@ -122,8 +122,8 @@ namespace storm {
             bool hasStateActionRewards;
 
             // A mapping from modules/commands to the programs players
-            std::map<uint_fast32_t, uint_fast32_t> moduleIndexToPlayerIndexMap;
-            std::map<uint_fast32_t, uint_fast32_t> commandIndexToPlayerIndexMap;
+            std::vector<storm::prism::PlayerIndex> moduleIndexToPlayerIndexMap;
+            std::map<uint_fast64_t, storm::prism::PlayerIndex> actionIndexToPlayerIndexMap;
         };
 
     }

src/storm/storage/prism/Player.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace prism {
-        Player::Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> const& controlledActions, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledActions(controlledActions) {
+        Player::Player(std::string const& playerName, std::unordered_set<std::string> const& controlledModules, std::unordered_set<std::string> const& controlledActions, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledActions(controlledActions) {
             // Nothing to do here.
         }
 
@@ -10,11 +10,11 @@ namespace storm {
             return this->playerName;
         }
 
-        std::map<std::string, uint_fast64_t> const& Player::getModules() const {
+        std::unordered_set<std::string> const& Player::getModules() const {
             return this->controlledModules;
         }
 
-        std::map<std::string, uint_fast64_t> const& Player::getActions() const {
+        std::unordered_set<std::string> const& Player::getActions() const {
             return this->controlledActions;
         }
 
@@ -25,10 +25,10 @@ namespace storm {
             }
             stream << std::endl;
             for (auto const& module : player.getModules()) {
-                stream << "\t" << module.first << std::endl;
+                stream << "\t" << module << std::endl;
             }
-            for (auto const& command : player.getActions()) {
-                stream << "\t[" << command.first << "]" << std::endl;
+            for (auto const& action : player.getActions()) {
+                stream << "\t[" << action << "]" << std::endl;
             }
             stream << "endplayer" << std::endl;
             return stream;

src/storm/storage/prism/Player.h

@@ -1,7 +1,7 @@
 #pragma once
 
 #include <string>
-#include <vector>
+#include <unordered_set>
 
 #include "storm/storage/prism/Module.h"
 #include "storm/storage/prism/Command.h"
@@ -14,6 +14,7 @@ namespace storm {
     namespace prism {
         
         typedef uint_fast64_t PlayerIndex;
+        PlayerIndex const INVALID_PLAYER_INDEX = std::numeric_limits<PlayerIndex>::max();
         
         class Player : public LocatedInformation {
         public:
@@ -26,7 +27,7 @@ namespace storm {
              * @param filename The filename in which the player is defined.
              * @param lineNumber The line number in which the player is defined.
              */
-            Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> const& controlledActions, std::string const& filename = "", uint_fast32_t lineNumber = 0);
+            Player(std::string const& playerName, std::unordered_set<std::string> const& controlledModules, std::unordered_set<std::string> const& controlledActions, std::string const& filename = "", uint_fast32_t lineNumber = 0);
 
             // Create default implementations of constructors/assignment.
             Player() = default;
@@ -47,14 +48,14 @@ namespace storm {
              *
              * @return The modules controlled by the player.
              */
-            std::map<std::string, uint_fast64_t> const& getModules() const; // TODO
+            std::unordered_set<std::string> const& getModules() const;
 
             /*!
              * Retrieves all controlled Actions of the player.
              *
              * @return The Actions controlled by the player.
              */
-            std::map<std::string, uint_fast64_t> const& getActions() const;
+            std::unordered_set<std::string> const& getActions() const;
 
             friend std::ostream& operator<<(std::ostream& stream, Player const& player);
         private:
@@ -62,10 +63,10 @@ namespace storm {
             std::string playerName;
 
             // The modules associated with this player.
-            std::map<std::string, uint_fast64_t> controlledModules;
+            std::unordered_set<std::string> controlledModules;
 
             // The Actions associated with this player.
-            std::map<std::string, uint_fast64_t> controlledActions;
+            std::unordered_set<std::string>  controlledActions;
         };
 
     } // namespace prism

src/storm/storage/prism/Program.cpp

@@ -16,6 +16,7 @@
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/InternalException.h"
 #include "storm/solver/SmtSolver.h"
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
@@ -494,6 +495,35 @@ namespace storm {
         std::map<std::string, 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) {
+                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.");
+                    result[moduleToIndexMap.at(module)] = i;
+                }
+            }
+            return result;
+        }
+        
+        std::map<uint64_t, PlayerIndex> Program::buildActionIndexToPlayerIndexMap() const {
+            std::map<uint64_t, 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);
+            }
+            // 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 (auto const& act : this->getPlayers()[i].getActions()) {
+                    STORM_LOG_ASSERT(hasAction(act), "Action " << act << " not found.");
+                    result.emplace(actionToIndexMap.at(act), i);
+                }
+            }
+            return result;
+        }
 
         std::size_t Program::getNumberOfFormulas() const {
             return this->getFormulas().size();
@@ -1371,6 +1401,17 @@ namespace storm {
                 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
             }
 
+            // Check the players
+            for (auto const& player : this->getPlayers()) {
+                // The stored action/module names shall be available
+                for (auto const& controlledAction : player.getActions()) {
+                    STORM_LOG_THROW(this->hasAction(controlledAction), storm::exceptions::InternalException, "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled action " << controlledAction << " is not available.");
+                }
+                for (auto const& controlledModule : player.getModules()) {
+                    STORM_LOG_THROW(this->hasModule(controlledModule), storm::exceptions::InternalException, "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled module " << controlledModule << " is not available.");
+                }
+            }
+            
             if(lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
                 // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
                 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
@@ -1500,6 +1541,7 @@ namespace storm {
             // If we have to delete whole actions, do so now.
             std::map<std::string, uint_fast64_t> newActionToIndexMap;
             std::vector<RewardModel> newRewardModels;
+            std::vector<Player> newPlayers;
             if (!actionIndicesToDelete.empty()) {
                 storm::storage::FlatSet<uint_fast64_t> actionsToKeep;
                 std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
@@ -1519,11 +1561,23 @@ namespace storm {
                     newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
                 }
 
+                // Restrict action name to index mapping. Old action indices remain valid.
                 for (auto const& entry : this->getActionNameToIndexMapping()) {
                     if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
                         newActionToIndexMap.emplace(entry.first, entry.second);
                     }
                 }
+                
+                // Restrict player controlled actions
+                for (auto const& player : this->getPlayers()) {
+                    std::unordered_set<std::string> newControlledActions;
+                    for (auto const& act : player.getActions()) {
+                        if (newActionToIndexMap.count(act) != 0) {
+                            newControlledActions.insert(act);
+                        }
+                    }
+                    newPlayers.emplace_back(player.getName(), player.getModules(), newControlledActions, player.getFilename(), player.getLineNumber());
+                }
             }
 
             std::vector<Label> newLabels;
@@ -1531,7 +1585,7 @@ namespace storm {
                 newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
             }
 
-            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), this->getPlayers(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), actionIndicesToDelete.empty() ? this->getPlayers() : newPlayers, newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
 
         Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {

src/storm/storage/prism/Program.h

@@ -345,6 +345,18 @@ namespace storm {
              */
             std::map<std::string, 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;
+            
+            /*!
+             * 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;
+            
             /*!
              * Retrieves the mapping of action names to their indices.
              *