From 8b77f7f6d674e3fb9577269f6068ae044b88473e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Aug 2019 21:19:32 +0200 Subject: [PATCH] Added placeholders to DRN format --- .../parser/DirectEncodingParser.cpp | 75 ++++++++---- .../parser/DirectEncodingParser.h | 20 +++- src/storm/utility/DirectEncodingExporter.cpp | 107 ++++++++++++++++-- src/storm/utility/DirectEncodingExporter.h | 20 ++++ 4 files changed, 191 insertions(+), 31 deletions(-) diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 847b007cd..d77415f72 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -40,6 +40,7 @@ namespace storm { ValueParser valueParser; bool sawType = false; bool sawParameters = false; + std::unordered_map placeholders; size_t nrStates = 0; storm::models::ModelType type; std::vector rewardModelNames; @@ -56,7 +57,8 @@ namespace storm { STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice"); type = storm::models::getModelType(line.substr(7)); STORM_LOG_TRACE("Model type: " << type); - STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported."); + STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, + "Stochastic Two Player Games in DRN format are not supported."); sawType = true; } else if (line == "@parameters") { @@ -73,6 +75,23 @@ namespace storm { } sawParameters = true; + } else if (line == "@placeholders") { + // Parse placeholders + while (std::getline(file, line)) { + size_t posColon = line.find(':'); + STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found."); + std::string placeName = line.substr(0, posColon - 1); + STORM_LOG_THROW(placeName.front() == '$', storm::exceptions::WrongFormatException, "Placeholder must start with dollar symbol $."); + std::string valueStr = line.substr(posColon + 2); + ValueType value = parseValue(valueStr, placeholders, valueParser); + STORM_LOG_TRACE("Placeholder " << placeName << " for value " << value); + auto ret = placeholders.insert(std::make_pair(placeName.substr(1), value)); + STORM_LOG_THROW(ret.second, storm::exceptions::WrongFormatException, "Placeholder '$" << placeName << "' was already defined before."); + if (file.peek() == '@') { + // Next character is @ -> placeholder definitions ended + break; + } + } } else if (line == "@reward_models") { // Parse reward models STORM_LOG_THROW(rewardModelNames.empty(), storm::exceptions::WrongFormatException, "Reward model names declared twice"); @@ -90,7 +109,7 @@ namespace storm { STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model."); // Construct model components - modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames); + modelComponents = parseStates(file, type, nrStates, placeholders, valueParser, rewardModelNames); break; } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'."); @@ -104,7 +123,10 @@ namespace storm { } template - std::shared_ptr> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser, std::vector const& rewardModelNames) { + std::shared_ptr> + DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, + std::unordered_map const& placeholders, 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); @@ -152,7 +174,7 @@ namespace storm { size_t posEnd = line.find(" "); if (posEnd != std::string::npos) { curString = line.substr(0, posEnd); - line = line.substr(posEnd+1); + line = line.substr(posEnd + 1); } else { line = ""; } @@ -172,11 +194,11 @@ namespace storm { posEnd = line.find(" "); if (posEnd != std::string::npos) { curString = line.substr(0, posEnd); - line = line.substr(posEnd+1); + line = line.substr(posEnd + 1); } else { line = ""; } - ValueType exitRate = valueParser.parseValue(curString); + ValueType exitRate = parseValue(curString, placeholders, valueParser); if (type == storm::models::ModelType::MarkovAutomaton && !storm::utility::isZero(exitRate)) { modelComponents->markovianStates.get().set(state); } @@ -188,7 +210,7 @@ namespace storm { // Parse rewards size_t posEndReward = line.find(']'); STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); - std::string rewardsStr = line.substr(1, posEndReward-1); + std::string rewardsStr = line.substr(1, posEndReward - 1); STORM_LOG_TRACE("State rewards: " << rewardsStr); std::vector rewards; boost::split(rewards, rewardsStr, boost::is_any_of(",")); @@ -197,7 +219,7 @@ namespace storm { } auto stateRewardsIt = stateRewards.begin(); for (auto const& rew : rewards) { - auto rewardValue = valueParser.parseValue(rew); + auto rewardValue = parseValue(rew, placeholders, valueParser); if (!storm::utility::isZero(rewardValue)) { if (stateRewardsIt->empty()) { stateRewardsIt->resize(stateSize, storm::utility::zero()); @@ -206,17 +228,17 @@ namespace storm { } ++stateRewardsIt; } - line = line.substr(posEndReward+1); + line = line.substr(posEndReward + 1); } if (type == storm::models::ModelType::Pomdp) { if (boost::starts_with(line, "{")) { size_t posEndObservation = line.find("}"); - std::string observation = line.substr(1, posEndObservation-1); + std::string observation = line.substr(1, posEndObservation - 1); STORM_LOG_TRACE("State observation " << observation); modelComponents->observabilityClasses.get()[state] = std::stoi(observation); - line = line.substr(posEndObservation+1); + line = line.substr(posEndObservation + 1); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Expected an observation for state " << state << "."); } @@ -270,7 +292,7 @@ namespace storm { size_t posEnd = line.find(" "); if (posEnd != std::string::npos) { curString = line.substr(0, posEnd); - line = line.substr(posEnd+1); + line = line.substr(posEnd + 1); } else { line = ""; } @@ -281,7 +303,7 @@ namespace storm { // Rewards found size_t posEndReward = line.find(']'); STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); - std::string rewardsStr = line.substr(1, posEndReward-1); + std::string rewardsStr = line.substr(1, posEndReward - 1); STORM_LOG_TRACE("Action rewards: " << rewardsStr); std::vector rewards; boost::split(rewards, rewardsStr, boost::is_any_of(",")); @@ -290,7 +312,7 @@ namespace storm { } auto actionRewardsIt = actionRewards.begin(); for (auto const& rew : rewards) { - auto rewardValue = valueParser.parseValue(rew); + auto rewardValue = parseValue(rew, placeholders, valueParser); if (!storm::utility::isZero(rewardValue)) { if (actionRewardsIt->size() <= row) { actionRewardsIt->resize(std::max(row + 1, stateSize), storm::utility::zero()); @@ -299,7 +321,7 @@ namespace storm { } ++actionRewardsIt; } - line = line.substr(posEndReward+1); + line = line.substr(posEndReward + 1); } // TODO import choice labeling when the export works @@ -307,9 +329,9 @@ namespace storm { // New transition size_t posColon = line.find(':'); STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found."); - size_t target = parseNumber(line.substr(2, posColon-3)); - std::string valueStr = line.substr(posColon+2); - ValueType value = valueParser.parseValue(valueStr); + size_t target = parseNumber(line.substr(2, posColon - 3)); + std::string valueStr = line.substr(posColon + 2); + ValueType value = parseValue(valueStr, placeholders, valueParser); STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value); STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize); builder.addNextValue(row, target, value); @@ -338,12 +360,27 @@ namespace storm { actionRewards[i].resize(row + 1, storm::utility::zero()); actionRewardVector = std::move(actionRewards[i]); } - modelComponents->rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(std::move(stateRewardVector), std::move(actionRewardVector))); + modelComponents->rewardModels.emplace(rewardModelName, + storm::models::sparse::StandardRewardModel(std::move(stateRewardVector), std::move(actionRewardVector))); } STORM_LOG_TRACE("Built reward models"); return modelComponents; } + template + ValueType DirectEncodingParser::parseValue(std::string const& valueStr, std::unordered_map const& placeholders, + ValueParser const& valueParser) { + if (boost::starts_with(valueStr, "$")) { + auto it = placeholders.find(valueStr.substr(1)); + STORM_LOG_THROW(it != placeholders.end(), storm::exceptions::WrongFormatException, "Placeholder " << valueStr << " unknown."); + return it->second; + } else { + // Use default value parser + return valueParser.parseValue(valueStr); + } + } + + // Template instantiations. template class DirectEncodingParser; template class DirectEncodingParser; diff --git a/src/storm-parsers/parser/DirectEncodingParser.h b/src/storm-parsers/parser/DirectEncodingParser.h index f025b8dfc..5637a2f46 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.h +++ b/src/storm-parsers/parser/DirectEncodingParser.h @@ -30,13 +30,27 @@ namespace storm { /*! * Parse states and return transition matrix. * - * @param file Input file stream. - * @param type Model type. + * @param file Input file stream. + * @param type Model type. * @param stateSize No. of states + * @param placeholders Placeholders for values. + * @param valueParser Value parser. + * @param rewardModelNames Names of reward models. * * @return Transition matrix. */ - static std::shared_ptr> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser, std::vector const& rewardModelNames); + static std::shared_ptr> + parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, std::unordered_map const& placeholders, + ValueParser const& valueParser, std::vector const& rewardModelNames); + + /*! + * Parse value from string while using placeholders. + * @param valueStr String. + * @param placeholders Placeholders. + * @param valueParser Value parser. + * @return + */ + static ValueType parseValue(std::string const& valueStr, std::unordered_map const& placeholders, ValueParser const& valueParser); }; } // namespace parser diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 568223489..ebda39247 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -45,12 +45,24 @@ namespace storm { } } os << std::endl; + + // Optionally write placeholders which only need to be parsed once + // This is used to reduce the parsing effort for rational functions + // Placeholders begin with the dollar symbol $ + std::unordered_map placeholders = generatePlaceholders(sparseModel, exitRates); + if (!placeholders.empty()) { + os << "@placeholders" << std::endl; + for (auto const& entry : placeholders) { + os << "$" << entry.second << " : " << entry.first << 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 << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; os << "@model" << std::endl; storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); @@ -61,7 +73,8 @@ namespace storm { // Write exit rates for CTMCs and MAs if (!exitRates.empty()) { - os << " !" << exitRates.at(group); + os << " !"; + writeValue(os, exitRates.at(group), placeholders); } // Write state rewards @@ -74,8 +87,8 @@ namespace storm { os << ", "; } - if(rewardModelEntry.second.hasStateRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateRewardVector().at(group)); + if (rewardModelEntry.second.hasStateRewards()) { + writeValue(os, rewardModelEntry.second.getStateRewardVector().at(group), placeholders); } else { os << "0"; } @@ -90,10 +103,11 @@ namespace storm { } // Write labels. Only labels with a whitespace are put in (double) quotation marks. - for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { - STORM_LOG_THROW(std::count( label.begin(), label.end(), '\"' ) == 0, storm::exceptions::NotSupportedException, "Labels with quotation marks are not supported in the DRN format and therefore may not be exported."); + for (auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { + STORM_LOG_THROW(std::count(label.begin(), label.end(), '\"') == 0, storm::exceptions::NotSupportedException, + "Labels with quotation marks are not supported in the DRN format and therefore may not be exported."); // TODO consider escaping the quotation marks. Not sure whether that is a good idea. - if (std::count_if( label.begin(), label.end(), isspace ) > 0) { + if (std::count_if(label.begin(), label.end(), isspace) > 0) { os << " \"" << label << "\""; } else { os << " " << label; @@ -133,7 +147,7 @@ namespace storm { } if (rewardModelEntry.second.hasStateActionRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row)); + writeValue(os, rewardModelEntry.second.getStateActionRewardVector().at(row), placeholders); } else { os << "0"; } @@ -148,7 +162,8 @@ namespace storm { for (auto it = matrix.begin(row); it != matrix.end(row); ++it) { ValueType prob = it->getValue(); os << "\t\t" << it->getColumn() << " : "; - os << storm::utility::to_string(prob) << std::endl; + writeValue(os, prob, placeholders); + os << std::endl; } } @@ -179,6 +194,80 @@ namespace storm { return parameters; } + template + std::unordered_map generatePlaceholders(std::shared_ptr>, std::vector) { + return {}; + } + + /*! + * Helper function to create a possible placeholder. + * A new placeholder is inserted if the rational function is not constant and the function does not exist yet. + * @param placeholders Existing placeholders. + * @param value Value. + * @param i Counter to enumerate placeholders. + */ + + void createPlaceholder(std::unordered_map& placeholders, storm::RationalFunction const& value, size_t& i) { + if (!storm::utility::isConstant(value)) { + auto ret = placeholders.insert(std::make_pair(value, std::to_string(i))); + if (ret.second) { + // New element was inserted + ++i; + } + } + } + + template<> + std::unordered_map + generatePlaceholders(std::shared_ptr> sparseModel, std::vector exitRates) { + std::unordered_map placeholders; + size_t i = 0; + + // Exit rates + for (auto const& exitRate : exitRates) { + createPlaceholder(placeholders, exitRate, i); + } + + // Rewards + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (rewardModelEntry.second.hasStateRewards()) { + for (auto const& reward : rewardModelEntry.second.getStateRewardVector()) { + createPlaceholder(placeholders, reward, i); + } + } + if (rewardModelEntry.second.hasStateActionRewards()) { + for (auto const& reward : rewardModelEntry.second.getStateActionRewardVector()) { + createPlaceholder(placeholders, reward, i); + } + } + } + + // Transition probabilities + for (auto const& entry : sparseModel->getTransitionMatrix()) { + createPlaceholder(placeholders, entry.getValue(), i); + } + + return placeholders; + } + + template + void writeValue(std::ostream& os, ValueType value, std::unordered_map const& placeholders) { + if (storm::utility::isConstant(value)) { + os << value; + return; + } + + // Try to use placeholder + auto it = placeholders.find(value); + if (it != placeholders.end()) { + // Use placeholder + os << "$" << it->second; + } else { + os << value; + } + } + + // Template instantiations template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h index 5ffe4d10d..c39622bf1 100644 --- a/src/storm/utility/DirectEncodingExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -1,4 +1,5 @@ #pragma once + #include #include @@ -17,6 +18,7 @@ namespace storm { template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + /*! * Accumulate parameters in the model. * @@ -26,5 +28,23 @@ namespace storm { template std::vector getParameters(std::shared_ptr> sparseModel); + /*! + * Generate placeholders for rational functions in the model. + * + * @param sparseModel Model. + * @param exitRates Exit rates. + * @return Mapping of the form:rational function -> placeholder name. + */ + template + std::unordered_map generatePlaceholders(std::shared_ptr> sparseModel, std::vector exitRates); + + /*! + * Write value to stream while using the placeholders. + * @param os Output stream. + * @param value Value. + * @param placeholders Placeholders. + */ + template + void writeValue(std::ostream& os, ValueType value, std::unordered_map const& placeholders); } }