From 6a2d75d68dbbd97991d64a4acf7b516b36d337a4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 15 May 2014 21:34:23 +0200
Subject: [PATCH] Some changes in anticipation of integrating MEDDLY.

Former-commit-id: 0f7a71ec9bdfaa979ab071dbf0ba60dbab8d9b83
---
 src/storage/dd/CuddDdManager.h        |   2 +-
 src/storage/dd/CuddDdMetaVariable.cpp |  52 ++++++++++
 src/storage/dd/CuddDdMetaVariable.h   | 138 ++++++++++++++++++++++++++
 src/storage/dd/DdMetaVariable.cpp     |  65 ------------
 src/storage/dd/DdMetaVariable.h       | 136 ++-----------------------
 5 files changed, 197 insertions(+), 196 deletions(-)
 create mode 100644 src/storage/dd/CuddDdMetaVariable.cpp
 create mode 100644 src/storage/dd/CuddDdMetaVariable.h
 delete mode 100644 src/storage/dd/DdMetaVariable.cpp

diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index a4607a57c..14ea4d8a3 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -4,7 +4,7 @@
 #include <unordered_map>
 
 #include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/dd/CuddDdMetaVariable.h"
 #include "src/utility/OsDetection.h"
 
 // Include the C++-interface of CUDD.
