Merge commit '6a71c19d8a5808b3a0c5be21f0966e8ada7f4252' into smg-merge

src/storm-parsers/parser/PrismParser.cpp

@@ -273,6 +273,22 @@ namespace storm {
             moduleDefinition = ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
             moduleDefinition.name("module definition");
 
+            freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshPlayerName, phoenix::ref(*this), qi::_1)];
+            freshPlayerName.name("fresh player name");
+
+            commandName = (qi::lit("[") >> identifier >> qi::lit("]"))[qi::_val = qi::_1];
+            commandName.name("command name");
+
+            moduleName = identifier[qi::_val = qi::_1];
+            moduleName.name("module name");
+
+            playerDefinition = (qi::lit("player") > freshPlayerName[qi::_a = qi::_1]
+                    > +(   (commandName[phoenix::push_back(qi::_c, qi::_1)]
+                        |   moduleName[phoenix::push_back(qi::_b, qi::_1)]) % ','
+                        )
+                    > qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParser::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
+            playerDefinition.name("player definition");
+
             moduleRenaming = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = phoenix::bind(&PrismParser::createModuleRenaming, phoenix::ref(*this), qi::_a)];
             moduleRenaming.name("Module renaming list");
 
@@ -286,6 +302,7 @@ namespace storm {
                      > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
                      > -observablesConstruct
                      >  *( definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
+                         | playerDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]
                          | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
                          | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
                          | globalVariableDefinition(phoenix::ref(globalProgramInformation))
@@ -473,6 +490,10 @@ namespace storm {
             return true;
         }
 
+        bool PrismParser::isFreshPlayerName(std::string const& playerName) {
+            return true;
+        }
+
         bool PrismParser::isOfBoolType(storm::expressions::Expression const& expression) {
             return !this->secondRun || expression.hasBooleanType();
         }
@@ -757,10 +778,51 @@ namespace storm {
         }
 
         storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
+            if (!this->secondRun) {
                 globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
+            } else {
+                STORM_LOG_THROW(globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), storm::exceptions::WrongFormatException, "Internal error while parsing: the index for module " << moduleName << " does not match the on in the first run.");
+            }
             return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
         }
 
