diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 6fb53a765..cc2cfa6db 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -230,10 +230,10 @@ namespace storm { * * @param The program in which to search for active commands. * @param state The current state. - * @param action The action label to select. + * @param actionIndex The index of the action label to select. * @return A list of lists of active commands or nothing. */ - static boost::optional>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, std::string const& action) { + static boost::optional>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) { boost::optional>>> result((std::vector>>())); // Iterate over all modules. @@ -241,11 +241,11 @@ namespace storm { storm::prism::Module const& module = program.getModule(i); // If the module has no command labeled with the given action, we can skip this module. - if (!module.hasAction(action)) { + if (!module.hasActionIndex(actionIndex)) { continue; } - std::set const& commandIndices = module.getCommandIndicesByAction(action); + std::set const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); // If the module contains the action, but there is no command in the module that is labeled with // this action, we don't have any feasible command combinations. @@ -288,7 +288,7 @@ namespace storm { storm::prism::Command const& command = module.getCommand(j); // Only consider unlabeled commands. - if (command.getActionName() != "") continue; + if (!command.isLabeled()) continue; // Skip the command, if it is not enabled. if (!command.getGuardExpression().evaluateAsBool(currentState)) { @@ -538,7 +538,7 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { + if (!transitionReward.empty() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); } } @@ -551,7 +551,7 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { + if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); } } @@ -589,7 +589,7 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionName() == "" && 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))); } } @@ -616,7 +616,7 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { + if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); } } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 74b7b43d3..e1a0791cb 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -139,7 +139,7 @@ namespace storm { updateListDefinition %= +updateDefinition(qi::_r1) % "+"; updateListDefinition.name("update list"); - commandDefinition = qi::lit("[") > +(qi::char_ - qi::lit(";")) > qi::lit(";")[qi::_val = phoenix::construct()]; + commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)]; commandDefinition.name("command definition"); moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)]; @@ -355,7 +355,21 @@ namespace storm { storm::prism::Command PrismParser::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const { ++globalProgramInformation.currentCommandIndex; - return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName, guardExpression, updates, this->getFilename()); + return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename()); + } + + storm::prism::Command PrismParser::createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const { + STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run."); + + if (!actionName.empty()) { + // Register the action name if it has not appeared earlier. + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size(); + } + } + + return storm::prism::Command(); } storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { @@ -474,7 +488,12 @@ namespace storm { newActionName = renamingPair->second; } - commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size(); + } + + commands.emplace_back(globalProgramInformation.currentCommandIndex, globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 38e31a568..9272d1d0e 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -21,7 +21,7 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) { + GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) { // Intentionally left empty. } @@ -32,6 +32,7 @@ namespace storm { std::vector globalBooleanVariables; std::vector globalIntegerVariables; std::map moduleToIndexMap; + std::map actionIndices; std::vector modules; std::vector rewardModels; std::vector labels; @@ -235,6 +236,7 @@ namespace storm { storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const; storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector const& assignments, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Command createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const; storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const; storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const; storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h index 0aeeb8eca..2865e0e86 100644 --- a/src/storage/expressions/Valuation.h +++ b/src/storage/expressions/Valuation.h @@ -3,6 +3,7 @@ #include #include +#include namespace storm { namespace expressions { diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index aa13da0e8..fec849628 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -2,10 +2,14 @@ namespace storm { namespace prism { - Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) { + Command::Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex), labeled(actionName != "") { // Nothing to do here. } + uint_fast64_t Command::getActionIndex() const { + return this->actionIndex; + } + std::string const& Command::getActionName() const { return this->actionName; } @@ -37,7 +41,11 @@ namespace storm { newUpdates.emplace_back(update.substitute(substitution)); } - return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); + return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); + } + + bool Command::isLabeled() const { + return labeled; } std::ostream& operator<<(std::ostream& stream, Command const& command) { diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index 60095d13c..e0dac47f9 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -17,18 +17,19 @@ namespace storm { * Creates a command with the given action name, guard and updates. * * @param globalIndex The global index of the command. + * @param actionIndex The index of the action of the command. * @param actionName The action name of the command. * @param guardExpression the expression that defines the guard of the command. * @param updates A list of updates that is associated with this command. * @param filename The filename in which the command is defined. * @param lineNumber The line number in which the command is defined. */ - Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Command() = default; Command(Command const& other) = default; - Command& operator=(Command const& other)= default; + Command& operator=(Command const& other) = default; #ifndef WINDOWS Command(Command&& other) = default; Command& operator=(Command&& other) = default; @@ -41,6 +42,13 @@ namespace storm { */ std::string const& getActionName() const; + /*! + * Retrieves the action index of this command. + * + * @return The action index of the command. + */ + uint_fast64_t getActionIndex() const; + /*! * Retrieves a reference to the guard of the command. * @@ -84,9 +92,19 @@ namespace storm { */ Command substitute(std::map const& substitution) const; + /*! + * Retrieves whether the command possesses a synchronization label. + * + * @return True iff the command is labeled. + */ + bool isLabeled() const; + friend std::ostream& operator<<(std::ostream& stream, Command const& command); private: + // The index of the action associated with this command. + uint_fast64_t actionIndex; + // The name of the command. std::string actionName; @@ -98,6 +116,9 @@ namespace storm { // The global index of the command. uint_fast64_t globalIndex; + + // A flag indicating whether the command is labeled. + bool labeled; }; } // namespace prism diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 2233ababa..3259c2673 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -10,7 +10,7 @@ namespace storm { // Intentionally left empty. } - Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map 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) { // Initialize the internal mappings for fast information retrieval. this->createMappings(); } @@ -76,6 +76,10 @@ namespace storm { return actionEntry != this->actions.end(); } + bool Module::hasActionIndex(uint_fast64_t const& actionIndex) const { + return this->actionIndices.find(actionIndex) != this->actionIndices.end(); + } + bool Module::isRenamedFromModule() const { return this->renamedFromModule != ""; } @@ -99,9 +103,19 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module."); } + std::set const& Module::getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const { + auto actionIndicesCommandSetPair = this->actionIndicesToCommandIndexMap.find(actionIndex); + if (actionIndicesCommandSetPair != this->actionIndicesToCommandIndexMap.end()) { + return actionIndicesCommandSetPair->second; + } + + STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action index '" << actionIndex << "' does not exist in module."); + } + void Module::createMappings() { // Clear the current mappings. this->actionsToCommandIndexMap.clear(); + this->actionIndicesToCommandIndexMap.clear(); this->booleanVariableToIndexMap.clear(); this->integerVariableToIndexMap.clear(); @@ -116,12 +130,19 @@ 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()); } + if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) { + this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set()); + } this->actionsToCommandIndexMap[action].insert(i); + this->actionIndicesToCommandIndexMap[actionIndex].insert(i); + this->actions.insert(action); + this->actionIndices.insert(this->commands[i].getActionIndex()); } } @@ -132,6 +153,11 @@ namespace storm { this->actionsToCommandIndexMap[action] = std::set(); } } + for (auto const& actionIndex : this->actionIndices) { + if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) { + this->actionIndicesToCommandIndexMap[actionIndex] = std::set(); + } + } } Module Module::restrictCommands(boost::container::flat_set const& indexSet) const { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 9fe981340..c22437fdc 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -148,6 +148,14 @@ namespace storm { * @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. + * @return True iff the module has at least one command labeled with the given action index. + */ + bool hasActionIndex(uint_fast64_t const& actionIndex) const; /*! * Retrieves whether this module was created from another module via renaming. @@ -180,6 +188,14 @@ namespace storm { */ std::set const& getCommandIndicesByAction(std::string const& action) const; + /*! + * Retrieves the indices of all commands within this module that are labelled by the given action. + * + * @param actionIndex The index of the action with which the commands have to be labelled. + * @return A set of indices of commands that are labelled with the given action index. + */ + std::set const& getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const; + /*! * Creates a new module that drops all commands whose indices are not in the given set. * @@ -225,8 +241,14 @@ namespace storm { // The set of actions present in this module. std::set actions; + // The set of action indices present in this module. + std::set actionIndices; + // A map of actions to the set of commands labeled with this action. std::map> actionsToCommandIndexMap; + + // A map of actions to the set of commands labeled with this action. + std::map> actionIndicesToCommandIndexMap; // This string indicates whether and from what module this module was created via renaming. std::string renamedFromModule;