From c36d869b3cf65f04fe0fc50214b4e21480b009b2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 20 Nov 2015 17:07:50 +0100
Subject: [PATCH] done cleaining up

Former-commit-id: 4c732fc1882854c5f0492a19ae052f6f99cd62d0
---
 src/storage/dd/Add.h       |  4 ++--
 src/storage/dd/Bdd.h       |  8 ++++++--
 src/storage/dd/DdManager.h | 22 +++++++++++++++++++---
 src/storage/dd/Odd.cpp     |  1 +
 4 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h
index 120aef683..3aedb86a4 100644
--- a/src/storage/dd/Add.h
+++ b/src/storage/dd/Add.h
@@ -626,10 +626,10 @@ namespace storm {
             
         private:
             /*!
-             * Creates a DD that encapsulates the given CUDD ADD.
+             * Creates a DD that encapsulates the given CUDD internal ADD.
              *
              * @param ddManager The manager responsible for this DD.
-             * @param cuddBdd The CUDD BDD to store.
+             * @param internalAdd The internal ADD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
             Add(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalAdd<LibraryType, ValueType> const& internalAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index e5c0fe5b3..65cf35f55 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -7,6 +7,10 @@
 #include "src/storage/dd/cudd/InternalCuddBdd.h"
 
 namespace storm {
+    namespace logic {
+        enum class ComparisonType;
+    }
+    
     namespace dd {
         template<DdType LibraryType, typename ValueType>
         class Add;
@@ -265,10 +269,10 @@ namespace storm {
             operator InternalBdd<LibraryType>() const;
             
             /*!
-             * Creates a DD that encapsulates the given CUDD ADD.
+             * Creates a DD that encapsulates the given internal BDD.
              *
              * @param ddManager The manager responsible for this DD.
-             * @param cuddBdd The CUDD BDD to store.
+             * @param internalBdd The internal BDD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
             Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
index fa7e5d3ea..1c068684e 100644
--- a/src/storage/dd/DdManager.h
+++ b/src/storage/dd/DdManager.h
@@ -146,21 +146,21 @@ namespace storm {
             bool hasMetaVariable(std::string const& variableName) const;
             
             /*!
-             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
+             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager (if supported).
              *
              * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
              */
             void allowDynamicReordering(bool value);
             
             /*!
-             * Retrieves whether dynamic reordering is currently allowed.
+             * Retrieves whether dynamic reordering is currently allowed (if supported).
              *
              * @return True iff dynamic reordering is currently allowed.
              */
             bool isDynamicReorderingAllowed() const;
             
             /*!
-             * Triggers a reordering of the DDs managed by this manager.
+             * Triggers a reordering of the DDs managed by this manager (if supported).
              */
             void triggerReordering();
             
@@ -179,6 +179,11 @@ namespace storm {
              */
             std::shared_ptr<DdManager<LibraryType> const> asSharedPointer() const;
             
+            /*!
+             * Retrieves the set of meta variables contained in the DD.
+             *
+             * @return All contained meta variables.
+             */
             std::set<storm::expressions::Variable> getAllMetaVariables() const;
             
             /*!
@@ -242,7 +247,18 @@ namespace storm {
              */
             storm::expressions::ExpressionManager& getExpressionManager();
             
+            /*!
+             * Retrieves a pointer to the internal DD manager.
+             *
+             * @return A pointer to the internal DD manager.
+             */
             InternalDdManager<LibraryType>* getInternalDdManagerPointer();
+
+            /*!
+             * Retrieves a pointer to the internal DD manager.
+             *
+             * @return A pointer to the internal DD manager.
+             */
             InternalDdManager<LibraryType> const* getInternalDdManagerPointer() const;
             
             // A mapping from variables to the meta variable information.
diff --git a/src/storage/dd/Odd.cpp b/src/storage/dd/Odd.cpp
index 7bf0f18ab..bac7c2112 100644
--- a/src/storage/dd/Odd.cpp
+++ b/src/storage/dd/Odd.cpp
@@ -59,6 +59,7 @@ namespace storm {
             if (this->isTerminalNode()) {
                 return 1;
             } else {
+                // Since both subtrees have the same height, we only count the height of the else-tree.
                 return 1 + this->getElseSuccessor().getHeight();
             }
         }