+        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;
+                for(std::string moduleName : moduleNames) {
+                    auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
+                    if (moduleIndexPair != globalProgramInformation.moduleToIndexMap.end()) {
+                        controlledModuleIndices.insert(std::pair<std::string, uint_fast64_t>(moduleIndexPair->first, moduleIndexPair->second));
+                        if (std::find(globalProgramInformation.playerControlledModules.begin(), globalProgramInformation.playerControlledModules.end(), moduleName) != globalProgramInformation.playerControlledModules.end()) {
+                            STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName << "' already controlled by another player.");
+                        } else {
+                            globalProgramInformation.playerControlledModules.push_back(moduleName);
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
+                    }
+                }
+                for(std::string actionName : actionNames) {
+                    auto const& actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
+                    if (actionIndexPair != globalProgramInformation.actionIndices.end()) {
+                        controlledActionIndices.insert(std::pair<std::string, uint_fast64_t>(actionIndexPair->first, actionIndexPair->second));
+                        if (std::find(globalProgramInformation.playerControlledCommands.begin(), globalProgramInformation.playerControlledCommands.end(), actionName) != globalProgramInformation.playerControlledCommands.end()) {
+                            STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName << "' already controlled by another player.");
+                        } else {
+                            globalProgramInformation.playerControlledCommands.push_back(actionName);
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
+                    }
+                }
+                STORM_LOG_DEBUG("PLAYER created:" << playerName);
+                return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices);
+            } else {
+                return storm::prism::Player();
+            }
+        }
+
         bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const {
             if (!this->secondRun) {
                 auto const& renaming = moduleRenaming.getRenaming();
@@ -969,7 +1031,7 @@ namespace storm {
                 }
             }
 
-            return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
+            return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
         }
 
         void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {

src/storm-parsers/parser/PrismParser.h

@@ -38,6 +38,9 @@ namespace storm {
                 globalBooleanVariables.clear();
                 globalIntegerVariables.clear();
                 moduleToIndexMap.clear();
+                players.clear();
+                playerControlledModules.clear();
+                playerControlledCommands.clear();
                 modules.clear();
                 rewardModels.clear();
                 labels.clear();
@@ -62,6 +65,11 @@ namespace storm {
             std::vector<storm::prism::RewardModel> rewardModels;
             std::vector<storm::prism::Label> labels;
             std::vector<storm::prism::ObservationLabel> observationLabels;
+            std::vector<storm::prism::Player> players;
+
+            std::vector<std::string> playerControlledModules;
+            std::vector<std::string> playerControlledCommands;
+
             bool hasInitialConstruct;
             storm::prism::InitialConstruct initialConstruct;
             boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
@@ -101,7 +109,8 @@ namespace storm {
                     ("ctmdp", storm::prism::Program::ModelType::CTMDP)
                     ("ma", storm::prism::Program::ModelType::MA)
                     ("pomdp", storm::prism::Program::ModelType::POMDP)
-                    ("pta", storm::prism::Program::ModelType::PTA);
+                    ("pta", storm::prism::Program::ModelType::PTA)
+                    ("smg", storm::prism::Program::ModelType::SMG);
                 }
             };
 
@@ -131,7 +140,9 @@ namespace storm {
                     ("init", 21)
                     ("endinit", 22)
                     ("invariant", 23)
-                    ("endinvariant", 24);
+                    ("endinvariant", 24)
+                    ("smg", 25)
+                    ("endplayer", 26);
                 }
             };
 
@@ -260,6 +271,12 @@ namespace storm {
             qi::rule<Iterator, storm::prism::StateActionReward(GlobalProgramInformation&), Skipper> stateActionRewardDefinition;
             qi::rule<Iterator, storm::prism::TransitionReward(GlobalProgramInformation&), qi::locals<std::string, storm::expressions::Expression, storm::expressions::Expression,storm::expressions::Expression>, Skipper> transitionRewardDefinition;
 
+            // Rules for player definitions
+            qi::rule<Iterator, std::string(), Skipper> freshPlayerName;
+            qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> commandName;
+            qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> moduleName;
+            qi::rule<Iterator, storm::prism::Player(GlobalProgramInformation&), qi::locals<std::string, std::vector<std::string>, std::vector<std::string>>, Skipper> playerDefinition;
+
             // Rules for initial states expression.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
 
@@ -316,6 +333,7 @@ namespace storm {
             bool isFreshLabelName(std::string const& moduleName);
             bool isFreshObservationLabelName(std::string const& labelName);
             bool isFreshRewardModelName(std::string const& moduleName);
+            bool isFreshPlayerName(std::string const& playerName);
             bool isOfBoolType(storm::expressions::Expression const& expression);
             bool isOfIntType(storm::expressions::Expression const& expression);
             bool isOfNumericalType(storm::expressions::Expression const& expression);
@@ -355,6 +373,7 @@ namespace storm {
             storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::ModuleRenaming createModuleRenaming(std::map<std::string,std::string> const& renaming) const;
             storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::Player createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames, std::vector<std::string> const & commandNames);
             storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
             void createObservablesList(std::vector<std::string> const& observables);
 
@@ -368,4 +387,3 @@ namespace storm {
 } // namespace storm
 
 #endif	/* STORM_PARSER_PRISMPARSER_H_ */
-

src/storm/builder/ExplicitModelBuilder.cpp

@@ -80,6 +80,8 @@ namespace storm {
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents());
                 case storm::generator::ModelType::MA:
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents());
+                case storm::generator::ModelType::SMG:
+                    return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Smg, buildModelComponents());
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type.");
             }
@@ -118,7 +120,7 @@ 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<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
+        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) {
 
             // Create markovian states bit vector, if required.
             if (generator->getModelType() == storm::generator::ModelType::MA) {
@@ -126,6 +128,12 @@ namespace storm {
                 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);
+            }
+
             // Create a callback for the next-state generator to enable it to request the index of states.
             std::function<StateType (CompressedState const&)> stateToIdCallback = std::bind(&ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex, this, std::placeholders::_1);
 
@@ -201,6 +209,11 @@ namespace storm {
                             }
                         }
 
+                        if (playerActionIndices) {
+                            // TODO change this to storm::utility::infinity<ValueType>() ?
+                            playerActionIndices.get().push_back(-1);
+                        }
+
                         ++currentRow;
                         ++currentRowGroup;
                     } else {
@@ -255,6 +268,10 @@ namespace storm {
                         }
                         ++currentRow;
                     }
+
+                    if (playerActionIndices) {
+                        playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex());
+                    }
                     ++currentRowGroup;
                 }
 
@@ -286,6 +303,10 @@ namespace storm {
                 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) {
@@ -329,6 +350,7 @@ namespace storm {
             }
             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;
@@ -336,10 +358,10 @@ namespace storm {
                 stateValuationsBuilder = generator->initializeStateValuationsBuilder();
             }
 
-            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder);
+            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, playerActionIndices, stateValuationsBuilder);
 
             // 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));
+            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));
 
             // Now finalize all reward models.
             for (auto& rewardModelBuilder : rewardModelBuilders) {

src/storm/builder/ExplicitModelBuilder.h

@@ -131,7 +131,7 @@ namespace storm {
              * @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
              */
-            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
+            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);
 
             /*!
              * Explores the state space of the given program and returns the components of the model as a result.

src/storm/generator/Choice.cpp

@@ -92,6 +92,21 @@ namespace storm {
             return labels.get();
         }
 
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::setPlayerIndex(uint_fast32_t playerIndex) {
+            this->playerIndex = playerIndex;
+        }
+
+        template<typename ValueType, typename StateType>
+        bool Choice<ValueType, StateType>::hasPlayerIndex() const {
+            return playerIndex.is_initialized();
+        }
+
+        template<typename ValueType, typename StateType>
+        uint_fast32_t const& Choice<ValueType, StateType>::getPlayerIndex() const {
+            return playerIndex.get();
+        }
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addOriginData(boost::any const& data) {
             if (!this->originData || this->originData->empty()) {

src/storm/generator/Choice.h

@@ -91,6 +91,25 @@ namespace storm {
              */
             std::set<std::string> const& getLabels() const;
 
+            /*!
+             * Sets the players index
+             *
+             * @param The player index associated with this choice.
+             */
+            void setPlayerIndex(uint_fast32_t playerIndex);
+
+            /*!
+             * Returns whether there is an index for the player defined for this choice.
+             */
+            bool hasPlayerIndex() const;
+
+            /*!
+             * Retrieves the players index associated with this choice
+             *
+             * @return The player index associated with this choice.
+             */
+            uint_fast32_t const& getPlayerIndex() const;
+
             /*!
              * Adds the given data that specifies the origin of this choice w.r.t. the model specification
              */
@@ -176,6 +195,9 @@ namespace storm {
 
             // The labels of this choice
             boost::optional<std::set<std::string>> labels;
+
+            // The playerIndex of this choice
+            boost::optional<uint_fast32_t> playerIndex = boost::none;
         };
 
         template<typename ValueType, typename StateType>

src/storm/generator/NextStateGenerator.h

@@ -30,7 +30,8 @@ namespace storm {
             CTMC,
             MDP,
             MA,
-            POMDP
+            POMDP,
+            SMG
         };
 
         template<typename ValueType, typename StateType = uint32_t>

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>
@@ -127,6 +139,7 @@ namespace storm {
                 case storm::prism::Program::ModelType::MDP: return ModelType::MDP;
                 case storm::prism::Program::ModelType::MA: return ModelType::MA;
                 case storm::prism::Program::ModelType::POMDP: return ModelType::POMDP;
+                case storm::prism::Program::ModelType::SMG: return ModelType::SMG;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
             }
@@ -368,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));
@@ -583,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 << ").");
@@ -645,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

@@ -120,6 +120,10 @@ 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::map<uint_fast32_t, uint_fast32_t> moduleIndexToPlayerIndexMap;
+            std::map<uint_fast32_t, uint_fast32_t> commandIndexToPlayerIndexMap;
         };
 
     }

src/storm/models/ModelType.cpp

@@ -19,6 +19,8 @@ namespace storm {
                 return ModelType::S2pg;
             } else if (type == "POMDP") {
                 return ModelType::Pomdp;
+            } else if (type == "SMG") {
+                return ModelType::Smg;
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known.");
             }
