generator now assigns player indices to states

src/storm/generator/PrismNextStateGenerator.cpp

@@ -80,6 +80,18 @@ 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.getCommands()) {
+                        commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex;
+                    }
+                }
+            }
         }
 
         template<typename ValueType, typename StateType>
@@ -369,6 +381,19 @@ 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.");
+                    }
+                }
+            }
+
             // Move all remaining choices in place.
             for (auto& choice : allChoices) {
                 result.addChoice(std::move(choice));
@@ -584,6 +609,12 @@ namespace storm {
                         choice.addReward(stateActionRewardValue);
                     }
 
+                    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]);
+                    }
+
                     if (this->options.isExplorationChecksSet()) {
                         // Check that the resulting distribution is in fact a distribution.
                         STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
@@ -646,6 +677,10 @@ namespace storm {
                         // Now create the actual distribution.
                         Choice<ValueType>& choice = choices.back();
 
+                        if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
+                            choice.setPlayerIndex(commandIndexToPlayerIndexMap[actionIndex]);
+                        }
+
                         // Remember the choice label and origins only if we were asked to.
                         if (this->options.isBuildChoiceLabelsSet()) {
                             choice.addLabel(program.getActionName(actionIndex));

src/storm/generator/PrismNextStateGenerator.h

@@ -111,17 +111,21 @@ namespace storm {
              * A recursive helper function to generate a synchronziing distribution.
              */
             void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> const& iteratorList, storm::builder::jit::Distribution<StateType, ValueType>& distribution, StateToIdCallback stateToIdCallback);
-            
+
             // The program used for the generation of next states.
             storm::prism::Program program;
-            
+
             // The reward models that need to be considered.
             std::vector<std::reference_wrapper<storm::prism::RewardModel const>> rewardModels;
-            
+
             // 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::map<uint_fast32_t, uint_fast32_t> moduleIndexToPlayerIndexMap;
+            std::map<uint_fast32_t, uint_fast32_t> commandIndexToPlayerIndexMap;
         };
-        
+
     }
 }