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

Replaced action names by indices in PRISM programs. 

Former-commit-id: e66820c247
tempestpy_adaptions
dehnert 10 years ago
parent
3260a6203c
commit
ab0caf79e8
10 changed files with 136 additions and 106 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. 16
      src/adapters/ExplicitModelAdapter.h
  2. 14
      src/parser/PrismParser.cpp
  3. 6
      src/parser/PrismParser.h
  4. 45
      src/storage/prism/Module.cpp
  5. 32
      src/storage/prism/Module.h
  6. 42
      src/storage/prism/Program.cpp
  7. 34
      src/storage/prism/Program.h
  8. 14
      src/storage/prism/TransitionReward.cpp
  9. 25
      src/storage/prism/TransitionReward.h
  10. 14
      src/utility/PrismUtility.h

16
src/adapters/ExplicitModelAdapter.h
View File

@ -233,7 +233,7 @@ namespace storm {
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
static boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) {
static boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>()));
// Iterate over all modules.
@ -288,14 +288,14 @@ namespace storm {
storm::prism::Command const& command = module.getCommand(j);
// Only consider unlabeled commands.
if (!command.isLabeled()) continue;
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!command.getGuardExpression().evaluateAsBool(currentState)) {
continue;
}
result.push_back(Choice<ValueType>(""));
result.push_back(Choice<ValueType>());
Choice<ValueType>& choice = result.back();
choice.addChoiceLabel(command.getGlobalIndex());
@ -331,9 +331,9 @@ namespace storm {
static std::list<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
std::list<Choice<ValueType>> result;
for (std::string const& action : program.getActions()) {
for (uint_fast64_t actionIndex : program.getActionIndices()) {
StateType const* currentState = stateInformation.reachableStates[stateIndex];
boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action);
boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, currentState, actionIndex);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
@ -401,7 +401,7 @@ namespace storm {
// At this point, we applied all commands of the current command combination and newTargetStates
// contains all target states and their respective probabilities. That means we are now ready to
// add the choice to the list of transitions.
result.push_back(Choice<ValueType>(action));
result.push_back(Choice<ValueType>(actionIndex));
// Now create the actual distribution.
Choice<ValueType>& choice = result.back();
@ -526,7 +526,7 @@ namespace storm {
// Then, based on whether the model is deterministic or not, either add the choices individually
// or compose them to one choice.
if (deterministicModel) {
Choice<ValueType> globalChoice("");
Choice<ValueType> globalChoice;
std::map<uint_fast64_t, ValueType> stateToRewardMap;
boost::container::flat_set<uint_fast64_t> allChoiceLabels;
@ -538,7 +538,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
if (!transitionReward.empty() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
}
}

14
src/parser/PrismParser.cpp
View File

@ -111,12 +111,12 @@ namespace storm {
stateRewardDefinition = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
transitionRewardDefinition.name("transition reward definition");
rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\""))
> +( stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
| transitionRewardDefinition[phoenix::push_back(qi::_c, qi::_1)]
| transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_c, qi::_1)]
)
>> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
rewardModelDefinition.name("reward model definition");
@ -161,7 +161,7 @@ namespace storm {
| globalVariableDefinition(qi::_a)
| (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)]
| initialStatesConstruct(qi::_a)
| rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)]
| rewardModelDefinition(qi::_a)[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)]
| labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
)
@ -340,8 +340,10 @@ namespace storm {
return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename());
}
storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const {
return storm::prism::TransitionReward(actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'.");
return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
}
storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
@ -502,7 +504,7 @@ namespace storm {
}
storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
}
} // namespace parser
} // namespace storm

6
src/parser/PrismParser.h
View File

