diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h
index 0931e1ca5..85a0847af 100644
--- a/src/solver/GlpkLpSolver.h
+++ b/src/solver/GlpkLpSolver.h
@@ -184,7 +184,7 @@ namespace storm {
throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
- virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
+ virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 087382c71..fd26a782c 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -3,6 +3,7 @@
#include <algorithm>
#include "src/storage/dd/CuddDdManager.h"
+#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/settings/Settings.h"
@@ -49,17 +50,9 @@ namespace storm {
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
- // Check whether the meta variable exists.
- if (!this->hasMetaVariable(metaVariableName)) {
- throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
- }
-
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
- // Check whether the value is legal for this meta variable.
- if (value < metaVariable.getLow() || value > metaVariable.getHigh()) {
- throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'.";
- }
+ LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'.");
// Now compute the encoding relative to the low value of the meta variable.
value -= metaVariable.getLow();
@@ -85,11 +78,6 @@ namespace storm {
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(std::string const& metaVariableName) {
- // Check whether the meta variable exists.
- if (!this->hasMetaVariable(metaVariableName)) {
- throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
- }
-
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
Dd<DdType::CUDD> result = this->getZero();
@@ -101,11 +89,6 @@ namespace storm {
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(std::string const& metaVariableName) {
- // Check whether the meta variable exists.
- if (!this->hasMetaVariable(metaVariableName)) {
- throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
- }
-
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
Dd<DdType::CUDD> result = this->getZero();
@@ -116,91 +99,57 @@ namespace storm {
}
void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+ // Check whether the variable name is legal.
+ LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+
// Check whether a meta variable already exists.
- if (this->hasMetaVariable(name)) {
- throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
- }
+ LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
// Check that the range is legal.
- if (high == low) {
- throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
- }
+ LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
std::vector<Dd<DdType::CUDD>> variables;
+ std::vector<Dd<DdType::CUDD>> variablesPrime;
for (std::size_t i = 0; i < numberOfBits; ++i) {
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
+ variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name + "'"}));
+ }
+
+ // Now group the non-primed and primed variable.
+ for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
+ this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
}
metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
+ metaVariableMap.emplace(name + "'", DdMetaVariable<DdType::CUDD>(name + "'", low, high, variablesPrime, this->shared_from_this()));
}
void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
+ // Check whether the variable name is legal.
+ LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+
// Check whether a meta variable already exists.
- if (this->hasMetaVariable(name)) {
- throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
- }
+ LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
std::vector<Dd<DdType::CUDD>> variables;
+ std::vector<Dd<DdType::CUDD>> variablesPrime;
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
-
- metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
- }
-
- void DdManager<DdType::CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup) {
- // Make sure that at least one meta variable is added.
- if (names.size() == 0) {
- throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
- }
-
- // Check that there are no duplicate names in the given name vector.
- std::vector<std::string> nameCopy(names);
- std::sort(nameCopy.begin(), nameCopy.end());
- if (std::adjacent_find(nameCopy.begin(), nameCopy.end()) != nameCopy.end()) {
- throw storm::exceptions::InvalidArgumentException() << "Cannot add duplicate meta variables.";
- }
-
- // Check that the range is legal.
- if (high == low) {
- throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
- }
+ variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name + "'"}));
- // Check whether a meta variable already exists.
- for (auto const& metaVariableName : names) {
- if (this->hasMetaVariable(metaVariableName)) {
- throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists.";
- }
- }
-
- // Add the variables in interleaved order.
- std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
- std::vector<std::vector<Dd<DdType::CUDD>>> variables(names.size());
- for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
- for (uint_fast64_t i = 0; i < names.size(); ++i) {
- variables[i].emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
- }
- }
-
- // If required, we group the bits on the same layer of the interleaved meta variables.
- if (fixedGroup) {
- for (uint_fast64_t i = 0; i < names.size(); ++i) {
- this->getCuddManager().MakeTreeNode(variables[i].front().getCuddAdd().NodeReadIndex(), names.size(), MTR_FIXED);
- }
- }
+ // Now group the non-primed and primed variable.
+ this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
- // Now add the meta variables.
- for (uint_fast64_t i = 0; i < names.size(); ++i) {
- metaVariableMap.emplace(names[i], DdMetaVariable<DdType::CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
- }
+ metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
+ metaVariableMap.emplace(name + "'", DdMetaVariable<DdType::CUDD>(name + "'", variablesPrime, this->shared_from_this()));
}
DdMetaVariable<DdType::CUDD> const& DdManager<DdType::CUDD>::getMetaVariable(std::string const& metaVariableName) const {
auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
- if (!this->hasMetaVariable(metaVariableName)) {
- throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
- }
+ // Check whether the meta variable exists.
+ LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'.");
return nameVariablePair->second;
}
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 6fba4d254..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.
@@ -16,6 +16,7 @@ namespace storm {
class DdManager<DdType::CUDD> : public std::enable_shared_from_this<DdManager<DdType::CUDD>> {
public:
friend class Dd<DdType::CUDD>;
+ friend class DdForwardIterator<DdType::CUDD>;
/*!
* Creates an empty manager without any meta variables.
@@ -83,7 +84,7 @@ namespace storm {
/*!
* Adds an integer meta variable with the given name and range.
*
- * @param name The name of the meta variable.
+ * @param name The (non-empty) 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.
*/
@@ -92,30 +93,10 @@ namespace storm {
/*!
* Adds a boolean meta variable with the given name.
*
- * @param name The name of the meta variable.
+ * @param name The (non-empty) name of the meta variable.
*/
void addMetaVariable(std::string const& name);
- /*!
- * Adds integer meta variables with the given names and (equal) range and arranges the DD variables in an
- * interleaved order.
- *
- * @param names The names of the variables.
- * @param low The lowest value of the ranges of the variables.
- * @param high The highest value of the ranges of the variables.
- * @param fixedGroup If set to true, the interleaved bits of the meta variable are always kept together as
- * a group during a potential reordering.
- */
- void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup = 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<DdType::CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
-
/*!
* Retrieves the names of all meta variables that have been added to the manager.
*
@@ -157,6 +138,15 @@ namespace storm {
*/
void triggerReordering();
+ protected:
+ /*!
+ * 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<DdType::CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
+
private:
/*!
* Retrieves a list of names of the DD variables in the order of their index.
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
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index ce40c94d1..f39e4ad48 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -38,26 +38,18 @@ TEST(CuddDdManager, Constants) {
TEST(CuddDdManager, AddGetMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
- EXPECT_EQ(1, manager->getNumberOfMetaVariables());
+ EXPECT_EQ(2, manager->getNumberOfMetaVariables());
- std::vector<std::string> names = {"x", "x'"};
- ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
+ ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
- names = {"y", "y"};
- ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
+ ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
+ EXPECT_EQ(4, manager->getNumberOfMetaVariables());
- names = {"y", "y'"};
- ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3));
- EXPECT_EQ(3, manager->getNumberOfMetaVariables());
-
- EXPECT_FALSE(manager->hasMetaVariable("x'"));
+ EXPECT_TRUE(manager->hasMetaVariable("x'"));
EXPECT_TRUE(manager->hasMetaVariable("y'"));
- std::set<std::string> metaVariableSet = {"x", "y", "y'"};
+ std::set<std::string> metaVariableSet = {"x", "x'", "y", "y'"};
EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
-
- ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
- ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
}
TEST(CuddDdManager, EncodingTest) {
@@ -99,20 +91,6 @@ TEST(CuddDdManager, IdentityTest) {
EXPECT_EQ(21, range.getNodeCount());
}
-TEST(CuddDdMetaVariable, AccessorTest) {
- std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
- manager->addMetaVariable("x", 1, 9);
- EXPECT_EQ(1, manager->getNumberOfMetaVariables());
- ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
- storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x");
-
- EXPECT_EQ(1, metaVariableX.getLow());
- EXPECT_EQ(9, metaVariableX.getHigh());
- EXPECT_EQ("x", metaVariableX.getName());
- EXPECT_EQ(manager, metaVariableX.getDdManager());
- EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables());
-}
-
TEST(CuddDd, OperatorTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
@@ -200,7 +178,7 @@ TEST(CuddDd, OperatorTest) {
TEST(CuddDd, AbstractionTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
- manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+ manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
storm::dd::Dd<storm::dd::DdType::CUDD> dd3;
@@ -246,7 +224,7 @@ TEST(CuddDd, AbstractionTest) {
TEST(CuddDd, SwapTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
- manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+ manager->addMetaVariable("x", 1, 9);
manager->addMetaVariable("z", 2, 8);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
@@ -259,7 +237,7 @@ TEST(CuddDd, SwapTest) {
TEST(CuddDd, MultiplyMatrixTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
- manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+ manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'"));
storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getRange("x'");