sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

check if state is controlled by multiple players 

We do this by storing a list of modules/commands which have already been claimed by one player
main
Stefan Pranger 5 years ago
parent
e9a6077acb
commit
9bf2a572a7
2 changed files with 17 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/storm-parsers/parser/PrismParser.cpp
  2. 7
      src/storm-parsers/parser/PrismParser.h

12
src/storm-parsers/parser/PrismParser.cpp
View File

@ -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<std::string> const& moduleNames, std::vector<std::string> const & actionNames) const {
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;
@ -794,6 +794,11 @@ namespace storm {
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.");
}
@ -802,6 +807,11 @@ namespace storm {
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.");
}

7
src/storm-parsers/parser/PrismParser.h
View File

@ -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<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;
@ -368,7 +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) 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);

Write Preview
Loading…
Cancel
Save