Polished ExplicitModelBuilder:

* ChoiceInformationBuilder renamed to StateAndChoiceInformationBuilder, now also keeping track of state-based information (StateValuations, MarkovianStates, statePlayerIndications)
* ModelComponents now consider statePlayerIndications and PlayerNamesToIndices separately

src/storm/builder/ChoiceInformationBuilder.cpp

@@ -1,38 +0,0 @@
-#include "storm/builder/ChoiceInformationBuilder.h"
-
-namespace storm {
-    namespace builder {
-         
-        void ChoiceInformationBuilder::addLabel(std::string const& label, uint_fast64_t choiceIndex) {
-            storm::storage::BitVector& labeledChoices = labels[label];
-            labeledChoices.grow(choiceIndex + 1);
-            labeledChoices.set(choiceIndex, true);
-        }
-        
-        void ChoiceInformationBuilder::addOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
-            if (dataOfOrigins.size() != choiceIndex) {
-                dataOfOrigins.resize(choiceIndex);
-            }
-            dataOfOrigins.push_back(originData);
-        }
-        
-        boost::optional<storm::models::sparse::ChoiceLabeling> ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
-            if (labels.empty()) {
-                return boost::none;
-            } else {
-                storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
-                for (auto& label : labels) {
-                    label.second.resize(totalNumberOfChoices, false);
-                    result.addLabel(label.first, std::move(label.second));
-                }
-                return result;
-            }
-        }
-            
-        std::vector<boost::any> ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
-            dataOfOrigins.resize(totalNumberOfChoices);
-            return std::move(dataOfOrigins);
-        }
-        
-    }
-}

src/storm/builder/ChoiceInformationBuilder.h

@@ -1,40 +0,0 @@
-#pragma once
-
-#include <memory>
-#include <string>
-#include <unordered_map>
-#include <vector>
-#include <boost/any.hpp>
-
-#include "storm/models/sparse/ChoiceLabeling.h"
-#include "storm/storage/BitVector.h"
-#include "storm/storage/sparse/PrismChoiceOrigins.h"
-#include "storm/storage/prism/Program.h"
-
-
-namespace storm {
-    namespace builder {
-        
-        /*!
-         * This class collects information regarding the choices
-         */
-        class ChoiceInformationBuilder {
-        public:
-            
-            ChoiceInformationBuilder() = default;
-
-            void addLabel(std::string const& label, uint_fast64_t choiceIndex);
-            
-            void addOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
-            
-            boost::optional<storm::models::sparse::ChoiceLabeling> buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
-            
-            std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
-            
-        private:
-            std::unordered_map<std::string, storm::storage::BitVector> labels;
-            std::vector<boost::any> dataOfOrigins;
-        };
-    }
-}
-    

src/storm/builder/ExplicitModelBuilder.cpp

@@ -4,7 +4,7 @@
 
 
 #include "storm/builder/RewardModelBuilder.h"
-#include "storm/builder/ChoiceInformationBuilder.h"
+#include "storm/builder/StateAndChoiceInformationBuilder.h"
 
 #include "storm/exceptions/AbortException.h"
 #include "storm/exceptions/WrongFormatException.h"
@@ -120,18 +120,11 @@ namespace storm {
         }
 
         template <typename ValueType, typename RewardModelType, typename StateType>
-        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
+        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder) {
 
-            // Create markovian states bit vector, if required.
-            if (generator->getModelType() == storm::generator::ModelType::MA) {
-                // The bit vector will be resized when the correct size is known.
-                markovianStates = storm::storage::BitVector(1000);
-            }
-
-            // Create the player indices vector, if required.
-            if (generator->getModelType() == storm::generator::ModelType::SMG) {
-                playerActionIndices = std::vector<uint_fast32_t>{};
-                playerActionIndices.get().reserve(1000);
+            // Initialize building state valuations (if necessary)
+            if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+                stateAndChoiceInformationBuilder.stateValuationsBuilder() = generator->initializeStateValuationsBuilder();
             }
 
             // Create a callback for the next-state generator to enable it to request the index of states.
@@ -175,8 +168,8 @@ namespace storm {
                 }
 
                 generator->load(currentState);
-                if (stateValuationsBuilder) {
-                    generator->addStateValuation(currentIndex, stateValuationsBuilder.get());
+                if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+                    generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder());
                 }
                 storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
 
