From 724e059083d6d24d00e7a35b16778a41a871d62b Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 29 Jul 2017 11:48:00 +0200 Subject: [PATCH] Fixed parsing prism models with action rewards that refer to action labels introduced during module renaming. --- src/storm/parser/PrismParser.cpp | 34 +++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 62ef9eebe..0230fbaca 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -443,23 +443,35 @@ namespace storm { } storm::prism::StateReward PrismParser::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const { - return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); + if (this->secondRun) { + return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); + } else { + return storm::prism::StateReward(); + } } storm::prism::StateActionReward PrismParser::createStateActionReward(boost::optional const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { - std::string realActionName = actionName ? actionName.get() : ""; - - auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); - STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); - return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename()); + if (this->secondRun) { + std::string realActionName = actionName ? actionName.get() : ""; + + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); + STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); + return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename()); + } else { + return storm::prism::StateActionReward(); + } } storm::prism::TransitionReward PrismParser::createTransitionReward(boost::optional const& actionName, storm::expressions::Expression sourceStatePredicateExpression, storm::expressions::Expression targetStatePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { - std::string realActionName = actionName ? actionName.get() : ""; - - auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); - STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); - return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); + if (this->secondRun) { + std::string realActionName = actionName ? actionName.get() : ""; + + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); + STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); + return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); + } else { + return storm::prism::TransitionReward(); + } } storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {