diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index e039f6cbb..624dda819 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -786,7 +786,7 @@ namespace storm { 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 const& moduleNames, std::vector const & actionNames) const { + storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & actionNames) { if (this->secondRun) { std::map controlledModuleIndices; std::map controlledActionIndices; @@ -794,6 +794,11 @@ namespace storm { auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName); if (moduleIndexPair != globalProgramInformation.moduleToIndexMap.end()) { controlledModuleIndices.insert(std::pair(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."); } @@ -802,6 +807,11 @@ namespace storm { auto const& actionIndexPair = globalProgramInformation.actionIndices.find(actionName); if (actionIndexPair != globalProgramInformation.actionIndices.end()) { controlledActionIndices.insert(std::pair(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."); } diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 775b0b48b..9153f64bd 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -39,6 +39,8 @@ namespace storm { globalIntegerVariables.clear(); moduleToIndexMap.clear(); players.clear(); + playerControlledModules.clear(); + playerControlledCommands.clear(); modules.clear(); rewardModels.clear(); labels.clear(); @@ -65,6 +67,9 @@ namespace storm { std::vector observationLabels; std::vector players; + std::vector playerControlledModules; + std::vector playerControlledCommands; + bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; boost::optional systemCompositionConstruct; @@ -368,7 +373,7 @@ namespace storm { storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::ModuleRenaming createModuleRenaming(std::map 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 const& moduleNames, std::vector const & commandNames) const; + storm::prism::Player createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & commandNames); storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; void createObservablesList(std::vector const& observables);