@@ -188,11 +181,6 @@ namespace storm {
                             this->stateStorage.deadlockStateIndices.push_back(currentIndex);
                         }
 
-                        if (markovianStates) {
-                            markovianStates.get().grow(currentRowGroup + 1, false);
-                            markovianStates.get().set(currentRowGroup);
-                        }
-
                         if (!generator->isDeterministicModel()) {
                             transitionMatrixBuilder.newRowGroup(currentRow);
                         }
@@ -208,11 +196,14 @@ namespace storm {
                                 rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>());
                             }
                         }
-
-                        if (playerActionIndices) {
-                            // TODO change this to storm::utility::infinity<ValueType>() ?
-                            playerActionIndices.get().push_back(-1);
+                        
+                        // This state shall be Markovian (to not introduce Zeno behavior)
+                        if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) {
+                            stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup);
                         }
+                        // Other state-based information does not need to be treated, in particular:
+                        // * StateValuations have already been set above
+                        // * The associated player shall be the "default" player, i.e. INVALID_PLAYER_INDEX
 
                         ++currentRow;
                         ++currentRowGroup;
@@ -235,22 +226,26 @@ namespace storm {
                     }
 
                     // Now add all choices.
+                    bool firstChoiceOfState = true;
                     for (auto const& choice : behavior) {
 
                         // add the generated choice information
-                        if (choice.hasLabels()) {
+                        if (stateAndChoiceInformationBuilder.isBuildChoiceLabels() && choice.hasLabels()) {
                             for (auto const& label : choice.getLabels()) {
-                                choiceInformationBuilder.addLabel(label, currentRow);
+                                stateAndChoiceInformationBuilder.addChoiceLabel(label, currentRow);
                             }
                         }
-                        if (choice.hasOriginData()) {
-                            choiceInformationBuilder.addOriginData(choice.getOriginData(), currentRow);
+                        if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins() && choice.hasOriginData()) {
+                            stateAndChoiceInformationBuilder.addChoiceOriginData(choice.getOriginData(), currentRow);
                         }
-
-                        // If we keep track of the Markovian choices, store whether the current one is Markovian.
-                        if (markovianStates && choice.isMarkovian()) {
-                            markovianStates.get().grow(currentRowGroup + 1, false);
-                            markovianStates.get().set(currentRowGroup);
+                        if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications() && choice.hasPlayerIndex()) {
+                            STORM_LOG_ASSERT(firstChoiceOfState || stateAndChoiceInformationBuilder.hasStatePlayerIndicationBeenSet(choice.getPlayerIndex(), currentRowGroup), "There is a state where different players have an enabled choice."); // Should have been detected in generator, already
+                            if (firstChoiceOfState) {
+                                stateAndChoiceInformationBuilder.addStatePlayerIndication(choice.getPlayerIndex(), currentRowGroup);
+                            }
+                        }
+                        if (stateAndChoiceInformationBuilder.isBuildMarkovianStates() &&  choice.isMarkovian()) {
+                            stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup);
                         }
 
                         // Add the probabilistic behavior to the matrix.
@@ -267,11 +262,9 @@ namespace storm {
                             ++choiceRewardIt;
                         }
                         ++currentRow;
+                        firstChoiceOfState = false;
                     }
 
-                    if (playerActionIndices) {
-                        playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex());
-                    }
                     ++currentRowGroup;
                 }
 
@@ -298,15 +291,6 @@ namespace storm {
                 }
             }
 
-            if (markovianStates) {
-                // Since we now know the correct size, cut the bit vector to the correct length.
-                markovianStates->resize(currentRowGroup, false);
-            }
-
-            if (playerActionIndices) {
-                playerActionIndices.get().shrink_to_fit();
-            }
-
             // If the exploration order was not breadth-first, we need to fix the entries in the matrix according to
             // (reversed) mapping of row groups to indices.
             if (options.explorationOrder != ExplorationOrder::Bfs) {
@@ -348,39 +332,48 @@ namespace storm {
             for (uint64_t i = 0; i < generator->getNumberOfRewardModels(); ++i) {
                 rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i));
             }