@@ -44,6 +46,9 @@ namespace storm {
                 case ModelType::Pomdp:
                     os << "POMDP";
                     break;
+                case ModelType::Smg:
+                    os << "Smg";
+                    break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type.");
             }

src/storm/models/ModelType.h

@@ -7,7 +7,7 @@ namespace storm {
     namespace models {
         // All supported model types.
         enum class ModelType {
-            Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp
+            Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp, Smg
         };
 
         ModelType getModelType(std::string const& type);

src/storm/models/sparse/Model.cpp

@@ -62,12 +62,15 @@ namespace storm {
                     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).");
-                } else {
-                    STORM_LOG_THROW(this->isOfType(ModelType::S2pg), storm::exceptions::IllegalArgumentException, "Invalid model type.");
+                } else if (this->isOfType(ModelType::S2pg)) {
                     STORM_LOG_THROW(components.player1Matrix.is_initialized(), storm::exceptions::IllegalArgumentException, "No player 1 matrix given for stochastic game.");
                     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.");
                 }
 
                 // Branch on continuous/discrete timing

src/storm/models/sparse/Smg.cpp

@@ -0,0 +1,49 @@
+#include "storm/models/sparse/Smg.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/vector.h"
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+#include "storm/models/sparse/StandardRewardModel.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
+            }
+
+            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
+            }
+
+            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
+            }
+
+           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 class Smg<double>;
+            template class Smg<storm::RationalNumber>;
+
+            template class Smg<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+            template class Smg<storm::RationalFunction>;
+        } // namespace sparse
+    } // namespace models
+} // namespace storm

src/storm/models/sparse/Smg.h

@@ -0,0 +1,57 @@
+#ifndef STORM_MODELS_SPARSE_SMG_H_
+#define STORM_MODELS_SPARSE_SMG_H_
+
+#include "storm/models/sparse/NondeterministicModel.h"
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+
+            /*!
+             * This class represents a stochastic multiplayer game.
+             */
+            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(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;
+            };
+
+        } // namespace sparse
+    } // namespace models
+} // namespace storm
+
+#endif /* STORM_MODELS_SPARSE_SMG_H_ */

src/storm/storage/SymbolicModelDescription.cpp

@@ -65,6 +65,7 @@ namespace storm {
                     case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP;
                     case storm::prism::Program::ModelType::POMDP: return SymbolicModelDescription::ModelType::POMDP;
                     case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA;
+                    case storm::prism::Program::ModelType::SMG: return SymbolicModelDescription::ModelType::SMG;
                     default:
                         STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type.");
                 }

src/storm/storage/SymbolicModelDescription.h

