From 6fe76a009d41dbb53c882c1d258c6c4baf93d93c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 12 Jan 2021 07:09:18 +0100
Subject: [PATCH] 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
---
src/storm-parsers/parser/PrismParser.cpp | 102 +++++++++---------
src/storm-parsers/parser/PrismParser.h | 56 +++++-----
.../generator/PrismNextStateGenerator.cpp | 2 +-
src/storm/storage/prism/Player.cpp | 10 +-
src/storm/storage/prism/Player.h | 25 ++---
src/storm/storage/prism/Program.cpp | 22 ++--
src/storm/storage/prism/Program.h | 9 +-
7 files changed, 119 insertions(+), 107 deletions(-)
diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp
index 624dda819..ba67e1ce3 100644
--- a/src/storm-parsers/parser/PrismParser.cpp
+++ b/src/storm-parsers/parser/PrismParser.cpp
@@ -191,7 +191,7 @@ namespace storm {
invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
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");
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.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)];
- 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.name("Module renaming list");
@@ -302,7 +302,6 @@ 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))
@@ -310,8 +309,9 @@ namespace storm {
| initialStatesConstruct(phoenix::ref(globalProgramInformation))
| 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)]
- | 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))];
start.name("probabilistic program");
@@ -430,8 +430,8 @@ namespace storm {
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 << "'.");
return false;
}
@@ -446,6 +446,14 @@ namespace storm {
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) {
if (!this->secondRun && this->manager->hasVariable(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.
}
- 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(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) {
- 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);
} else {
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 {
if (!this->secondRun) {
auto const& renaming = moduleRenaming.getRenaming();
@@ -867,9 +863,12 @@ namespace storm {
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::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();
-
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.
// We already checked before, whether the renaiming is valid.
for (auto const& variable : moduleToRename.getBooleanVariables()) {
@@ -918,9 +917,10 @@ namespace storm {
// Return a dummy module in the first pass.
return storm::prism::Module();
} 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.
std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
for (auto const& namePair : renaming) {
diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h
index c86e75324..2a1d5beeb 100644
--- a/src/storm-parsers/parser/PrismParser.h
+++ b/src/storm-parsers/parser/PrismParser.h
@@ -39,7 +39,7 @@ namespace storm {
globalIntegerVariables.clear();
players.clear();
playerControlledModules.clear();
- playerControlledCommands.clear();
+ playerControlledActions.clear();
modules.clear();
rewardModels.clear();
labels.clear();
@@ -65,9 +65,8 @@ namespace storm {
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;
+ std::set<uint_fast64_t> playerControlledModules;
+ std::set<uint_fast64_t> playerControlledActions;
bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct;
@@ -123,25 +122,26 @@ namespace storm {
("ma", 5)
("pomdp", 6)
("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, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;
qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
+ qi::rule<Iterator, std::string(), Skipper> knownActionName;
// Rules for reward definitions.
qi::rule<Iterator, std::string(), Skipper> freshRewardModelName;
@@ -272,9 +273,9 @@ namespace storm {
// 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;
+ 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.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
@@ -327,8 +328,9 @@ namespace storm {
// Helper methods used in the grammar.
bool isValidIdentifier(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 isKnownActionName(std::string const& actionName, bool inSecondRun);
bool isFreshLabelName(std::string const& moduleName);
bool isFreshObservationLabelName(std::string const& labelName);
bool isFreshRewardModelName(std::string const& moduleName);
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index 03b4975a6..bcadbe7ee 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -87,7 +87,7 @@ namespace storm {
for (auto const& moduleIndexPair : player.getModules()) {
moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex;
}
- for (auto const& commandIndexPair : player.getCommands()) {
+ for (auto const& commandIndexPair : player.getActions()) {
commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex;
}
}
diff --git a/src/storm/storage/prism/Player.cpp b/src/storm/storage/prism/Player.cpp
index f2e30d3ad..02c2117cf 100644
--- a/src/storm/storage/prism/Player.cpp
+++ b/src/storm/storage/prism/Player.cpp
@@ -2,7 +2,7 @@
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) {
+ 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.
}
@@ -10,12 +10,12 @@ namespace storm {
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;
}
- 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) {
@@ -27,7 +27,7 @@ namespace storm {
for (auto const& module : player.getModules()) {
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 << "endplayer" << std::endl;
diff --git a/src/storm/storage/prism/Player.h b/src/storm/storage/prism/Player.h
index 7d9437f7f..92a79b3bd 100644
--- a/src/storm/storage/prism/Player.h
+++ b/src/storm/storage/prism/Player.h
@@ -1,5 +1,4 @@
-#ifndef STORM_STORAGE_PRISM_PLAYER_H_
-#define STORM_STORAGE_PRISM_PLAYER_H_
+#pragma once
#include <string>
#include <vector>
@@ -13,6 +12,9 @@
namespace storm {
namespace prism {
+
+ typedef uint_fast64_t PlayerIndex;
+
class Player : public LocatedInformation {
public:
/*!
@@ -20,11 +22,11 @@ namespace storm {
*
* @param playerName The name of the player.
* @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 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.
Player() = default;
@@ -45,14 +47,14 @@ namespace storm {
*
* @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);
private:
@@ -60,13 +62,12 @@ namespace storm {
std::string playerName;
// 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 storm
-#endif /* STORM_STORAGE_PRISM_PLAYER_H_ */
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index 3acef442e..9599766ff 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -483,6 +483,18 @@ namespace storm {
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 {
return this->getFormulas().size();
}
@@ -491,10 +503,6 @@ 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];
}
@@ -513,10 +521,6 @@ 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;
}
@@ -813,7 +817,7 @@ 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) {
+ for (PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
}
for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index 56610556f..af25c4d47 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -338,8 +338,13 @@ namespace storm {
*
* @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.
*
@@ -761,7 +766,7 @@ namespace storm {
std::vector<Player> players;
// 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.
std::vector<Module> modules;