From 6a3310f7eead9e9ba9e3b6fd4882728af470cf4a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 25 Apr 2017 18:15:33 +0200
Subject: [PATCH] Improved Jani-to-dot:

- Fixed problems when the model name contained a dot
- Edges are displayed nicer
- Action names are displayed.
---
 src/storm/storage/jani/Automaton.cpp |  6 +++---
 src/storm/storage/jani/Automaton.h   |  2 +-
 src/storm/storage/jani/Model.cpp     | 22 ++++++++++++++++++++--
 3 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index 00e5bf14b..e3ec908c1 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -529,7 +529,7 @@ namespace storm {
             return result;
         }
 
-        void Automaton::writeDotToStream(std::ostream& outStream) const {
+        void Automaton::writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const {
             outStream << "\tsubgraph " << name << " {" << std::endl;
 
             // Write all locations to the stream.
@@ -541,14 +541,14 @@ namespace storm {
             // Write for each edge an node to the stream;
             uint64_t edgeIndex = 0;
             for (auto const& edge : edges) {
-                outStream << "\t" << name << "_e" << edgeIndex << ";" << std::endl;
+                outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl;
                 ++edgeIndex;
             }
 
             // Connect edges
             edgeIndex = 0;
             for (auto const& edge : edges) {
-                outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << ";" << std::endl;
+                outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << " [label=\"" << actionNames.at(edge.getActionIndex()) << "\"];" << std::endl;
                 for (auto const& edgeDest : edge.getDestinations()) {
                     outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl;
                 }
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index cf8c92fd7..37b4e9755 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -372,7 +372,7 @@ namespace storm {
              */
             bool isLinear() const;
 
-            void writeDotToStream(std::ostream& outStream = std::cout) const;
+            void writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const;
             
         private:
             /// The name of the automaton.
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 7cd420a65..27232786b 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1,5 +1,7 @@
 #include "storm/storage/jani/Model.h"
 
+#include <algorithm>
+
 #include "storm/storage/expressions/ExpressionManager.h"
 
 
@@ -1166,11 +1168,27 @@ namespace storm {
             return newModel;
         }
 
+
+        // Helper for writeDotToStream:
+
+        std::string filterName(std::string const& text)  {
+            std::string result = text;
+            std::replace_if(result.begin() , result.end() ,
+                            [] (const char& c) { return std::ispunct(c) ;},'_');
+            return result;
+        }
+
+
         void Model::writeDotToStream(std::ostream& outStream) const {
-            outStream << "digraph " << name << " {" << std::endl;
+            outStream << "digraph " << filterName(name) << " {" << std::endl;
+
+            std::vector<std::string> actionNames;
+            for (auto const& act : actions) {
+                actionNames.push_back(act.getName());
+            }
 
             for (auto const& automaton : automata) {
-                automaton.writeDotToStream(outStream);
+                automaton.writeDotToStream(outStream, actionNames);
                 outStream << std::endl;
             }