From da691c8102a1eb22c0f8f061e4fb0e0bf65fd358 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 21 Aug 2018 14:23:46 +0200
Subject: [PATCH] Add .dot representation for lattice

---
 src/storm-pars-cli/storm-pars.cpp   |  7 +++++-
 src/storm-pars/analysis/Lattice.cpp | 39 +++++++++++++++++++++++++++++
 src/storm-pars/analysis/Lattice.h   |  8 +++---
 3 files changed, 50 insertions(+), 4 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 7437f10ea..7ff92ca34 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -540,7 +540,12 @@ namespace storm {
 
                 latticeWatch.stop();
                 STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
-                lattice->toString(std::cout);
+
+                ofstream myfile;
+                myfile.open ("output.dot");
+                lattice->toDotFile(myfile);
+                myfile.close();
+
 
                 // Monotonicity?
                 storm::utility::Stopwatch monotonicityWatch(true);
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index 3f0f8da3f..1c4fe63c7 100644
--- a/src/storm-pars/analysis/Lattice.cpp
+++ b/src/storm-pars/analysis/Lattice.cpp
@@ -136,6 +136,45 @@ namespace storm {
             }
         }
 
+        void Lattice::toDotFile(std::ostream &out) {
+            out << "digraph \"Lattice\" {" << std::endl;
+
+            // print all nodes
+            std::vector<Node*> printed;
+            out << "\t" << "node [shape=ellipse]" << std::endl;
+            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+                if (find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
+                    out << "\t\"" << (*itr) << "\" [label = \"";
+                    uint_fast64_t index = (*itr)->states.getNextSetIndex(0);
+                    while (index < numberOfStates) {
+                        out << index;
+                        index = (*itr)->states.getNextSetIndex(index + 1);
+                        if (index < numberOfStates) {
+                            out << ", ";
+                        }
+                    }
+
+                    out << "\"]" << std::endl;
+                    printed.push_back(*itr);
+                }
+            }
+
+            // print arcs
+            printed.clear();
+            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+                if (find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
+                    auto below = (*itr)->below;
+                    for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) {
+                        out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl;
+                    }
+                    printed.push_back(*itr);
+                }
+            }
+
+            out << "}" << std::endl;
+
+
+        }
         bool Lattice::above(Node *node1, Node *node2) {
             bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();
 
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index e3e9f5246..34242fe75 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -83,6 +83,8 @@ namespace storm {
                      */
                     void toString(std::ostream &out);
 
+                    void toDotFile(std::ostream &out);
+
                     /*!
                      * Creates a Lattice based on the transition matrix, topStates of the Lattice and bottomStates of the Lattice
                      * @tparam ValueType Type of the probabilities
@@ -171,11 +173,11 @@ namespace storm {
                         uint_fast64_t successor2;
                     };
 
-                    std::vector<Node *> nodes;
+                    std::vector<Node*> nodes;
 
-                    Node * top;
+                    Node* top;
 
-                    Node * bottom;
+                    Node* bottom;
 
                     uint_fast64_t numberOfStates;