diff --git a/src/storage/dd/CuddDdMetaVariable.cpp b/src/storage/dd/CuddDdMetaVariable.cpp
new file mode 100644
index 000000000..b7f45dbe3
--- /dev/null
+++ b/src/storage/dd/CuddDdMetaVariable.cpp
@@ -0,0 +1,52 @@
+#include "src/storage/dd/CuddDdMetaVariable.h"
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+    namespace dd {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+            // Create the cube of all variables of this meta variable.
+            for (auto const& ddVariable : this->ddVariables) {
+                this->cube *= ddVariable;
+            }
+        }
+        
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+            // Create the cube of all variables of this meta variable.
+            for (auto const& ddVariable : this->ddVariables) {
+                this->cube *= ddVariable;
+            }
+        }
+        
+        std::string const& DdMetaVariable<DdType::CUDD>::getName() const {
+            return this->name;
+        }
+        
+        typename DdMetaVariable<DdType::CUDD>::MetaVariableType DdMetaVariable<DdType::CUDD>::getType() const {
+            return this->type;
+        }
+        
+        int_fast64_t DdMetaVariable<DdType::CUDD>::getLow() const {
+            return this->low;
+        }
+
+        int_fast64_t DdMetaVariable<DdType::CUDD>::getHigh() const {
+            return this->high;
+        }
+        
+        std::size_t DdMetaVariable<DdType::CUDD>::getNumberOfDdVariables() const {
+            return this->ddVariables.size();
+        }
+        
+        std::shared_ptr<DdManager<DdType::CUDD>> DdMetaVariable<DdType::CUDD>::getDdManager() const {
+            return this->manager;
+        }
+
+        std::vector<Dd<DdType::CUDD>> const& DdMetaVariable<DdType::CUDD>::getDdVariables() const {
+            return this->ddVariables;
+        }
+        
+        Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCube() const {
+            return this->cube;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storage/dd/CuddDdMetaVariable.h b/src/storage/dd/CuddDdMetaVariable.h
new file mode 100644
index 000000000..b54ca1939
--- /dev/null
+++ b/src/storage/dd/CuddDdMetaVariable.h
@@ -0,0 +1,138 @@
+#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
+#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
+
+#include <memory>
+#include <vector>
+#include <cstdint>
+#include <string>
+
+#include "utility/OsDetection.h"
+#include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace dd {
+        // Forward-declare the DdManager class.
+        template<DdType Type> class DdManager;
+        
+        template<>
+        class DdMetaVariable<DdType::CUDD> {
+        public:
+            // Declare the DdManager class as friend so it can access the internals of a meta variable.
+            friend class DdManager<DdType::CUDD>;
+            friend class Dd<DdType::CUDD>;
+            friend class DdForwardIterator<DdType::CUDD>;
+            
+            // An enumeration for all legal types of meta variables.
+            enum class MetaVariableType { Bool, Int };
+            
+            /*!
+             * Creates an integer meta variable with the given name and range bounds.
+             *
+             * @param name The name of the meta variable.
+             * @param low The lowest value of the range of the variable.
+             * @param high The highest value of the range of the variable.
+             * @param ddVariables The vector of variables used to encode this variable.
+             * @param manager A pointer to the manager that is responsible for this meta variable.
+             */
+            DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            
+            /*!
+             * Creates a boolean meta variable with the given name.
+             * @param name The name of the meta variable.
+             * @param ddVariables The vector of variables used to encode this variable.
+             * @param manager A pointer to the manager that is responsible for this meta variable.
+             */
+            DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            
+            // Explictly generate all default versions of copy/move constructors/assignments.
+            DdMetaVariable(DdMetaVariable const& other) = default;
+			DdMetaVariable& operator=(DdMetaVariable const& other) = default;
+#ifndef WINDOWS
+            DdMetaVariable(DdMetaVariable&& other) = default;
+            DdMetaVariable& operator=(DdMetaVariable&& other) = default;
+#endif
+            
+            /*!
+             * Retrieves the name of the meta variable.
+             *
+             * @return The name of the variable.
+             */
+            std::string const& getName() const;
+            
+            /*!
+             * Retrieves the type of the meta variable.
+             *
+             * @return The type of the meta variable.
+             */
+            MetaVariableType getType() const;
+            
+            /*!
+             * Retrieves the lowest value of the range of the variable.
+             *
+             * @return The lowest value of the range of the variable.
+             */
+            int_fast64_t getLow() const;
+            
+            /*!
+             * Retrieves the highest value of the range of the variable.
+             *
+             * @return The highest value of the range of the variable.
+             */
+            int_fast64_t getHigh() const;
+            
+            /*!
+             * Retrieves the manager that is responsible for this meta variable.
+             *
+             * A pointer to the manager that is responsible for this meta variable.
+             */
+            std::shared_ptr<DdManager<DdType::CUDD>> getDdManager() const;
+            
+            /*!
+             * Retrieves the number of DD variables for this meta variable.
+             *
+             * @return The number of DD variables for this meta variable.
+             */
+            std::size_t getNumberOfDdVariables() const;
+            
+        private:
+            /*!
+             * Retrieves the variables used to encode the meta variable.
+             *
+             * @return A vector of variables used to encode the meta variable.
+             */
+            std::vector<Dd<DdType::CUDD>> const& getDdVariables() const;
+            
+            /*!
+             * Retrieves the cube of all variables that encode this meta variable.
+             *
+             * @return The cube of all variables that encode this meta variable.
+             */
+            Dd<DdType::CUDD> const& getCube() const;
+            
+            // The name of the meta variable.
+            std::string name;
+            
+            // The type of the variable.
+            MetaVariableType type;
+            
+            // The lowest value of the range of the variable.
+            int_fast64_t low;
+            
+            // The highest value of the range of the variable.
+            int_fast64_t high;
+            
+            // The vector of variables that are used to encode the meta variable.
+            std::vector<Dd<DdType::CUDD>> ddVariables;
+            
+            // The cube consisting of all variables that encode the meta variable.
+            Dd<DdType::CUDD> cube;
+            
+            // A pointer to the manager responsible for this meta variable.
+            std::shared_ptr<DdManager<DdType::CUDD>> manager;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp
deleted file mode 100644
index 453b83cc8..000000000
--- a/src/storage/dd/DdMetaVariable.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-#include "src/storage/dd/DdMetaVariable.h"
-#include "src/storage/dd/CuddDdManager.h"
-
-namespace storm {
-    namespace dd {
-        template<DdType Type>
-        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
-            // Create the cube of all variables of this meta variable.
-            for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
-            }
-        }
-        
-        template<DdType Type>
-        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
-            // Create the cube of all variables of this meta variable.
-            for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
-            }
-        }
-        
-        template<DdType Type>
-        std::string const& DdMetaVariable<Type>::getName() const {
-            return this->name;
-        }
-        
-        template<DdType Type>
-        typename DdMetaVariable<Type>::MetaVariableType DdMetaVariable<Type>::getType() const {
-            return this->type;
-        }
-        
-        template<DdType Type>
-        int_fast64_t DdMetaVariable<Type>::getLow() const {
-            return this->low;
-        }
-
-        template<DdType Type>
-        int_fast64_t DdMetaVariable<Type>::getHigh() const {
-            return this->high;
-        }
-        
-        template<DdType Type>
-        std::size_t DdMetaVariable<Type>::getNumberOfDdVariables() const {
-            return this->ddVariables.size();
-        }
-        
-        template<DdType Type>
-        std::shared_ptr<DdManager<Type>> DdMetaVariable<Type>::getDdManager() const {
-            return this->manager;
-        }
-
-        template<DdType Type>
-        std::vector<Dd<Type>> const& DdMetaVariable<Type>::getDdVariables() const {
-            return this->ddVariables;
-        }
-        
-        template<DdType Type>
-        Dd<Type> const& DdMetaVariable<Type>::getCube() const {
-            return this->cube;
-        }
-        
-        // Explicitly instantiate DdMetaVariable.
-        template class DdMetaVariable<DdType::CUDD>;
-    }
-}
\ No newline at end of file
diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h
index 47936d805..b85b23c1c 100644
--- a/src/storage/dd/DdMetaVariable.h
+++ b/src/storage/dd/DdMetaVariable.h
@@ -1,137 +1,13 @@
-#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
-#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
+#ifndef STORM_STORAGE_DD_DDMETAVARIBLE_H_
+#define STORM_STORAGE_DD_DDMETAVARIBLE_H_
 
