Started writing the DD abstraction layer.

Former-commit-id: 8720a38b17

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})

CPackConfig.cmake

@@ -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)

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();

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_ */

src/storage/dd/CuddDdManager.cpp

@@ -0,0 +1,7 @@
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+    namespace dd {
+        
+    }
+}

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_ */

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_ */

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_ */

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>;
+    }
+}

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_ */