From 976f85cc25d551acd8b7b0df9811f140fe2bcfc3 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 19 Jul 2019 00:10:55 +0200
Subject: [PATCH] drn export for labels with whitespace is now put into
 quotation marks

---
 src/storm/utility/DirectEncodingExporter.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp
index 61487bb25..568223489 100644
--- a/src/storm/utility/DirectEncodingExporter.cpp
+++ b/src/storm/utility/DirectEncodingExporter.cpp
@@ -1,3 +1,4 @@
+#include <storm/exceptions/NotSupportedException.h>
 #include "DirectEncodingExporter.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -88,9 +89,15 @@ namespace storm {
                     os << " {" << sparseModel->template as<storm::models::sparse::Pomdp<ValueType>>()->getObservation(group) << "}";
                 }
 
-                // Write labels
+                // Write labels. Only labels with a whitespace are put in (double) quotation marks.
                 for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) {
-                    os << " " << label;
+                    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) {
+                        os << " \"" << label << "\"";
+                    } else {
+                        os << " " << label;
+                    }
                 }
                 os << std::endl;