@ -193,9 +193,9 @@ namespace storm {
qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
// Rules for reward definitions.
qi::rule<Iterator, storm::prism::RewardModel(), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::RewardModel(GlobalProgramInformation&), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(GlobalProgramInformation&), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
@ -232,7 +232,7 @@ namespace storm {
storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const;
storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const;
storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;

45
src/storage/prism/Module.cpp
View File

@ -10,11 +10,11 @@ namespace storm {
// Intentionally left empty.
}
Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionIndices(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
// Initialize the internal mappings for fast information retrieval.
this->createMappings();
}
std::size_t Module::getNumberOfBooleanVariables() const {
return this->booleanVariables.size();
}
@ -32,7 +32,7 @@ namespace storm {
std::vector<storm::prism::BooleanVariable> const& Module::getBooleanVariables() const {
return this->booleanVariables;
}
storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName);
STORM_LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'.");
@ -67,16 +67,11 @@ namespace storm {
return this->moduleName;
}
std::set<std::string> const& Module::getActions() const {
return this->actions;
std::set<uint_fast64_t> const& Module::getActionIndices() const {
return this->actionIndices;
}
bool Module::hasAction(std::string const& action) const {
auto const& actionEntry = this->actions.find(action);
return actionEntry != this->actions.end();
}
bool Module::hasActionIndex(uint_fast64_t const& actionIndex) const {
bool Module::hasActionIndex(uint_fast64_t actionIndex) const {
return this->actionIndices.find(actionIndex) != this->actionIndices.end();
}
@ -94,15 +89,6 @@ namespace storm {
return this->renaming;
}
std::set<uint_fast64_t> const& Module::getCommandIndicesByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
return actionsCommandSetPair->second;
}
STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
}
std::set<uint_fast64_t> const& Module::getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const {
auto actionIndicesCommandSetPair = this->actionIndicesToCommandIndexMap.find(actionIndex);
if (actionIndicesCommandSetPair != this->actionIndicesToCommandIndexMap.end()) {
@ -114,7 +100,6 @@ namespace storm {
void Module::createMappings() {
// Clear the current mappings.
this->actionsToCommandIndexMap.clear();
this->actionIndicesToCommandIndexMap.clear();
this->booleanVariableToIndexMap.clear();
this->integerVariableToIndexMap.clear();
@ -129,30 +114,18 @@ namespace storm {
// Add the mapping for all commands.
for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
std::string const& action = this->commands[i].getActionName();
uint_fast64_t actionIndex = this->commands[i].getActionIndex();
if (action != "") {
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>());
}
if (this->commands[i].isLabeled()) {
uint_fast64_t actionIndex = this->commands[i].getActionIndex();
if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set<uint_fast64_t>());
}
this->actionsToCommandIndexMap[action].insert(i);
this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
this->actions.insert(action);
this->actionIndices.insert(this->commands[i].getActionIndex());
this->actionIndices.insert(actionIndex);
}
}
// For all actions that are "in the module", but for which no command exists, we add the mapping to an empty
// set of commands.
for (auto const& action : this->actions) {
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
this->actionsToCommandIndexMap[action] = std::set<uint_fast64_t>();
}
}
for (auto const& actionIndex : this->actionIndices) {
if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
this->actionIndicesToCommandIndexMap[actionIndex] = std::set<uint_fast64_t>();

32
src/storage/prism/Module.h
View File

@ -135,27 +135,19 @@ namespace storm {
std::string const& getName() const;
/*!
* Retrieves the set of actions present in this module.
* Retrieves the set of action indices present in this module.
*
* @return the set of actions present in this module.
* @return the set of action indices present in this module.
*/
std::set<std::string> const& getActions() const;
std::set<uint_fast64_t> const& getActionIndices() const;
/*!
* Retrieves whether or not this module contains a command labeled with the given action.
*
* @param action The action name to look for in this module.
* @return True iff the module has at least one command labeled with the given action.
*/
bool hasAction(std::string const& action) const;
/*!
* Retrieves whether or not this module contains a command labeled with the given action index.
*
* @param action The action name to look for in this module.
* @param actionIndex The index of the action to look for in this module.
* @return True iff the module has at least one command labeled with the given action index.
*/
bool hasActionIndex(uint_fast64_t const& actionIndex) const;
bool hasActionIndex(uint_fast64_t actionIndex) const;
/*!
* Retrieves whether this module was created from another module via renaming.
@ -180,14 +172,6 @@ namespace storm {
*/
std::map<std::string, std::string> const& getRenaming() const;
/*!
* Retrieves the indices of all commands within this module that are labelled by the given action.
*
* @param action The action with which the commands have to be labelled.
* @return A set of indices of commands that are labelled with the given action.
*/
std::set<uint_fast64_t> const& getCommandIndicesByAction(std::string const& action) const;
/*!
* Retrieves the indices of all commands within this module that are labelled by the given action.
*
@ -238,15 +222,9 @@ namespace storm {
// The commands associated with the module.
std::vector<storm::prism::Command> commands;
// The set of actions present in this module.
std::set<std::string> actions;
// The set of action indices present in this module.
std::set<uint_fast64_t> actionIndices;
// A map of actions to the set of commands labeled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
// A map of actions to the set of commands labeled with this action.
std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;

42
src/storage/prism/Program.cpp
View File

@ -11,7 +11,7 @@
namespace storm {
namespace prism {
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::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
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, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
this->createMappings();
// Create a new initial construct if the corresponding flag was set.
@ -124,6 +124,10 @@ namespace storm {
return this->modules;
}
std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
return actionToIndexMap;
}
storm::prism::InitialConstruct const& Program::getInitialConstruct() const {
return this->initialConstruct;
}
@ -132,9 +136,19 @@ namespace storm {
return this->actions;
}
std::set<uint_fast64_t> const& Program::getActionIndices() const {
return this->actionIndices;
}
std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
auto const& actionModuleSetPair = this->actionsToModuleIndexMap.find(action);
STORM_LOG_THROW(actionModuleSetPair != this->actionsToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
auto const& nameIndexPair = this->actionToIndexMap.find(action);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
return this->getModuleIndicesByActionIndex(nameIndexPair->second);
}
std::set<uint_fast64_t> const& Program::getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const {
auto const& actionModuleSetPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
STORM_LOG_THROW(actionModuleSetPair != this->actionIndicesToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << actionIndex << "' does not exist.");
return actionModuleSetPair->second;
}
@ -188,7 +202,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->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
}
void Program::createMappings() {
@ -215,17 +229,21 @@ namespace storm {
this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex;
}
for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
this->actions.insert(actionIndexPair.first);
this->actionIndices.insert(actionIndexPair.second);
}
// Build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
Module const& module = this->getModule(moduleIndex);
for (auto const& action : module.getActions()) {
auto const& actionModuleIndicesPair = this->actionsToModuleIndexMap.find(action);
if (actionModuleIndicesPair == this->actionsToModuleIndexMap.end()) {
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
for (auto const& actionIndex : module.getActionIndices()) {
auto const& actionModuleIndicesPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
if (actionModuleIndicesPair == this->actionIndicesToModuleIndexMap.end()) {
this->actionIndicesToModuleIndexMap[actionIndex] = std::set<uint_fast64_t>();
}
this->actionsToModuleIndexMap[action].insert(moduleIndex);
this->actions.insert(action);
this->actionIndicesToModuleIndexMap[actionIndex].insert(moduleIndex);
}
// Put in the appropriate entries for the mapping from variable names to module index.
@ -279,7 +297,7 @@ namespace storm {
STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
}
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
}
Program Program::substituteConstants() const {
@ -338,7 +356,7 @@ namespace storm {
newLabels.emplace_back(label.substitute(constantSubstitution));
}
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, false, newInitialConstruct, newLabels);
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, false, newInitialConstruct, newLabels);
}
void Program::checkValidity() const {

34
src/storage/prism/Program.h
View File

@ -35,6 +35,7 @@ namespace storm {
* @param globalIntegerVariables The global integer variables of the program.
* @param formulas The formulas defined in the program.
* @param modules The modules of the program.
* @param actionToIndexMap A mapping of action names to their indices.
* @param fixInitialConstruct A flag that indicates whether the given initial construct is to be ignored and
* replaced by a new one created from the initial values of the variables.
* @param initialConstruct The initial construct of the program. If the initial construct specifies "false"
@ -46,7 +47,7 @@ namespace storm {
* @param lineNumber The line number in which the program is defined.
* @param checkValidity If set to true, the program is checked for validity.
*/
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::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool checkValidity = 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<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool checkValidity = true);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -189,6 +190,13 @@ namespace storm {
*/
std::vector<Module> const& getModules() const;
/*!
* Retrieves the mapping of action names to their indices.
*
* @return The mapping of action names to their indices.
*/
std::map<std::string, uint_fast64_t> const& getActionNameToIndexMapping() const;
/*!
* Retrieves the initial construct of the program.
*
@ -203,6 +211,13 @@ namespace storm {
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the set of action indices present in the program.
*
* @return The set of action indices present in the program.
*/
std::set<uint_fast64_t> const& getActionIndices() const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the
* given action.
@ -211,6 +226,15 @@ namespace storm {
* @return A set of indices of all matching modules.
*/
std::set<uint_fast64_t> const& getModuleIndicesByAction(std::string const& action) const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the
* given action index.
*
* @param actionIndex The index of the action the modules are supposed to possess.
* @return A set of indices of all matching modules.
*/
std::set<uint_fast64_t> const& getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const;
/*!
* Retrieves the index of the module in which the given variable name was declared.
@ -381,11 +405,17 @@ namespace storm {
// A mapping from label names to their corresponding indices.
std::map<std::string, uint_fast64_t> labelToIndexMap;
// A mapping from action names to their indices.
std::map<std::string, uint_fast64_t> actionToIndexMap;
// The set of actions present in this program.
std::set<std::string> actions;
// The set of actions present in this program.
std::set<uint_fast64_t> actionIndices;
// A map of actions to the set of modules containing commands labelled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToModuleIndexMap;
// A mapping from variable names to the modules in which they were declared.
std::map<std::string, uint_fast64_t> variableToModuleIndexMap;

14
src/storage/prism/TransitionReward.cpp
View File

@ -2,12 +2,16 @@
namespace storm {
namespace prism {
TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
// Nothing to do here.
}
std::string const& TransitionReward::getActionName() const {
return this->commandName;
return this->actionName;
}
uint_fast64_t TransitionReward::getActionIndex() const {
return this->actionIndex;
}
storm::expressions::Expression const& TransitionReward::getStatePredicateExpression() const {
@ -18,8 +22,12 @@ namespace storm {
return this->rewardValueExpression;
}
bool TransitionReward::isLabeled() const {
return labeled;
}
TransitionReward TransitionReward::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
return TransitionReward(this->getActionIndex(), this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {

25
src/storage/prism/TransitionReward.h
View File

@ -16,6 +16,7 @@ namespace storm {
* Creates a transition reward for the transitions with the given name emanating from states satisfying the
* given expression with the value given by another expression.
*
* @param actionIndex The index of the action.
* @param actionName The name of the command that obtains this reward.
* @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously
* specified name in order to obtain the reward.
@ -23,7 +24,7 @@ namespace storm {
* @param filename The filename in which the transition reward is defined.
* @param lineNumber The line number in which the transition reward is defined.
*/
TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
TransitionReward() = default;
@ -41,6 +42,13 @@ namespace storm {
*/
std::string const& getActionName() const;
/*!
* Retrieves the action index of the action associated with this transition reward (if any).
*
* @return The action index of the transition reward.
*/
uint_fast64_t getActionIndex() const;
/*!
* Retrieves the state predicate expression that is associated with this state reward.
*
@ -54,6 +62,13 @@ namespace storm {
* @return The reward value expression associated with this state reward.
*/
storm::expressions::Expression const& getRewardValueExpression() const;
/*!
* Retrieves whether the transition reward has an action label.
*
* @return True iff the transition reward has an action label.
*/
bool isLabeled() const;
/*!
* Substitutes all identifiers in the transition reward according to the given map.
@ -66,8 +81,14 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward);
private:
// The index of the action name.
uint_fast64_t actionIndex;
// The name of the command this transition-based reward is attached to.
std::string commandName;
std::string actionName;
// A flag that stores whether the transition reward has an action label.
bool labeled;
// A predicate that needs to be satisfied by states for the reward to be obtained (by taking
// a corresponding command transition).

14
src/utility/PrismUtility.h
View File

@ -13,7 +13,7 @@ namespace storm {
template<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
struct Choice {
public:
Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() {
Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() {
// Intentionally left empty.
}
@ -108,12 +108,12 @@ namespace storm {
}
/*!
* Retrieves the action label of this choice.
* Retrieves the index of the action of this choice.
*
* @return The action label of this choice.
* @return The index of the action of this choice.
*/
std::string const& getActionLabel() const {
return actionLabel;
uint_fast64_t getActionIndex() const {
return actionIndex;
}
/*!
@ -152,8 +152,8 @@ namespace storm {
// The distribution that is associated with the choice.
std::map<KeyType, ValueType, Compare> distribution;
// The label of the choice.
std::string actionLabel;
// The index of the action name.
uint_fast64_t actionIndex;
// The labels that are associated with this choice.
boost::container::flat_set<uint_fast64_t> choiceLabels;

Write Preview
Loading…
Cancel
Save