-            ChoiceInformationBuilder choiceInformationBuilder;
-            boost::optional<storm::storage::BitVector> markovianStates;
-            boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
-
-            // If we need to build state valuations, initialize them now.
-            boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;
-            if (generator->getOptions().isBuildStateValuationsSet()) {
-                stateValuationsBuilder = generator->initializeStateValuationsBuilder();
-            }
-
-            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, playerActionIndices, stateValuationsBuilder);
-
+            StateAndChoiceInformationBuilder stateAndChoiceInformationBuilder;
+            stateAndChoiceInformationBuilder.setBuildChoiceLabels(generator->getOptions().isBuildChoiceLabelsSet());
+            stateAndChoiceInformationBuilder.setBuildChoiceOrigins(generator->getOptions().isBuildChoiceOriginsSet());
+            stateAndChoiceInformationBuilder.setBuildStatePlayerIndications(generator->getModelType() == storm::generator::ModelType::SMG);
+            stateAndChoiceInformationBuilder.setBuildMarkovianStates(generator->getModelType() == storm::generator::ModelType::MA);
+            stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet());
+
+            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder);
+            
             // Initialize the model components with the obtained information.
-            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates), /* player1Matrix = */ boost::none, std::move(playerActionIndices));
+            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel());
+
+            uint_fast64_t numStates = modelComponents.transitionMatrix.getColumnCount();
+            uint_fast64_t numChoices = modelComponents.transitionMatrix.getRowCount();
 
             // Now finalize all reward models.
             for (auto& rewardModelBuilder : rewardModelBuilders) {
-                modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
+                modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(numChoices, modelComponents.transitionMatrix.getColumnCount(), numStates));
+            }
+            // Build the player assignment
+            if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications()) {
+                modelComponents.statePlayerIndications = stateAndChoiceInformationBuilder.buildStatePlayerIndications(numStates);
+                modelComponents.playerNameToIndexMap = generator->getPlayerNameToIndexMap();
+            }
+            // Build Markovian states
+            if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) {
+                modelComponents.markovianStates = stateAndChoiceInformationBuilder.buildMarkovianStates(numStates);
             }
             // Build the choice labeling
-            modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
-
+            if (stateAndChoiceInformationBuilder.isBuildChoiceLabels()) {
+                modelComponents.choiceLabeling = stateAndChoiceInformationBuilder.buildChoiceLabeling(numChoices);
+            }
             // If requested, build the state valuations and choice origins
-            if (stateValuationsBuilder) {
-                modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount());
+            if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+                modelComponents.stateValuations = stateAndChoiceInformationBuilder.stateValuationsBuilder().build(numStates);
             }
