diff --git a/CMakeLists.txt b/CMakeLists.txt
index aa1e269c0..8942c984f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -242,7 +242,8 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR
file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp)
file(GLOB_RECURSE STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp)
file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp)
-file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
+file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
+file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp)
file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp)
@@ -275,6 +276,7 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES})
source_group(settings FILES ${STORM_SETTINGS_FILES})
source_group(solver FILES ${STORM_SOLVER_FILES})
source_group(storage FILES ${STORM_STORAGE_FILES})
+source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES})
source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES})
source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES})
diff --git a/CPackConfig.cmake b/CPackConfig.cmake
deleted file mode 100644
index 5ce6c0f53..000000000
--- a/CPackConfig.cmake
+++ /dev/null
@@ -1,27 +0,0 @@
-include(InstallRequiredSystemLibraries)
-
-# For help take a look at:
-# http://www.cmake.org/Wiki/CMake:CPackConfiguration
-
-### general settings
-set(CPACK_PACKAGE_NAME "StoRM")
-set(CPACK_PACKAGE_VENDOR "i2 RWTH Aachen University")
-set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Stochastic Reward Model Checker - An extensible model checker written in C++.")
-
-set(CPACK_RESOURCE_FILE_LICENSE "${CMAKE_SOURCE_DIR}/LICENSE")
-
-### versions
-set(CPACK_PACKAGE_VERSION_MAJOR "${STORM_CPP_VERSION_MAJOR}")
-set(CPACK_PACKAGE_VERSION_MINOR "${STORM_CPP_VERSION_MINOR}")
-set(CPACK_PACKAGE_VERSION_PATCH "${STORM_CPP_VERSION_PATCH}")
-set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION_MAJOR}.${CPACK_PACKAGE_VERSION_MINOR}.${CPACK_PACKAGE_VERSION_PATCH}-${STORM_CPP_VERSION_HASH}")
-
-set(CPACK_GENERATOR "ZIP")
-set(CPACK_PACKAGE_INSTALL_DIRECTORY "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}")
-
-### source package settings
-set(CPACK_SOURCE_GENERATOR "ZIP")
-set(CPACK_SOURCE_IGNORE_FILES "~$;[.]swp$;/[.]svn/;/[.]git/;.gitignore;/build/;tags;cscope.*")
-set(CPACK_SOURCE_PACKAGE_FILE_NAME "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}-src")
-
-include(CPack)
\ No newline at end of file
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 3ec8256ed..027369182 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -1021,7 +1021,7 @@ namespace storm {
LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.");
throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.";
}
- bool strictBound = !probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS;
+ bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS);
// Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
double bound = probBoundFormula->getBound();
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
new file mode 100644
index 000000000..d608b07e5
--- /dev/null
+++ b/src/storage/dd/CuddDd.h
@@ -0,0 +1,126 @@
+#ifndef STORM_STORAGE_DD_CUDDDD_H_
+#define STORM_STORAGE_DD_CUDDDD_H_
+
+#include "src/storage/dd/Dd.h"
+#include "src/storage/dd/CuddDdManager.h"
+
+// Include the C++-interface of CUDD.
+#include "cuddObj.hh"
+
+namespace storm {
+ namespace dd {
+
+ template<>
+ class Dd<CUDD> {
+ /*!
+ * Creates a DD that encapsulates the given CUDD ADD.
+ *
+ * @param cuddAdd The CUDD ADD to store.
+ */
+ Dd(ADD cuddAdd);
+
+ // Instantiate all copy/move constructors/assignments with the default implementation.
+ Dd(Dd<CUDD> const& other) = default;
+ Dd(Dd<CUDD>&& other) = default;
+ Dd& operator=(Dd<CUDD> const& other) = default;
+ Dd& operator=(Dd<CUDD>&& other) = default;
+
+ /*!
+ * Adds the two DDs.
+ *
+ * @param other The DD to add to the current one.
+ * @return The result of the addition.
+ */
+ Dd<CUDD> operator+(Dd<CUDD> const& other) const;
+
+ /*!
+ * Adds the given DD to the current one.
+ *
+ * @param other The DD to add to the current one.
+ * @return A reference to the current DD after the operation.
+ */
+ Dd<CUDD>& operator+=(Dd<CUDD> const& other);
+
+ /*!
+ * Multiplies the two DDs.
+ *
+ * @param other The DD to multiply with the current one.
+ * @return The result of the multiplication.
+ */
+ Dd<CUDD> operator*(Dd<CUDD> const& other) const;
+
+ /*!
+ * Multiplies the given DD with the current one and assigns the result to the current DD.
+ *
+ * @param other The DD to multiply with the current one.
+ * @return A reference to the current DD after the operation.
+ */
+ Dd<CUDD>& operator*=(Dd<CUDD> const& other);
+
+ /*!
+ * Subtracts the given DD from the current one.
+ *
+ * @param other The DD to subtract from the current one.
+ * @return The result of the subtraction.
+ */
+ Dd<CUDD> operator-(Dd<CUDD> const& other) const;
+
+ /*!
+ * Subtracts the given DD from the current one and assigns the result to the current DD.
+ *
+ * @param other The DD to subtract from the current one.
+ * @return A reference to the current DD after the operation.
+ */
+ Dd<CUDD>& operator-=(Dd<CUDD> const& other);
+
+ /*!
+ * Divides the current DD by the given one.
+ *
+ * @param other The DD by which to divide the current one.
+ * @return The result of the division.
+ */
+ Dd<CUDD> operator/(Dd<CUDD> const& other) const;
+
+ /*!
+ * Divides the current DD by the given one and assigns the result to the current DD.
+ *
+ * @param other The DD by which to divide the current one.
+ * @return A reference to the current DD after the operation.
+ */
+ Dd<CUDD>& operator/=(Dd<CUDD> const& other);
+
+ /*!
+ * Retrieves the logical complement of the current DD. The result will map all encodings with a value
+ * unequal to zero to false and all others to true.
+ *
+ * @return The logical complement of the current DD.
+ */
+ Dd<CUDD> operator~() const;
+
+ /*!
+ * Logically complements the current DD. The result will map all encodings with a value
+ * unequal to zero to false and all others to true.
+ */
+ void complement();
+
+ /*!
+ * Retrieves the manager that is responsible for this DD.
+ *
+ * A pointer to the manager that is responsible for this DD.
+ */
+ std::shared_ptr<DdManager<CUDD>> getDdManager() const;
+
+ private:
+ // A pointer to the manager responsible for this DD.
+ std::shared_ptr<DdManager<CUDD>> ddManager;
+
+ // The ADD created by CUDD.
+ ADD cuddAdd;
+
+ // The names of all meta variables that appear in this DD.
+ std::unordered_set<std::string> containedMetaVariableNames;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_DD_CUDDDD_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
new file mode 100644
index 000000000..af75ca402
--- /dev/null
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -0,0 +1,7 @@
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+ namespace dd {
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
new file mode 100644
index 000000000..8c47b4b2d
--- /dev/null
+++ b/src/storage/dd/CuddDdManager.h
@@ -0,0 +1,98 @@
+#ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_
+#define STORM_STORAGE_DD_CUDDDDMANAGER_H_
+
+#include <unordered_set>
+#include <unordered_map>
+
+#include "src/storage/dd/DdManager.h"
+
+// Include the C++-interface of CUDD.
+#include "cuddObj.hh"
+
+namespace storm {
+ namespace dd {
+ // To break the cylic dependencies, we need to forward-declare the other DD-related classes.
+ template<DdType Type> class DdMetaVariable;
+ template<DdType Type> class Dd;
+
+ template<>
+ class DdManager<CUDD> : std::enable_shared_from_this<DdManager<CUDD>> {
+ /*!
+ * Creates an empty manager without any meta variables.
+ */
+ DdManager();
+
+ // Explictly forbid copying a DdManager, but allow moving it.
+ DdManager(DdManager<CUDD> const& other) = delete;
+ DdManager(DdManager<CUDD>&& other) = default;
+ DdManager<CUDD>& operator=(DdManager<CUDD> const& other) = delete;
+ DdManager<CUDD>& operator=(DdManager<CUDD>&& other) = default;
+
+ /*!
+ * Retrieves a DD representing the constant one function.
+ *
+ * @return A DD representing the constant one function.
+ */
+ Dd<CUDD> getOne();
+
+ /*!
+ * Retrieves a DD representing the constant zero function.
+ *
+ * @return A DD representing the constant zero function.
+ */
+ Dd<CUDD> getZero();
+
+ /*!
+ * Retrieves a DD representing the constant function with the given value.
+ *
+ * @return A DD representing the constant function with the given value.
+ */
+ Dd<CUDD> getConstant(double value);
+
+ /*!
+ * Adds a meta variable with the given name and range.
+ *
+ * @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 addSuccessorVariable If set, a second meta variable is added. This can then be used, for example,
+ * to encode the value of the meta variable in a successor state.
+ * @param useInterleavedVariableOrdering If set, the variables used for the successor meta variable are
+ * interleaved with the ones for the added meta variable.
+ */
+ void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, bool addSuccessorVariable = false, bool useInterleavedVariableOrdering = true);
+
+ /*!
+ * Retrieves the meta variable with the given name if it exists.
+ *
+ * @param metaVariableName The name of the meta variable to retrieve.
+ * @return The meta variable with the given name.
+ */
+ DdMetaVariable<CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
+
+ /*!
+ * Retrieves the successor meta variable of the one with the given name if it exists.
+ *
+ * @param metaVariableName The name of the meta variable whose successor meta variable to retrieve.
+ * @return The successor meta variable of the one with the given name.
+ */
+ DdMetaVariable<CUDD> const& getSuccessorMetaVariable(std::string const& metaVariableName) const;
+
+ /*!
+ * Retrieves the names of all meta variables that have been added to the manager.
+ *
+ * @return The set of all meta variable names of the manager.
+ */
+ std::unordered_set<std::string> getAllMetaVariableNames();
+
+ private:
+ // A mapping from variable names to the meta variable information.
+ std::unordered_map<std::string, DdMetaVariable<CUDD>> metaVariableMap;
+
+ // The manager responsible for the DDs created/modified with this DdManager.
+ Cudd cuddManager;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_DD_CUDDDDMANAGER_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
new file mode 100644
index 000000000..bc7075f46
--- /dev/null
+++ b/src/storage/dd/Dd.h
@@ -0,0 +1,13 @@
+#ifndef STORM_STORAGE_DD_DD_H_
+#define STORM_STORAGE_DD_DD_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+ namespace dd {
+ // Declare Dd class so we can then specialize it for the different DD types.
+ template<DdType Type> class Dd;
+ }
+}
+
+#endif /* STORM_STORAGE_DD_DD_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
new file mode 100644
index 000000000..53fde64bb
--- /dev/null
+++ b/src/storage/dd/DdManager.h
@@ -0,0 +1,13 @@
+#ifndef STORM_STORAGE_DD_DDMANAGER_H_
+#define STORM_STORAGE_DD_DDMANAGER_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+ namespace dd {
+ // Declare DdManager class so we can then specialize it for the different DD types.
+ template<DdType Type> class DdManager;
+ }
+}
+
+#endif /* STORM_STORAGE_DD_DDMANAGER_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp
new file mode 100644
index 000000000..72c2be15f
--- /dev/null
+++ b/src/storage/dd/DdMetaVariable.cpp
@@ -0,0 +1,38 @@
+#include "src/storage/dd/DdMetaVariable.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), low(low), high(high), ddVariables(ddVariables), manager(manager) {
+ // Intentionally left empty.
+ }
+
+ template<DdType Type>
+ std::string const& DdMetaVariable<Type>::getName() const {
+ return this->name;
+ }
+
+ 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::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<CUDD>;
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h
new file mode 100644
index 000000000..2631143f2
--- /dev/null
+++ b/src/storage/dd/DdMetaVariable.h
@@ -0,0 +1,101 @@
+#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
+#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
+
+#include <memory>
+#include <vector>
+#include <cstdint>
+#include <string>
+
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddDd.h"
+
+namespace storm {
+ namespace dd {
+
+ template <DdType Type>
+ class DdMetaVariable {
+ // Declare the other DD-related classes as friends so they can access the internals of a meta variable.
+ friend class Dd<Type>;
+
+ /*!
+ * Creates a meta variable with the given name, 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);
+
+ // Explictly generate all default versions of copy/move constructors/assignments.
+ DdMetaVariable(DdMetaVariable const& other) = default;
+ DdMetaVariable(DdMetaVariable&& other) = default;
+ DdMetaVariable& operator=(DdMetaVariable const& other) = default;
+ DdMetaVariable& operator=(DdMetaVariable&& other) = default;
+
+ /*!
+ * Retrieves the name of the meta variable.
+ *
+ * @return The name of the variable.
+ */
+ std::string const& getName() 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;
+
+ 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 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;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */
\ No newline at end of file