@@ -11,7 +11,7 @@ namespace storm {
         class SymbolicModelDescription {
         public:
             enum class ModelType {
-                DTMC, CTMC, MDP, MA, POMDP
+                DTMC, CTMC, MDP, MA, POMDP, SMG
             };
 
             SymbolicModelDescription() = default;

src/storm/storage/prism/Player.cpp

@@ -0,0 +1,37 @@
+#include "storm/storage/prism/Player.h"
+
+namespace storm {
+    namespace prism {
+        Player::Player(std::string const& playerName, std::map<std::string, uint_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledCommands(controlledCommands) {
+            // Nothing to do here.
+        }
+
+        std::string const& Player::getName() const {
+            return this->playerName;
+        }
+
+        std::map<std::string, uint_fast32_t> const& Player::getModules() const {
+            return this->controlledModules;
+        }
+
+        std::map<std::string, uint_fast32_t> const& Player::getCommands() const {
+            return this->controlledCommands;
+        }
+
+        std::ostream& operator<<(std::ostream& stream, Player const& player) {
+            stream << "player";
+            if (player.getName() != "") {
+                stream << " " << player.getName();
+            }
+            stream << std::endl;
+            for (auto const& module : player.getModules()) {
+                stream << "\t" << module.first << std::endl;
+            }
+            for (auto const& command : player.getCommands()) {
+                stream << "\t[" << command.first << "]" << std::endl;
+            }
+            stream << "endplayer" << std::endl;
+            return stream;
+        }
+    } // namespace prism
+} // namespace storm

src/storm/storage/prism/Player.h

@@ -0,0 +1,72 @@
+#ifndef STORM_STORAGE_PRISM_PLAYER_H_
+#define STORM_STORAGE_PRISM_PLAYER_H_
+
+#include <string>
+#include <vector>
+
+#include "storm/storage/prism/Module.h"
+#include "storm/storage/prism/Command.h"
+
+// needed?
+#include "storm/storage/BoostTypes.h"
+#include "storm/utility/OsDetection.h"
+
+namespace storm {
+    namespace prism {
+        class Player : public LocatedInformation {
+        public:
+            /*!
+             * Creates a player with the given name, controlled modules and actions.
+             *
+             * @param playerName The name of the player.
+             * @param controlledModules The controlled modules.
+             * @param controlledCommands The controlled actions.
+             * @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_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename = "", uint_fast32_t lineNumber = 0);
+
+            // Create default implementations of constructors/assignment.
+            Player() = default;
+            Player(Player const& other) = default;
+            Player& operator=(Player const& other) = default;
+            Player(Player&& other) = default;
+            Player& operator=(Player&& other) = default;
+
+            /*!
+             * Retrieves the name of the player.
+             *
+             * @return The name of the player.
+             */
+            std::string const& getName() const;
+
+            /*!
+             * Retrieves all controlled Modules of the player.
+             *
+             * @return The modules controlled by the player.
+             */
+            std::map<std::string, uint_fast32_t> const& getModules() const; // TODO
+
+            /*!
+             * Retrieves all controlled Commands of the player.
+             *
+             * @return The commands controlled by the player.
+             */
+            std::map<std::string, uint_fast32_t> const& getCommands() const;
+
+            friend std::ostream& operator<<(std::ostream& stream, Player const& player);
+        private:
+            // The name of the player.
+            std::string playerName;
+
+            // The modules associated with this player.
+            std::map<std::string, uint_fast32_t> controlledModules;
+
+            // The commands associated with this player.
+            std::map<std::string, uint_fast32_t> controlledCommands;
+        };
+
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_PLAYER_H_ */

src/storm/storage/prism/Program.cpp

@@ -137,12 +137,12 @@ namespace storm {
             std::set<std::string> appearingModules;
         };
 
-        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
+        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
         : LocatedInformation(filename, lineNumber), manager(manager),
         modelType(modelType), constants(constants), constantToIndexMap(),
         globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
         globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
-        formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
+        formulas(formulas), formulaToIndexMap(), players(players), modules(modules), moduleToIndexMap(),
         rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
         labels(labels), labelToIndexMap(), observationLabels(observationLabels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
         synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
@@ -187,7 +187,7 @@ namespace storm {
         }
 
         bool Program::isDiscreteTimeModel() const {
-            return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP;
+            return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP || modelType == ModelType::SMG;
         }
 
         bool Program::isDeterministicModel() const {
@@ -479,6 +479,10 @@ namespace storm {
             return this->formulas;
         }
 
+        std::vector<Player> const& Program::getPlayers() const {
+            return this->players;
+        }
+
         std::size_t Program::getNumberOfFormulas() const {
             return this->getFormulas().size();
         }
@@ -487,6 +491,10 @@ namespace storm {
             return this->getModules().size();
         }
 
+        std::size_t Program::getNumberOfPlayers() const {
+            return this->getPlayers().size();
+        }
+
         storm::prism::Module const& Program::getModule(uint_fast64_t index) const {
             return this->modules[index];
         }
@@ -505,6 +513,10 @@ namespace storm {
             return this->modules;
         }
 
+        uint_fast32_t const& Program::getIndexOfPlayer(std::string playerName) const {
+            return this->playerToIndexMap.at(playerName);
+        }
+
         std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
             return actionToIndexMap;
         }
@@ -778,7 +790,7 @@ namespace storm {
                 newModules.push_back(module.restrictCommands(indexSet));
             }
 
-            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
 
         void Program::createMappings() {
@@ -801,6 +813,9 @@ namespace storm {
             for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
                 this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
             }
+            for (uint_fast64_t playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
+                this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
+            }
             for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
                 this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
             }
@@ -875,7 +890,7 @@ namespace storm {
                 }
             }
 
-            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
 
         Program Program::substituteConstants() const {
@@ -954,7 +969,7 @@ namespace storm {
                 newObservationLabels.emplace_back(label.substitute(substitution));
             }
 
-            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
 
         void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1512,7 +1527,7 @@ namespace storm {
                 newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
             }
 
-            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), 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(), this->getPlayers(), 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 {
@@ -1720,7 +1735,7 @@ namespace storm {
             // Finally, we can create the module and the program and return it.
             storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0);
 
-            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
+            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
         }
 
         std::vector<Constant> Program::usedConstants() const {
@@ -1935,6 +1950,7 @@ namespace storm {
                 case Program::ModelType::MA: out << "ma"; break;
                 case Program::ModelType::POMDP: out << "pomdp"; break;
                 case Program::ModelType::PTA: out << "pta"; break;
+                case Program::ModelType::SMG: out << "smg"; break;
             }
             return out;
         }
@@ -1946,6 +1962,10 @@ namespace storm {
             }
             stream << std::endl;
 
+            for (auto const& player : program.getPlayers()) {
+                stream << player << std::endl;
+            }
+
             for (auto const& variable : program.getGlobalBooleanVariables()) {
                 stream << "global " << variable << std::endl;
             }

src/storm/storage/prism/Program.h

@@ -15,6 +15,7 @@
 #include "storm/storage/prism/SystemCompositionConstruct.h"
 #include "storm/storage/prism/InitialConstruct.h"
 #include "storm/storage/prism/Composition.h"
+#include "storm/storage/prism/Player.h"
 #include "storm/storage/BoostTypes.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/OsDetection.h"
@@ -31,7 +32,7 @@ namespace storm {
             /*!
              * An enum for the different model types.
              */
-            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA};
+            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA, SMG};
 
             enum class ValidityCheckLevel  : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
 
@@ -57,7 +58,7 @@ namespace storm {
              * @param lineNumber The line number in which the program is defined.
              * @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
              */
-            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
+            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
 
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -318,6 +319,27 @@ namespace storm {
              */
             std::vector<Module> const& getModules() const;
 
+            /*!
+             * Retrieves the players of the program.
+             *
+             * @return The players of the program.
+             */
+            std::vector<Player> const& getPlayers() const;
+
+            /*!
+             * Retrieves the number of players in the program.
+             *
+             * @return The number of players in the program.
+             */
+            std::size_t getNumberOfPlayers() const;
+
+            /*!
+             * Retrieves the index of the player in the program.
+             *
+             * @return The index of the player in the program.
+             */
+            uint_fast32_t const& getIndexOfPlayer(std::string playerName) const;
+
             /*!
              * Retrieves the mapping of action names to their indices.
              *
@@ -741,6 +763,12 @@ namespace storm {
             // A mapping of module names to their indices.
             std::map<std::string, uint_fast64_t> moduleToIndexMap;
 
+            // The players associated with the program.
+            std::vector<Player> players;
+
+            // A mapping of player names to their indices.
+            std::map<std::string, uint_fast64_t> playerToIndexMap;
+
             // The reward models associated with the program.
             std::vector<RewardModel> rewardModels;
 

src/storm/storage/sparse/ModelComponents.h

@@ -30,8 +30,9 @@ 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)
-                        : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) {
+                                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) {
                     // Intentionally left empty
                 }
 
@@ -40,8 +41,9 @@ 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)
-                        : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) {
+                                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)) {
                     // Intentionally left empty
                 }
 
@@ -80,6 +82,10 @@ namespace storm {
                 // Stochastic two player game specific components:
                 // The matrix of player 1 choices (needed for stochastic two player games
                 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;
             };
         }
     }

src/storm/utility/builder.cpp

@@ -6,6 +6,7 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/Pomdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Smg.h"
 
 #include "storm/exceptions/InvalidModelException.h"
 
@@ -28,6 +29,8 @@ namespace storm {
                         return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
                     case storm::models::ModelType::S2pg:
                         return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components));
+                    case storm::models::ModelType::Smg:
+                        return std::make_shared<storm::models::sparse::Smg<ValueType, RewardModelType>>(std::move(components));
                 }
                 STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type");
             }