-#include <memory>
-#include <vector>
-#include <cstdint>
-#include <string>
-
-#include "utility/OsDetection.h"
-#include "src/storage/dd/CuddDd.h"
-#include "src/storage/expressions/Expression.h"
+#include "src/storage/dd/DdType.h"
 
 namespace storm {
     namespace dd {
-        // Forward-declare the DdManager class.
-        template<DdType Type> class DdManager;
-        
-        template <DdType Type>
-        class DdMetaVariable {
-        public:
-            // Declare the DdManager class as friend so it can access the internals of a meta variable.
-            friend class DdManager<Type>;
-            friend class Dd<Type>;
-            friend class DdForwardIterator<Type>;
-            
-            // An enumeration for all legal types of meta variables.
-            enum class MetaVariableType { Bool, Int };
-            
-            /*!
-             * Creates an integer meta variable with the given name and range bounds.
-             *
-             * @param name The name of the meta variable.
-             * @param low The lowest value of the range of the variable.
-             * @param high The highest value of the range of the variable.
-             * @param ddVariables The vector of variables used to encode this variable.
-             * @param manager A pointer to the manager that is responsible for this meta variable.
-             */
-            DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
-            
-            /*!
-             * Creates a boolean meta variable with the given name.
-             * @param name The name of the meta variable.
-             * @param ddVariables The vector of variables used to encode this variable.
-             * @param manager A pointer to the manager that is responsible for this meta variable.
-             */
-            DdMetaVariable(std::string const& name, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
-            
-            // Explictly generate all default versions of copy/move constructors/assignments.
-            DdMetaVariable(DdMetaVariable const& other) = default;
-			DdMetaVariable& operator=(DdMetaVariable const& other) = default;
-#ifndef WINDOWS
-            DdMetaVariable(DdMetaVariable&& other) = default;
-            DdMetaVariable& operator=(DdMetaVariable&& other) = default;
-#endif
-            
-            /*!
-             * Retrieves the name of the meta variable.
-             *
-             * @return The name of the variable.
-             */
-            std::string const& getName() const;
-            
-            /*!
-             * Retrieves the type of the meta variable.
-             *
-             * @return The type of the meta variable.
-             */
-            MetaVariableType getType() const;
-            
-            /*!
-             * Retrieves the lowest value of the range of the variable.
-             *
-             * @return The lowest value of the range of the variable.
-             */
-            int_fast64_t getLow() const;
-            
-            /*!
-             * Retrieves the highest value of the range of the variable.
-             *
-             * @return The highest value of the range of the variable.
-             */
-            int_fast64_t getHigh() const;
-            
-            /*!
-             * Retrieves the manager that is responsible for this meta variable.
-             *
-             * A pointer to the manager that is responsible for this meta variable.
-             */
-            std::shared_ptr<DdManager<Type>> getDdManager() const;
-            
-            /*!
-             * Retrieves the number of DD variables for this meta variable.
-             *
-             * @return The number of DD variables for this meta variable.
-             */
-            std::size_t getNumberOfDdVariables() const;
-            
-        private:
-            /*!
-             * Retrieves the variables used to encode the meta variable.
-             *
-             * @return A vector of variables used to encode the meta variable.
-             */
-            std::vector<Dd<Type>> const& getDdVariables() const;
-            
-            /*!
-             * Retrieves the cube of all variables that encode this meta variable.
-             *
-             * @return The cube of all variables that encode this meta variable.
-             */
-            Dd<Type> const& getCube() const;
-            
-            // The name of the meta variable.
-            std::string name;
-            
-            // The type of the variable.
-            MetaVariableType type;
-            
-            // The lowest value of the range of the variable.
-            int_fast64_t low;
-            
-            // The highest value of the range of the variable.
-            int_fast64_t high;
-            
-            // The vector of variables that are used to encode the meta variable.
-            std::vector<Dd<Type>> ddVariables;
-            
-            // The cube consisting of all variables that encode the meta variable.
-            Dd<Type> cube;
-            
-            // A pointer to the manager responsible for this meta variable.
-            std::shared_ptr<DdManager<Type>> manager;
-        };
+        // Declare DdMetaVariable class so we can then specialize it for the different DD types.
+        template<DdType Type> class DdMetaVariable;
     }
 }
 
-#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DD_DDMETAVARIBLE_H_ */
\ No newline at end of file