-            if (generator->getOptions().isBuildChoiceOriginsSet()) {
-                auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
+            if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins()) {
+                auto originData = stateAndChoiceInformationBuilder.buildDataOfChoiceOrigins(numChoices);
                 modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData);
             }
             if (generator->isPartiallyObservable()) {
-                std::vector<uint32_t> classes;
-                classes.resize(stateStorage.getNumberOfStates());
+                std::vector<uint32_t> classes(stateStorage.getNumberOfStates());
                 std::unordered_map<uint32_t, std::vector<std::pair<std::vector<std::string>, uint32_t>>> observationActions;
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
                     uint32_t varObservation = generator->observabilityClass(bitVectorIndexPair.first);

src/storm/builder/ExplicitModelBuilder.h

@@ -43,7 +43,7 @@ namespace storm {
         
         // Forward-declare classes.
         template <typename ValueType> class RewardModelBuilder;
-        class ChoiceInformationBuilder;
+        class StateAndChoiceInformationBuilder;
 
         template<typename StateType>
         class ExplicitStateLookup {
@@ -127,11 +127,9 @@ namespace storm {
              *
              * @param transitionMatrixBuilder The builder of the transition matrix.
              * @param rewardModelBuilders The builders for the selected reward models.
-             * @param choiceInformationBuilder The builder for the requested information of the choices
-             * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
-             * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
+             * @param stateAndChoiceInformationBuilder The builder for the requested information of the individual states and choices
              */
-            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
+            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder);
 
             /*!
              * Explores the state space of the given program and returns the components of the model as a result.

src/storm/builder/StateAndChoiceInformationBuilder.cpp

@@ -0,0 +1,121 @@
+#include "storm/builder/StateAndChoiceInformationBuilder.h"
+
+namespace storm {
+    namespace builder {
+
+        StateAndChoiceInformationBuilder::StateAndChoiceInformationBuilder() : _buildChoiceLabels(false), _buildChoiceOrigins(false), _buildStatePlayerIndications(false), _buildMarkovianStates(false), _buildStateValuations(false) {
+            // Intentionally left empty
+        }
+
+        void StateAndChoiceInformationBuilder::setBuildChoiceLabels(bool value) {
+            _buildChoiceLabels = value;
+        }
+
+        bool StateAndChoiceInformationBuilder::isBuildChoiceLabels() const {
+            return _buildChoiceLabels;
+        }
+
+        void StateAndChoiceInformationBuilder::addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex) {
+            STORM_LOG_ASSERT(_buildChoiceLabels, "Building ChoiceLabels was not enabled.");
+            storm::storage::BitVector& labeledChoices = _choiceLabels[label];
+            labeledChoices.grow(choiceIndex + 1, false);
+            labeledChoices.set(choiceIndex, true);
+        }
+
+        storm::models::sparse::ChoiceLabeling StateAndChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
+            storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
+            for (auto& label : _choiceLabels) {
+                label.second.resize(totalNumberOfChoices, false);
+                result.addLabel(label.first, std::move(label.second));
+            }
+            return result;
+        }
+
+        void StateAndChoiceInformationBuilder::setBuildChoiceOrigins(bool value) {
+            _buildChoiceOrigins = value;
+        }
+
+        bool StateAndChoiceInformationBuilder::isBuildChoiceOrigins() const {
+            return _buildChoiceOrigins;
+        }
+
+        void StateAndChoiceInformationBuilder::addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
+            STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled.");
+            STORM_LOG_ASSERT(_dataOfChoiceOrigins.size() <= choiceIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
+            if (_dataOfChoiceOrigins.size() != choiceIndex) {
+                _dataOfChoiceOrigins.resize(choiceIndex);
+            }
+            _dataOfChoiceOrigins.push_back(originData);
+        }
+
+        std::vector<boost::any> StateAndChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
+            STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled.");
+            _dataOfChoiceOrigins.resize(totalNumberOfChoices);
+            _dataOfChoiceOrigins.shrink_to_fit();
+            return std::move(_dataOfChoiceOrigins);
+        }
+
+        void StateAndChoiceInformationBuilder::setBuildStatePlayerIndications(bool value) {
+            _buildStatePlayerIndications = value;
+        }
+
+        bool StateAndChoiceInformationBuilder::isBuildStatePlayerIndications() const {
+            return _buildStatePlayerIndications;
+        }
+
+        void StateAndChoiceInformationBuilder::addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex) {
+            STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+            STORM_LOG_ASSERT(_statePlayerIndications.size() <= stateIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
+            if (_statePlayerIndications.size() != stateIndex) {
+                _statePlayerIndications.resize(stateIndex, storm::storage::INVALID_PLAYER_INDEX);
+            }
+            _statePlayerIndications.push_back(player);
+        }
+
+        bool StateAndChoiceInformationBuilder::hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const {
+            STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+            return (stateIndex < _statePlayerIndications.size()) && (_statePlayerIndications[stateIndex] == expectedPlayer);
+        }
+
+        std::vector<storm::storage::PlayerIndex> StateAndChoiceInformationBuilder::buildStatePlayerIndications(uint_fast64_t totalNumberOfStates) {
+            STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+            _statePlayerIndications.resize(totalNumberOfStates, storm::storage::INVALID_PLAYER_INDEX);
+            _statePlayerIndications.shrink_to_fit();
+            return std::move(_statePlayerIndications);
+        }
+
+        void StateAndChoiceInformationBuilder::setBuildMarkovianStates(bool value) {
+            _buildMarkovianStates = value;
+        }
+
+        bool StateAndChoiceInformationBuilder::isBuildMarkovianStates() const {
+            return _buildMarkovianStates;
+        }
+
+        void StateAndChoiceInformationBuilder::addMarkovianState(uint_fast64_t markovianStateIndex) {
+            STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled.");
+            _markovianStates.grow(markovianStateIndex + 1, false);
+            _markovianStates.set(markovianStateIndex, true);
+        }
+
+        storm::storage::BitVector StateAndChoiceInformationBuilder::buildMarkovianStates(uint_fast64_t totalNumberOfStates) {
+            STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled.");
+            _markovianStates.resize(totalNumberOfStates, false);
+            return _markovianStates;
+        }
+
+        void StateAndChoiceInformationBuilder::setBuildStateValuations(bool value) {
+            _buildStateValuations = value;
+        }
+
+        bool StateAndChoiceInformationBuilder::isBuildStateValuations() const {
+            return _buildStateValuations;
+        }
+
+        storm::storage::sparse::StateValuationsBuilder& StateAndChoiceInformationBuilder::stateValuationsBuilder() {
+            STORM_LOG_ASSERT(_buildStateValuations, "Building StateValuations was not enabled.");
+            return _stateValuationsBuilder;
+        }
+
+    }
+}

src/storm/builder/StateAndChoiceInformationBuilder.h

@@ -0,0 +1,75 @@
+#pragma once
+
+#include <memory>
+#include <string>
+#include <unordered_map>
+#include <vector>
+#include <boost/any.hpp>
+
+#include "storm/models/sparse/ChoiceLabeling.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/PlayerIndex.h"
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
+#include "storm/storage/prism/Program.h"
+#include "storm/storage/sparse/StateValuations.h"
+
+
+namespace storm {
+    namespace builder {
+        
+        /*!
+         * This class collects information regarding the states and choices during model building.
+         * It is expected that the provided indices are in ascending order
+         */
+        class StateAndChoiceInformationBuilder {
+        public:
+            
+            StateAndChoiceInformationBuilder();
+
+            void setBuildChoiceLabels(bool value);
+            bool isBuildChoiceLabels() const;
+            void addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex);
+            storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
+
+            void setBuildChoiceOrigins(bool value);
+            bool isBuildChoiceOrigins() const;
+            void addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
+            std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
+            
+            void setBuildStatePlayerIndications(bool value);
+            bool isBuildStatePlayerIndications() const;
+            /*!
+             * @note: skipped choiceIndices get assigned the invalid player index.
+             */
+            void addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex);
+            bool hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const;
+            std::vector<storm::storage::PlayerIndex> buildStatePlayerIndications(uint_fast64_t totalNumberOfStates);
+            
+            void setBuildMarkovianStates(bool value);
+            bool isBuildMarkovianStates() const;
+            void addMarkovianState(uint_fast64_t markovianStateIndex);
+            storm::storage::BitVector buildMarkovianStates(uint_fast64_t  totalNumberOfStates);
+            
+            void setBuildStateValuations(bool value);
+            bool isBuildStateValuations() const;
+            storm::storage::sparse::StateValuationsBuilder& stateValuationsBuilder();
+            
+        private:
+            bool _buildChoiceLabels;
+            std::unordered_map<std::string, storm::storage::BitVector> _choiceLabels;
+            
+            bool _buildChoiceOrigins;
+            std::vector<boost::any> _dataOfChoiceOrigins;
+            
+            bool _buildStatePlayerIndications;
+            std::vector<storm::storage::PlayerIndex> _statePlayerIndications;
+            
+            bool _buildMarkovianStates;
+            storm::storage::BitVector _markovianStates;
+            
+            bool _buildStateValuations;
+            storm::storage::sparse::StateValuationsBuilder _stateValuationsBuilder;
+        };
+    }
+}
+    

