diff --git a/CHANGELOG.md b/CHANGELOG.md index de69b3b1d..a96db712f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,7 +8,7 @@ Version 1.4.x ------------- ## Version 1.4.2 (under development) -- n.a. +- DRN: support import of choice labelling ### Version 1.4.1 (2019/12) - Implemented long run average (LRA) computation for DTMCs/CTMCs via value iteration and via gain/bias equations. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index a70ddf981..3f47635a5 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -287,12 +287,14 @@ namespace storm { } template - std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings, storm::settings::modules::BuildSettings const& buildSettings) { std::shared_ptr result; if (ioSettings.isExplicitSet()) { result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); } else if (ioSettings.isExplicitDRNSet()) { - result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); + storm::parser::DirectEncodingParserOptions options; + options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet(); + result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename(), options); } else { STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type."); result = storm::api::buildExplicitIMCAModel(ioSettings.getExplicitIMCAFilename()); @@ -315,7 +317,7 @@ namespace storm { } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); - result = buildModelExplicit(ioSettings); + result = buildModelExplicit(ioSettings, buildSettings); } modelBuildingWatch.stop(); diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index d77415f72..2e4dc5c39 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -28,7 +28,7 @@ namespace storm { namespace parser { template - std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename) { + std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename, DirectEncodingParserOptions const& options) { // Load file STORM_LOG_INFO("Reading from file " << filename); @@ -42,6 +42,7 @@ namespace storm { bool sawParameters = false; std::unordered_map placeholders; size_t nrStates = 0; + size_t nrChoices = 0; storm::models::ModelType type; std::vector rewardModelNames; std::shared_ptr> modelComponents; @@ -102,14 +103,19 @@ namespace storm { STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); std::getline(file, line); nrStates = parseNumber(line); + } else if (line == "@nr_choices") { + STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice"); + std::getline(file, line); + nrChoices = parseNumber(line); } else if (line == "@model") { // Parse rest of the model STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model."); STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model."); STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model."); - + STORM_LOG_THROW(!options.buildChoiceLabeling || nrChoices != 0, storm::exceptions::WrongFormatException, "No. of actions (@nr_choices) has to be declared before model."); + STORM_LOG_WARN_COND(nrChoices != 0, "No. of actions has to be declared. We may continue now, but future versions might not support this."); // Construct model components - modelComponents = parseStates(file, type, nrStates, placeholders, valueParser, rewardModelNames); + modelComponents = parseStates(file, type, nrStates, nrChoices, placeholders, valueParser, rewardModelNames, options); break; } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'."); @@ -124,9 +130,9 @@ namespace storm { template std::shared_ptr> - DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, + DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map const& placeholders, ValueParser const& valueParser, - std::vector const& rewardModelNames) { + std::vector const& rewardModelNames, DirectEncodingParserOptions const& options) { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp); @@ -135,6 +141,9 @@ namespace storm { modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); modelComponents->observabilityClasses = std::vector(); modelComponents->observabilityClasses->resize(stateSize); + if (options.buildChoiceLabeling) { + modelComponents->choiceLabeling = storm::models::sparse::ChoiceLabeling(nrChoices); + } std::vector> stateRewards; std::vector> actionRewards; if (continuousTime) { @@ -296,8 +305,15 @@ namespace storm { } else { line = ""; } - size_t parsedId = parseNumber(curString); - STORM_LOG_ASSERT(row == firstRowOfState + parsedId, "Action ids do not correspond."); + // curString contains action name or reward. + if (options.buildChoiceLabeling) { + if (curString != "__NOLABEL__") { + if (!modelComponents->choiceLabeling.get().containsLabel(curString)) { + modelComponents->choiceLabeling.get().addLabel(curString); + } + modelComponents->choiceLabeling.get().addLabelToChoice(curString, row); + } + } // Check for rewards if (boost::starts_with(line, "[")) { // Rewards found @@ -323,7 +339,6 @@ namespace storm { } line = line.substr(posEndReward + 1); } - // TODO import choice labeling when the export works } else { // New transition diff --git a/src/storm-parsers/parser/DirectEncodingParser.h b/src/storm-parsers/parser/DirectEncodingParser.h index 5637a2f46..6c4254013 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.h +++ b/src/storm-parsers/parser/DirectEncodingParser.h @@ -9,6 +9,9 @@ namespace storm { namespace parser { + struct DirectEncodingParserOptions { + bool buildChoiceLabeling = false; + }; /*! * Parser for models in the DRN format with explicit encoding. */ @@ -23,7 +26,7 @@ namespace storm { * * @return A sparse model */ - static std::shared_ptr> parseModel(std::string const& file); + static std::shared_ptr> parseModel(std::string const& fil, DirectEncodingParserOptions const& options = DirectEncodingParserOptions()); private: @@ -40,8 +43,8 @@ namespace storm { * @return Transition matrix. */ 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); + parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map const& placeholders, + ValueParser const& valueParser, std::vector const& rewardModelNames, DirectEncodingParserOptions const& options); /*! * Parse value from string while using placeholders. diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 5fc7898ee..0df66c7ff 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -144,8 +144,8 @@ namespace storm { } template - std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { - return storm::parser::DirectEncodingParser::parseModel(drnFile); + std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile, storm::parser::DirectEncodingParserOptions const& options = storm::parser::DirectEncodingParserOptions()) { + return storm::parser::DirectEncodingParser::parseModel(drnFile, options); } template diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index a5c152994..5e1ce3231 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -126,6 +126,9 @@ namespace storm { if (sparseModel->hasChoiceLabeling()) { os << "\taction "; bool lfirst = true; + if (sparseModel->getChoiceLabeling().getLabelsOfChoice(row).empty()) { + os << "__NOLABEL__"; + } for (auto const& label : sparseModel->getChoiceLabeling().getLabelsOfChoice(row)) { if (!lfirst) { os << "_";