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

Polished parsing of Prism-SMGs, in particular 

* Fixed issues related to module renaming that resulted from setting the module indices already in the first run
  * Fixed a few uint_fast32_t vs uint_fast64_t issues, created alias PlayerIndex
main
Tim Quatmann 4 years ago
parent
81db530f70
commit
6fe76a009d
7 changed files with 119 additions and 107 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 102
      src/storm-parsers/parser/PrismParser.cpp
  2. 56
      src/storm-parsers/parser/PrismParser.h
  3. 2
      src/storm/generator/PrismNextStateGenerator.cpp
  4. 10
      src/storm/storage/prism/Player.cpp
  5. 25
      src/storm/storage/prism/Player.h
  6. 22
      src/storm/storage/prism/Program.cpp
  7. 9
      src/storm/storage/prism/Program.h

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

@ -191,7 +191,7 @@ namespace storm {
invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1]; invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
invariantConstruct.name("invariant construct"); invariantConstruct.name("invariant construct");
knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1)];
knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1, false)];
knownModuleName.name("existing module name"); knownModuleName.name("existing module name");
freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshModuleName, phoenix::ref(*this), qi::_1)]; freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshModuleName, phoenix::ref(*this), qi::_1)];
@ -276,18 +276,18 @@ namespace storm {
freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshPlayerName, phoenix::ref(*this), qi::_1)]; freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshPlayerName, phoenix::ref(*this), qi::_1)];
freshPlayerName.name("fresh player name"); freshPlayerName.name("fresh player name");
commandName = (qi::lit("[") >> identifier >> qi::lit("]"))[qi::_val = qi::_1];
commandName.name("command name");
playerControlledActionName = ((qi::lit("[") > identifier > qi::lit("]"))[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownActionName, phoenix::ref(*this), qi::_1, true)];
playerControlledActionName.name("player controlled action name");
moduleName = identifier[qi::_val = qi::_1];
moduleName.name("module name");
playerControlledModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1, true)];
playerControlledModuleName.name("player controlled 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)]) % ','
playerConstruct = (qi::lit("player") > freshPlayerName[qi::_a = qi::_1]
> +( (playerControlledActionName[phoenix::push_back(qi::_c, qi::_1)]
| playerControlledModuleName[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)]; > qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParser::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
playerDefinition.name("player definition");
playerConstruct.name("player construct");
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 = (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"); moduleRenaming.name("Module renaming list");
@ -302,7 +302,6 @@ namespace storm {
> modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
> -observablesConstruct > -observablesConstruct
> *( definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] > *( 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)] | 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)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| globalVariableDefinition(phoenix::ref(globalProgramInformation)) | globalVariableDefinition(phoenix::ref(globalProgramInformation))
@ -310,8 +309,9 @@ namespace storm {
| initialStatesConstruct(phoenix::ref(globalProgramInformation)) | initialStatesConstruct(phoenix::ref(globalProgramInformation))
| rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] | rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)]
| labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)]
| observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| playerConstruct(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]
) )
> -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]; > -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))];
start.name("probabilistic program"); start.name("probabilistic program");
@ -430,8 +430,8 @@ namespace storm {
return true; return true;
} }
bool PrismParser::isKnownModuleName(std::string const& moduleName) {
if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
bool PrismParser::isKnownModuleName(std::string const& moduleName, bool inSecondRun) {
if ((this->secondRun == inSecondRun) && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'."); STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'.");
return false; return false;
} }
@ -446,6 +446,14 @@ namespace storm {
return true; return true;
} }
bool PrismParser::isKnownActionName(std::string const& actionName, bool inSecondRun) {
if ((this->secondRun == inSecondRun) && this->globalProgramInformation.actionIndices.count(actionName) == 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown action label '" << actionName << "'.");
return false;
}
return true;
};
bool PrismParser::isFreshIdentifier(std::string const& identifier) { bool PrismParser::isFreshIdentifier(std::string const& identifier) {
if (!this->secondRun && this->manager->hasVariable(identifier)) { if (!this->secondRun && this->manager->hasVariable(identifier)) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'."); STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'.");
@ -777,52 +785,40 @@ namespace storm {
// We need this list to be filled in both runs. // We need this list to be filled in both runs.
} }
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) { storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames, std::vector<std::string> const & actionNames) {
if (this->secondRun) { if (this->secondRun) {
std::map<std::string, uint_fast64_t> controlledModuleIndices; std::map<std::string, uint_fast64_t> controlledModuleIndices;
std::map<std::string, uint_fast64_t> controlledActionIndices; 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(auto const& moduleName : moduleNames) {
auto moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
STORM_LOG_ASSERT(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
controlledModuleIndices.insert(*moduleIndexPair);
bool moduleNotYetControlled = globalProgramInformation.playerControlledModules.insert(moduleIndexPair->second).second;
STORM_LOG_THROW(moduleNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName << "' already controlled by another player.");
} }
for(std::string actionName : actionNames) { 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.");
}
auto actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
STORM_LOG_ASSERT(actionIndexPair != globalProgramInformation.actionIndices.end(), "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
controlledActionIndices.insert(*actionIndexPair);
bool actionNotYetControlled = globalProgramInformation.playerControlledActions.insert(actionIndexPair->second).second;
STORM_LOG_THROW(actionNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName << "' already controlled by another player.");
} }
STORM_LOG_DEBUG("PLAYER created:" << playerName);
return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices); return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices);
} else { } else {
return storm::prism::Player(); return storm::prism::Player();
} }
} }
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();
}
// Assert that the module name is already known and has the expected index.
STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap.count(moduleName) > 0, "Module name '" << moduleName << "' was not found.");
STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), "The index for module '" << moduleName << "' does not match the index from the first parsing run.");
return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
}
bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const { bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const {
if (!this->secondRun) { if (!this->secondRun) {
auto const& renaming = moduleRenaming.getRenaming(); auto const& renaming = moduleRenaming.getRenaming();
@ -867,9 +863,12 @@ namespace storm {
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename."); STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second]; storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
STORM_LOG_THROW(!moduleToRename.isRenamedFromModule(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": The module '" << newModuleName << "' can not be created from module '" << oldModuleName << "' through module renaming because '" << oldModuleName << "' is also a renamed module. Create '" << newModuleName << "' via a renaming from base module '" << moduleToRename.getBaseModule() << "' instead.");
auto const& renaming = moduleRenaming.getRenaming(); auto const& renaming = moduleRenaming.getRenaming();
if (!this->secondRun) { if (!this->secondRun) {
// Add a mapping from the new module name to its (future) index.
globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
// Register all (renamed) variables for later use. // Register all (renamed) variables for later use.
// We already checked before, whether the renaiming is valid. // We already checked before, whether the renaiming is valid.
for (auto const& variable : moduleToRename.getBooleanVariables()) { for (auto const& variable : moduleToRename.getBooleanVariables()) {
@ -918,9 +917,10 @@ namespace storm {
// Return a dummy module in the first pass. // Return a dummy module in the first pass.
return storm::prism::Module(); return storm::prism::Module();
} else { } else {
// Add a mapping from the new module name to its (future) index.
globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
// Assert that the module name is already known and has the expected index.
STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap.count(newModuleName) > 0, "Module name '" << newModuleName << "' was not found.");
STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap[newModuleName] == globalProgramInformation.modules.size(), "The index for module " << newModuleName << " does not match the index from the first parsing run.");
// Create a mapping from identifiers to the expressions they need to be replaced with. // Create a mapping from identifiers to the expressions they need to be replaced with.
std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming; std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
for (auto const& namePair : renaming) { for (auto const& namePair : renaming) {

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

@ -39,7 +39,7 @@ namespace storm {
globalIntegerVariables.clear(); globalIntegerVariables.clear();
players.clear(); players.clear();
playerControlledModules.clear(); playerControlledModules.clear();
playerControlledCommands.clear();
playerControlledActions.clear();
modules.clear(); modules.clear();
rewardModels.clear(); rewardModels.clear();
labels.clear(); labels.clear();
@ -65,9 +65,8 @@ namespace storm {
std::vector<storm::prism::Label> labels; std::vector<storm::prism::Label> labels;
std::vector<storm::prism::ObservationLabel> observationLabels; std::vector<storm::prism::ObservationLabel> observationLabels;
std::vector<storm::prism::Player> players; std::vector<storm::prism::Player> players;
std::vector<std::string> playerControlledModules;
std::vector<std::string> playerControlledCommands;
std::set<uint_fast64_t> playerControlledModules;
std::set<uint_fast64_t> playerControlledActions;
bool hasInitialConstruct; bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct; storm::prism::InitialConstruct initialConstruct;
@ -123,25 +122,26 @@ namespace storm {
("ma", 5) ("ma", 5)
("pomdp", 6) ("pomdp", 6)
("pta", 7) ("pta", 7)
("const", 8)
("int", 9)
("bool", 10)
("module", 11)
("endmodule", 12)
("rewards", 13)
("endrewards", 14)
("true", 15)
("false", 16)
("min", 17)
("max", 18)
("floor", 19)
("ceil", 20)
("init", 21)
("endinit", 22)
("invariant", 23)
("endinvariant", 24)
("smg", 25)
("endplayer", 26);
("smg", 8)
("const", 9)
("int", 10)
("bool", 11)
("module", 12)
("endmodule", 13)
("rewards", 14)
("endrewards", 15)
("true", 16)
("false", 17)
("min", 18)
("max", 19)
("floor", 20)
("ceil", 21)
("init", 22)
("endinit", 23)
("invariant", 24)
("endinvariant", 25)
("player", 26)
("endplayer", 27);
} }
}; };
@ -262,6 +262,7 @@ namespace storm {
qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition; qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition;
qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList; qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;
qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition; qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
qi::rule<Iterator, std::string(), Skipper> knownActionName;
// Rules for reward definitions. // Rules for reward definitions.
qi::rule<Iterator, std::string(), Skipper> freshRewardModelName; qi::rule<Iterator, std::string(), Skipper> freshRewardModelName;
@ -272,9 +273,9 @@ namespace storm {
// Rules for player definitions // Rules for player definitions
qi::rule<Iterator, std::string(), Skipper> freshPlayerName; 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;
qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> playerControlledActionName;
qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> playerControlledModuleName;
qi::rule<Iterator, storm::prism::Player(GlobalProgramInformation&), qi::locals<std::string, std::vector<std::string>, std::vector<std::string>>, Skipper> playerConstruct;
// Rules for initial states expression. // Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct; qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
@ -327,8 +328,9 @@ namespace storm {
// Helper methods used in the grammar. // Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier); bool isValidIdentifier(std::string const& identifier);
bool isFreshIdentifier(std::string const& identifier); bool isFreshIdentifier(std::string const& identifier);
bool isKnownModuleName(std::string const& moduleName);
bool isKnownModuleName(std::string const& moduleName, bool inSecondRun);
bool isFreshModuleName(std::string const& moduleName); bool isFreshModuleName(std::string const& moduleName);
bool isKnownActionName(std::string const& actionName, bool inSecondRun);
bool isFreshLabelName(std::string const& moduleName); bool isFreshLabelName(std::string const& moduleName);
bool isFreshObservationLabelName(std::string const& labelName); bool isFreshObservationLabelName(std::string const& labelName);
bool isFreshRewardModelName(std::string const& moduleName); bool isFreshRewardModelName(std::string const& moduleName);

2
src/storm/generator/PrismNextStateGenerator.cpp
View File

@ -87,7 +87,7 @@ namespace storm {
for (auto const& moduleIndexPair : player.getModules()) { for (auto const& moduleIndexPair : player.getModules()) {
moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex; moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex;
} }
for (auto const& commandIndexPair : player.getCommands()) {
for (auto const& commandIndexPair : player.getActions()) {
commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex; commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex;
} }
} }

10
src/storm/storage/prism/Player.cpp
View File

@ -2,7 +2,7 @@
namespace storm { namespace storm {
namespace prism { 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) {
Player::Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> const& controlledActions, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledActions(controlledActions) {
// Nothing to do here. // Nothing to do here.
} }
@ -10,12 +10,12 @@ namespace storm {
return this->playerName; return this->playerName;
} }
std::map<std::string, uint_fast32_t> const& Player::getModules() const {
std::map<std::string, uint_fast64_t> const& Player::getModules() const {
return this->controlledModules; return this->controlledModules;
} }
std::map<std::string, uint_fast32_t> const& Player::getCommands() const {
return this->controlledCommands;
std::map<std::string, uint_fast64_t> const& Player::getActions() const {
return this->controlledActions;
} }
std::ostream& operator<<(std::ostream& stream, Player const& player) { std::ostream& operator<<(std::ostream& stream, Player const& player) {
@ -27,7 +27,7 @@ namespace storm {
for (auto const& module : player.getModules()) { for (auto const& module : player.getModules()) {
stream << "\t" << module.first << std::endl; stream << "\t" << module.first << std::endl;
} }
for (auto const& command : player.getCommands()) {
for (auto const& command : player.getActions()) {
stream << "\t[" << command.first << "]" << std::endl; stream << "\t[" << command.first << "]" << std::endl;
} }
stream << "endplayer" << std::endl; stream << "endplayer" << std::endl;

25
src/storm/storage/prism/Player.h
View File

@ -1,5 +1,4 @@
#ifndef STORM_STORAGE_PRISM_PLAYER_H_
#define STORM_STORAGE_PRISM_PLAYER_H_
#pragma once
#include <string> #include <string>
#include <vector> #include <vector>
@ -13,6 +12,9 @@
namespace storm { namespace storm {
namespace prism { namespace prism {
typedef uint_fast64_t PlayerIndex;
class Player : public LocatedInformation { class Player : public LocatedInformation {
public: public:
/*! /*!
@ -20,11 +22,11 @@ namespace storm {
* *
* @param playerName The name of the player. * @param playerName The name of the player.
* @param controlledModules The controlled modules. * @param controlledModules The controlled modules.
* @param controlledCommands The controlled actions.
* @param controlledActions The controlled actions.
* @param filename The filename in which the player is defined. * @param filename The filename in which the player is defined.
* @param lineNumber The line number 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);
Player(std::string const& playerName, std::map<std::string, uint_fast64_t> const& controlledModules, std::map<std::string, uint_fast64_t> const& controlledActions, std::string const& filename = "", uint_fast32_t lineNumber = 0);
// Create default implementations of constructors/assignment. // Create default implementations of constructors/assignment.
Player() = default; Player() = default;
@ -45,14 +47,14 @@ namespace storm {
* *
* @return The modules controlled by the player. * @return The modules controlled by the player.
*/ */
std::map<std::string, uint_fast32_t> const& getModules() const; // TODO
std::map<std::string, uint_fast64_t> const& getModules() const; // TODO
/*! /*!
* Retrieves all controlled Commands of the player.
* Retrieves all controlled Actions of the player.
* *
* @return The commands controlled by the player.
* @return The Actions controlled by the player.
*/ */
std::map<std::string, uint_fast32_t> const& getCommands() const;
std::map<std::string, uint_fast64_t> const& getActions() const;
friend std::ostream& operator<<(std::ostream& stream, Player const& player); friend std::ostream& operator<<(std::ostream& stream, Player const& player);
private: private:
@ -60,13 +62,12 @@ namespace storm {
std::string playerName; std::string playerName;
// The modules associated with this player. // The modules associated with this player.
std::map<std::string, uint_fast32_t> controlledModules;
std::map<std::string, uint_fast64_t> controlledModules;
// The commands associated with this player.
std::map<std::string, uint_fast32_t> controlledCommands;
// The Actions associated with this player.
std::map<std::string, uint_fast64_t> controlledActions;
}; };
} // namespace prism } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_STORAGE_PRISM_PLAYER_H_ */

22
src/storm/storage/prism/Program.cpp
View File

@ -483,6 +483,18 @@ namespace storm {
return this->players; return this->players;
} }
std::size_t Program::getNumberOfPlayers() const {
return this->getPlayers().size();
}
PlayerIndex const& Program::getIndexOfPlayer(std::string const& playerName) const {
return this->playerToIndexMap.at(playerName);
}
std::map<std::string, PlayerIndex> const& Program::getPlayerNameToIndexMapping() const {
return playerToIndexMap;
}
std::size_t Program::getNumberOfFormulas() const { std::size_t Program::getNumberOfFormulas() const {
return this->getFormulas().size(); return this->getFormulas().size();
} }
@ -491,10 +503,6 @@ namespace storm {
return this->getModules().size(); 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 { storm::prism::Module const& Program::getModule(uint_fast64_t index) const {
return this->modules[index]; return this->modules[index];
} }
@ -513,10 +521,6 @@ namespace storm {
return this->modules; 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 { std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
return actionToIndexMap; return actionToIndexMap;
} }
@ -813,7 +817,7 @@ namespace storm {
for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex; this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
} }
for (uint_fast64_t playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
for (PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex; this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
} }
for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) { for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {

9
src/storm/storage/prism/Program.h
View File

@ -338,8 +338,13 @@ namespace storm {
* *
* @return 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;
PlayerIndex const& getIndexOfPlayer(std::string const& playerName) const;
/*!
* @return Retrieves the mapping of player names to their indices.
*/
std::map<std::string, PlayerIndex> const& getPlayerNameToIndexMapping() const;
/*! /*!
* Retrieves the mapping of action names to their indices. * Retrieves the mapping of action names to their indices.
* *
@ -761,7 +766,7 @@ namespace storm {
std::vector<Player> players; std::vector<Player> players;
// A mapping of player names to their indices. // A mapping of player names to their indices.
std::map<std::string, uint_fast64_t> playerToIndexMap;
std::map<std::string, PlayerIndex> playerToIndexMap;
// The modules associated with the program. // The modules associated with the program.
std::vector<Module> modules; std::vector<Module> modules;

Write Preview
Loading…
Cancel
Save