src/storm/generator/Choice.cpp

@@ -3,7 +3,6 @@
 #include "storm/adapters/RationalFunctionAdapter.h"
 
 #include "storm/utility/constants.h"
-#include "storm/builder/ChoiceInformationBuilder.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"

src/storm/generator/NextStateGenerator.cpp

@@ -278,6 +278,11 @@ namespace storm {
             return classId;
         }
 
+        template<typename ValueType, typename StateType>
+        std::map<std::string, storm::storage::PlayerIndex> NextStateGenerator<ValueType, StateType>::getPlayerNameToIndexMap() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Generating player mappings is not supported for this model input format");
+        }
+        
         template<typename ValueType, typename StateType>
         void NextStateGenerator<ValueType, StateType>::remapStateIds(std::function<StateType(StateType const&)> const& remapping) {
             if (overlappingGuardStates != boost::none) {

src/storm/generator/NextStateGenerator.h

@@ -11,6 +11,7 @@
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/storage/sparse/ChoiceOrigins.h"
 #include "storm/storage/sparse/StateValuations.h"
+#include "storm/storage/PlayerIndex.h"
 
 #include "storm/builder/BuilderOptions.h"
 #include "storm/builder/RewardModelInformation.h"
@@ -74,6 +75,8 @@ namespace storm {
             std::string stateToString(CompressedState const& state) const;
 
             uint32_t observabilityClass(CompressedState const& state) const;
+            
+            virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const;
 
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
 

src/storm/generator/PrismNextStateGenerator.cpp

@@ -734,6 +734,11 @@ namespace storm {
             }
         }
 
+        template<typename ValueType, typename StateType>
+        std::map<std::string, storm::storage::PlayerIndex> PrismNextStateGenerator<ValueType, StateType>::getPlayerNameToIndexMap() const {
+            return program.getPlayerNameToIndexMapping();
+        }
+
         template<typename ValueType, typename StateType>
         storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
             // Gather a vector of labels and their expressions.

src/storm/generator/PrismNextStateGenerator.h

@@ -4,7 +4,6 @@
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/storage/prism/Program.h"
-#include "storm/storage/PlayerIndex.h"
 #include "storm/storage/BoostTypes.h"
 
 namespace storm {
@@ -43,7 +42,8 @@ namespace storm {
 
             virtual std::size_t getNumberOfRewardModels() const override;
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
-            
+            virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const override;
+
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
 
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;

src/storm/storage/sparse/ModelComponents.h

@@ -13,6 +13,7 @@
 #include "storm/storage/sparse/ChoiceOrigins.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/BitVector.h"
+#include "storm/storage/PlayerIndex.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 
 #include "storm/utility/macros.h"
@@ -30,9 +31,8 @@ namespace storm {
                                 std::unordered_map<std::string, RewardModelType> const& rewardModels =  std::unordered_map<std::string, RewardModelType>(),
                                 bool rateTransitions = false,
                                 boost::optional<storm::storage::BitVector> const& markovianStates = boost::none,
-                                boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none,
-                                boost::optional<std::vector<uint_fast32_t>> const& playerActionIndices = boost::none)
-                        : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) {
+                                boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none)
+                        : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) {
                     // Intentionally left empty
                 }
 
@@ -41,15 +41,12 @@ namespace storm {
                                 std::unordered_map<std::string, RewardModelType>&& rewardModels =  std::unordered_map<std::string, RewardModelType>(),
                                 bool rateTransitions = false,
                                 boost::optional<storm::storage::BitVector>&& markovianStates = boost::none,
-                                boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none,
-                                boost::optional<std::vector<uint_fast32_t>>&& playerActionIndices = boost::none)
-                        : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)), playerActionIndices(std::move(playerActionIndices)) {
+                                boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none)
+                        : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) {
                     // Intentionally left empty
                 }
 
 
-
-
                 // General components (applicable for all model types):
 
                 // The transition matrix.
@@ -68,7 +65,6 @@ namespace storm {
                 // POMDP specific components
                 // The POMDP observations
                 boost::optional<std::vector<uint32_t>> observabilityClasses;
-
                 boost::optional<storm::storage::sparse::StateValuations> observationValuations;
 
                 // Continuous time specific components (CTMCs, Markov Automata):
@@ -84,8 +80,10 @@ namespace storm {
                 boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> player1Matrix;
 
                 // Stochastic multiplayer game specific components:
-                // The vector mapping state choices to players
-                boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
+                // The vector mapping states to player indices.
+                boost::optional<std::vector<storm::storage::PlayerIndex>> statePlayerIndications;
+                // A mapping of player names to player indices.
+                boost::optional<std::map<std::string, storm::storage::PlayerIndex>> playerNameToIndexMap;
             };
         }
     }