From 9ad582dafca70cc9c63136fb47455e2869f9c063 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 1 Mar 2017 10:20:44 +0100
Subject: [PATCH] Import state labeling

---
 src/storm/parser/DirectEncodingParser.cpp    | 30 +++++++++++++-------
 src/storm/parser/DirectEncodingParser.h      |  2 +-
 src/storm/utility/DirectEncodingExporter.cpp |  1 +
 3 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
index 1be94ca4c..8c1288ce1 100644
--- a/src/storm/parser/DirectEncodingParser.cpp
+++ b/src/storm/parser/DirectEncodingParser.cpp
@@ -126,6 +126,7 @@ namespace storm {
             std::shared_ptr<ModelComponents> modelComponents = std::make_shared<ModelComponents>();
             modelComponents->nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
             storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, modelComponents->nonDeterministic, 0);
+            modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
 
             // Iterate over all lines
             std::string line;
@@ -136,6 +137,11 @@ namespace storm {
                 STORM_LOG_TRACE("Parsing: " << line);
                 if (boost::starts_with(line, "state ")) {
                     // New state
+                    if (first) {
+                        first = false;
+                    } else {
+                        ++state;
+                    }
                     line = line.substr(6);
                     size_t parsedId;
                     size_t posId = line.find(" ");
@@ -151,27 +157,36 @@ namespace storm {
                             STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
                             std::string rewards = line.substr(1, posEndReward-1);
                             STORM_LOG_TRACE("State rewards: " << rewards);
-                            // TODO save rewards
+                            // TODO import rewards
+                            STORM_LOG_WARN("Rewards were not imported");
                             line = line.substr(posEndReward+1);
                         }
                         // Check for labels
                         std::vector<std::string> labels;
                         boost::split(labels, line, boost::is_any_of(" "));
-                        if (!labels.empty()) {
-                            STORM_LOG_TRACE("Labels: " << labels);
+                        for (std::string label : labels) {
+                            if (!modelComponents->stateLabeling.containsLabel(label)) {
+                                modelComponents->stateLabeling.addLabel(label);
+                            }
+                            modelComponents->stateLabeling.addLabelToState(label, state);
+                            STORM_LOG_TRACE("New label: " << label);
                         }
                     } else {
                         // Only state id given
                         parsedId = boost::lexical_cast<size_t>(line);
                     }
-                    STORM_LOG_TRACE("New state " << state << " " << parsedId);
+                    STORM_LOG_TRACE("New state " << state);
                     STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond.");
                     if (modelComponents->nonDeterministic) {
                         builder.newRowGroup(row);
                     }
-                    ++state;
                 } else if (boost::starts_with(line, "\taction ")) {
                     // New action
+                    if (first) {
+                        first = false;
+                    } else {
+                        ++row;
+                    }
                     line = line.substr(8);
                     STORM_LOG_TRACE("New action: " << row);
                     // Check for rewards
@@ -186,11 +201,6 @@ namespace storm {
                     }
                     // TODO import choice labeling when the export works
 
-                    if (first) {
-                        first = false;
-                    } else {
-                        ++row;
-                    }
                 } else {
                     // New transition
                     size_t posColon = line.find(":");
diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h
index 1bbbf6a37..ba1056401 100644
--- a/src/storm/parser/DirectEncodingParser.h
+++ b/src/storm/parser/DirectEncodingParser.h
@@ -81,7 +81,7 @@ namespace storm {
                 // A vector that stores a labeling for each choice.
                 boost::optional<std::vector<storm::models::sparse::LabelSet>> choiceLabeling;
 
-                // The exit rates for CTMCs and MAs.
+                // The exit rates for MAs.
                 std::vector<ValueType> exitRates;
 
                 // The Markovian states for MA.
diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp
index 194ba7763..f08d979d6 100644
--- a/src/storm/utility/DirectEncodingExporter.cpp
+++ b/src/storm/utility/DirectEncodingExporter.cpp
@@ -104,6 +104,7 @@ namespace storm {
                     // Write choice labeling
                     if(sparseModel->hasChoiceLabeling()) {
                         // TODO export choice labeling
+                        STORM_LOG_WARN("Choice labeling was not exported.");
                     }
                     os << std::endl;