a version of parsing choice labels from DRN

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.

src/storm-cli-utilities/model-handling.h

@@ -287,12 +287,14 @@ namespace storm {
         }
         
         template <typename ValueType>
-        std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) {
+        std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings, storm::settings::modules::BuildSettings const& buildSettings) {
             std::shared_ptr<storm::models::ModelBase> result;
             if (ioSettings.isExplicitSet()) {
                 result = storm::api::buildExplicitModel<ValueType>(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
             } else if (ioSettings.isExplicitDRNSet()) {
-                result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename());
+                storm::parser::DirectEncodingParserOptions options;
+                options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet();
+                result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename(), options);
             } else {
                 STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
                 result = storm::api::buildExplicitIMCAModel<ValueType>(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<ValueType>(ioSettings);
+                result = buildModelExplicit<ValueType>(ioSettings, buildSettings);
             }
             
             modelBuildingWatch.stop();

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -28,7 +28,7 @@ namespace storm {
     namespace parser {
 
         template<typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseModel(std::string const& filename) {
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::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<std::string, ValueType> placeholders;
             size_t nrStates = 0;
+            size_t nrChoices = 0;
             storm::models::ModelType type;
             std::vector<std::string> rewardModelNames;
             std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> 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<size_t>(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<size_t>(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<typename ValueType, typename RewardModelType>
         std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
-        DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize,
+        DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices,
                                                                       std::unordered_map<std::string, ValueType> const& placeholders, ValueParser<ValueType> const& valueParser,
-                                                                      std::vector<std::string> const& rewardModelNames) {
+                                                                      std::vector<std::string> const& rewardModelNames, DirectEncodingParserOptions const& options) {
             // Initialize
             auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
             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<uint32_t>();
             modelComponents->observabilityClasses->resize(stateSize);
+            if (options.buildChoiceLabeling) {
+                modelComponents->choiceLabeling = storm::models::sparse::ChoiceLabeling(nrChoices);
+            }
             std::vector<std::vector<ValueType>> stateRewards;
             std::vector<std::vector<ValueType>> actionRewards;
             if (continuousTime) {
@@ -296,8 +305,15 @@ namespace storm {
                     } else {
                         line = "";
                     }
-                    size_t parsedId = parseNumber<size_t>(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

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<storm::models::sparse::Model<ValueType, RewardModelType>> parseModel(std::string const& file);
+            static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> parseModel(std::string const& fil, DirectEncodingParserOptions const& options = DirectEncodingParserOptions());
 
         private:
 
@@ -40,8 +43,8 @@ namespace storm {
              * @return Transition matrix.
              */
             static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
-            parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, std::unordered_map<std::string, ValueType> const& placeholders,
-                        ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
+            parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map<std::string, ValueType> const& placeholders,
+                        ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames, DirectEncodingParserOptions const& options);
 
             /*!
              * Parse value from string while using placeholders.

src/storm/api/builder.h

@@ -144,8 +144,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile) {
-            return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile);
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile, storm::parser::DirectEncodingParserOptions const& options = storm::parser::DirectEncodingParserOptions()) {
+            return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile, options);
         }
         
         template<typename ValueType>

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 << "_";