From 240f81dfcbd2054eefff3178f3dded509c19846e Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 14 Sep 2018 11:34:24 +0200
Subject: [PATCH] Clean up MonotonicityChecker

---
 src/storm-pars/analysis/MonotonicityChecker.cpp | 10 ++++------
 src/storm-pars/analysis/MonotonicityChecker.h   |  6 ++++++
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 62be096db..0d98cd3f9 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -3,14 +3,13 @@
 //
 
 #include "MonotonicityChecker.h"
-#include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"   
 
 namespace storm {
     namespace analysis {
         template <typename ValueType>
         void MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
-
             auto i = 0;
             for (auto itr = map.begin(); itr != map.end(); ++itr) {
                 auto lattice = itr->first;
@@ -52,7 +51,6 @@ namespace storm {
                         STORM_PRINT("  - Do not know if monotone decreasing in: " << itr2->first << std::endl);
                     }
                 }
-
                 ++i;
             }
         }
@@ -65,12 +63,12 @@ namespace storm {
             myfile.open (filename);
             myfile << "digraph \"MC\" {" << std::endl;
             myfile << "\t" << "node [shape=ellipse]" << std::endl;
+
             // print all nodes
             for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
                 myfile << "\t\"" << i << "\" [label = \"" << i << "\"]" << std::endl;
             }
 
-
             for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
                 // go over all rows
                 auto row = matrix.getRow(i);
@@ -134,7 +132,6 @@ namespace storm {
                                << std::endl;
                     }
 
-
                     myfile << "\t edge[style=\"\"];" << std::endl;
                 } else {
                     myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];"
@@ -153,7 +150,8 @@ namespace storm {
             myfile << "}" << std::endl;
             myfile.close();
             return varsMonotone;
-        };
+        }
+
         template class MonotonicityChecker<storm::RationalFunction>;
     }
 }
diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h
index 7b1dcb1f1..9d90e8b5d 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.h
+++ b/src/storm-pars/analysis/MonotonicityChecker.h
@@ -18,6 +18,12 @@ namespace storm {
         class MonotonicityChecker {
 
         public:
+            /*!
+             * Checks for all lattices in the map if they are monotone increasing or monotone decreasing.
+             *
+             * @param map The map with lattices and the assumptions made to create the lattices.
+             * @param matrix The transition matrix.
+             */
             void checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
 
         private: