diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 926993130..c2c1a5998 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -2,6 +2,8 @@ #include #include + +#include #include #include "storm/models/sparse/MarkovAutomaton.h" @@ -19,6 +21,7 @@ #include "storm/utility/macros.h" #include "storm/utility/file.h" + namespace storm { namespace parser { @@ -64,6 +67,8 @@ namespace storm { size_t nrStates = 0; storm::models::ModelType type; + std::vector rewardModelNames; + std::shared_ptr> modelComponents; // Parse header @@ -92,6 +97,11 @@ namespace storm { } sawParameters = true; } + if(line == "@reward_models") { + STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice"); + std::getline(file, line); + boost::split(rewardModelNames, line, boost::is_any_of("\t ")); + } if(line == "@nr_states") { STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); std::getline(file, line); @@ -104,7 +114,7 @@ namespace storm { STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model."); // Construct model components - modelComponents = parseStates(file, type, nrStates, valueParser); + modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames); break; } } @@ -116,7 +126,7 @@ namespace storm { } template - std::shared_ptr> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser) { + std::shared_ptr> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser, std::vector const& rewardModelNames) { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp); @@ -242,8 +252,15 @@ namespace storm { STORM_LOG_TRACE("Finished parsing"); modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0); + for (uint64_t i = 0; i < stateRewards.size(); ++i) { - modelComponents->rewardModels.emplace("rew" + std::to_string(i), storm::models::sparse::StandardRewardModel(std::move(stateRewards[i]))); + std::string rewardModelName; + if (rewardModelNames.size() <= i) { + rewardModelName = "rew" + std::to_string(i); + } else { + rewardModelName = rewardModelNames[i]; + } + modelComponents->rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(std::move(stateRewards[i]))); } STORM_LOG_TRACE("Built matrix"); return modelComponents; diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h index 43a5a6f8b..db1bac12e 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm/parser/DirectEncodingParser.h @@ -75,7 +75,7 @@ namespace storm { * * @return Transition matrix. */ - static std::shared_ptr> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser); + static std::shared_ptr> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser, std::vector const& rewardModelNames); }; } // namespace parser diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index a8ee45fb0..a7f95f3dc 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -47,6 +47,11 @@ namespace storm { } } os << std::endl; + os << "@reward_models" << std::endl; + for (auto const& rewardModel : sparseModel->getRewardModels()) { + os << rewardModel.first << " "; + } + os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; os << "@model" << std::endl;