diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index cc2cfa6db..a6e517038 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -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>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) { + static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) { boost::optional>>> result((std::vector>>())); // 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("")); + result.push_back(Choice()); Choice& choice = result.back(); choice.addChoiceLabel(command.getGlobalIndex()); @@ -331,9 +331,9 @@ namespace storm { static std::list> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { std::list> result; - for (std::string const& action : program.getActions()) { + for (uint_fast64_t actionIndex : program.getActionIndices()) { StateType const* currentState = stateInformation.reachableStates[stateIndex]; - boost::optional>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action); + boost::optional>>> 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(action)); + result.push_back(Choice(actionIndex)); // Now create the actual distribution. Choice& 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 globalChoice(""); + Choice globalChoice; std::map stateToRewardMap; boost::container::flat_set 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))); } } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index e1a0791cb..66e239c3a 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -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 diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 9272d1d0e..539c9bc48 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -193,9 +193,9 @@ namespace storm { qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule, std::vector>, Skipper> rewardModelDefinition; + qi::rule, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; // Rules for initial states expression. qi::rule 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 const& stateRewards, std::vector 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 const& assignments, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const; diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 3259c2673..bc40cbd78 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -10,11 +10,11 @@ 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(), actionIndices(), 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), 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 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 const& Module::getActions() const { - return this->actions; + std::set 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 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 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()); - } + 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()); } - 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(); - } - } for (auto const& actionIndex : this->actionIndices) { if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) { this->actionIndicesToCommandIndexMap[actionIndex] = std::set(); diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index c22437fdc..e8686cce5 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -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 const& getActions() const; + std::set 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 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 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 commands; - // 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; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 26bf980e8..013d3d77d 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -11,7 +11,7 @@ namespace storm { namespace prism { - Program::Program(std::shared_ptr manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::vector const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector