sjunges
11 years ago
30 changed files with 1379 additions and 37 deletions
-
1.gitignore
-
13CMakeLists.txt
-
0StormCPackConfig.cmake
-
7src/adapters/ExplicitModelAdapter.h
-
2src/adapters/SymbolicModelAdapter.h
-
10src/counterexamples/MILPMinimalLabelSetGenerator.h
-
17src/ir/Module.cpp
-
6src/ir/Module.h
-
2src/models/MarkovAutomaton.h
-
2src/solver/GlpkLpSolver.cpp
-
1src/solver/GmmxxLinearEquationSolver.cpp
-
1src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
-
1src/solver/NativeLinearEquationSolver.cpp
-
1src/solver/NativeNondeterministicLinearEquationSolver.cpp
-
2src/storage/BitVector.cpp
-
1src/storage/SparseMatrix.cpp
-
354src/storage/dd/CuddDd.cpp
-
407src/storage/dd/CuddDd.h
-
149src/storage/dd/CuddDdManager.cpp
-
141src/storage/dd/CuddDdManager.h
-
13src/storage/dd/Dd.h
-
13src/storage/dd/DdManager.h
-
52src/storage/dd/DdMetaVariable.cpp
-
114src/storage/dd/DdMetaVariable.h
-
12src/storage/dd/DdType.h
-
3src/storm.cpp
-
1src/utility/vector.h
-
7storm-config.h.in
-
12storm-version.h.in
-
71test/functional/storage/CuddDdTest.cpp
@ -0,0 +1,354 @@ |
|||
#include <algorithm>
|
|||
|
|||
#include "src/storage/dd/CuddDd.h"
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
Dd<CUDD>::Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool Dd<CUDD>::operator==(Dd<CUDD> const& other) const { |
|||
return this->getCuddAdd() == other.getCuddAdd(); |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::operator+(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result += other; |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) { |
|||
this->getCuddAdd() += other.getCuddAdd(); |
|||
|
|||
// Join the variable sets of the two participating DDs.
|
|||
this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::operator*(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result *= other; |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) { |
|||
this->getCuddAdd() *= other.getCuddAdd(); |
|||
|
|||
// Join the variable sets of the two participating DDs.
|
|||
this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::operator-(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result -= other; |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) { |
|||
this->getCuddAdd() -= other.getCuddAdd(); |
|||
|
|||
// Join the variable sets of the two participating DDs.
|
|||
this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::operator/(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result /= other; |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) { |
|||
this->getCuddAdd().Divide(other.getCuddAdd()); |
|||
|
|||
// Join the variable sets of the two participating DDs.
|
|||
this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::operator~() const { |
|||
Dd<CUDD> result(*this); |
|||
result.complement(); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD>& Dd<CUDD>::complement() { |
|||
this->getCuddAdd() = ~this->getCuddAdd(); |
|||
return *this; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::equals(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().Equals(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::notEquals(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().NotEquals(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::less(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().LessThan(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::lessOrEqual(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().LessThanOrEqual(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::greater(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().GreaterThan(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::greaterOrEqual(Dd<CUDD> const& other) const { |
|||
Dd<CUDD> result(*this); |
|||
result.getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()); |
|||
return result; |
|||
} |
|||
|
|||
void Dd<CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) { |
|||
Dd<CUDD> cubeDd(this->getDdManager()->getOne()); |
|||
|
|||
for (auto const& metaVariableName : metaVariableNames) { |
|||
// First check whether the DD contains the meta variable and erase it, if this is the case.
|
|||
if (!this->containsMetaVariable(metaVariableName)) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; |
|||
} |
|||
this->getContainedMetaVariableNames().erase(metaVariableName); |
|||
|
|||
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); |
|||
cubeDd *= metaVariable.getCube(); |
|||
} |
|||
|
|||
this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); |
|||
} |
|||
|
|||
void Dd<CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) { |
|||
Dd<CUDD> cubeDd(this->getDdManager()->getOne()); |
|||
|
|||
for (auto const& metaVariableName : metaVariableNames) { |
|||
// First check whether the DD contains the meta variable and erase it, if this is the case.
|
|||
if (!this->containsMetaVariable(metaVariableName)) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; |
|||
} |
|||
this->getContainedMetaVariableNames().erase(metaVariableName); |
|||
|
|||
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); |
|||
cubeDd *= metaVariable.getCube(); |
|||
} |
|||
|
|||
this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); |
|||
} |
|||
|
|||
void Dd<CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) { |
|||
Dd<CUDD> cubeDd(this->getDdManager()->getOne()); |
|||
|
|||
for (auto const& metaVariableName : metaVariableNames) { |
|||
// First check whether the DD contains the meta variable and erase it, if this is the case.
|
|||
if (!this->containsMetaVariable(metaVariableName)) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; |
|||
} |
|||
this->getContainedMetaVariableNames().erase(metaVariableName); |
|||
|
|||
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); |
|||
cubeDd *= metaVariable.getCube(); |
|||
} |
|||
|
|||
this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); |
|||
} |
|||
|
|||
void Dd<CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) { |
|||
Dd<CUDD> cubeDd(this->getDdManager()->getOne()); |
|||
|
|||
for (auto const& metaVariableName : metaVariableNames) { |
|||
// First check whether the DD contains the meta variable and erase it, if this is the case.
|
|||
if (!this->containsMetaVariable(metaVariableName)) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; |
|||
} |
|||
this->getContainedMetaVariableNames().erase(metaVariableName); |
|||
|
|||
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); |
|||
cubeDd *= metaVariable.getCube(); |
|||
} |
|||
|
|||
this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); |
|||
} |
|||
|
|||
void Dd<CUDD>::swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs) { |
|||
std::vector<ADD> from; |
|||
std::vector<ADD> to; |
|||
for (auto const& metaVariablePair : metaVariablePairs) { |
|||
DdMetaVariable<CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); |
|||
DdMetaVariable<CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); |
|||
|
|||
// Check if it's legal so swap the meta variables.
|
|||
if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; |
|||
} |
|||
|
|||
// Keep track of the contained meta variables in the DD.
|
|||
bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); |
|||
bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); |
|||
if (containsVariable1 && !containsVariable2) { |
|||
this->removeContainedMetaVariable(metaVariablePair.first); |
|||
this->addContainedMetaVariable(metaVariablePair.second); |
|||
} else if (!containsVariable1 && containsVariable2) { |
|||
this->removeContainedMetaVariable(metaVariablePair.second); |
|||
this->addContainedMetaVariable(metaVariablePair.first); |
|||
} |
|||
|
|||
// Add the variables to swap to the corresponding vectors.
|
|||
for (auto const& ddVariable : variable1.getDdVariables()) { |
|||
from.push_back(ddVariable.getCuddAdd()); |
|||
} |
|||
for (auto const& ddVariable : variable2.getDdVariables()) { |
|||
to.push_back(ddVariable.getCuddAdd()); |
|||
} |
|||
} |
|||
|
|||
// Finally, call CUDD to swap the variables.
|
|||
this->getCuddAdd().SwapVariables(from, to); |
|||
} |
|||
|
|||
Dd<CUDD> Dd<CUDD>::multiplyMatrix(Dd<CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) { |
|||
std::vector<ADD> summationDdVariables; |
|||
|
|||
// Create the CUDD summation variables.
|
|||
for (auto const& metaVariableName : summationMetaVariableNames) { |
|||
for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariableName).getDdVariables()) { |
|||
summationDdVariables.push_back(ddVariable.getCuddAdd()); |
|||
} |
|||
} |
|||
|
|||
std::set<std::string> unionOfMetaVariableNames; |
|||
std::set_union(this->getContainedMetaVariableNames().begin(), this->getContainedMetaVariableNames().end(), otherMatrix.getContainedMetaVariableNames().begin(), otherMatrix.getContainedMetaVariableNames().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); |
|||
std::set<std::string> containedMetaVariableNames; |
|||
std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); |
|||
|
|||
return Dd<CUDD>(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); |
|||
} |
|||
|
|||
|
|||
uint_fast64_t Dd<CUDD>::getNonZeroCount() const { |
|||
std::size_t numberOfDdVariables = 0; |
|||
for (auto const& metaVariableName : this->containedMetaVariableNames) { |
|||
numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); |
|||
} |
|||
return static_cast<uint_fast64_t>(this->cuddAdd.CountMinterm(static_cast<int>(numberOfDdVariables))); |
|||
} |
|||
|
|||
uint_fast64_t Dd<CUDD>::getLeafCount() const { |
|||
return static_cast<uint_fast64_t>(this->cuddAdd.CountLeaves()); |
|||
} |
|||
|
|||
uint_fast64_t Dd<CUDD>::getNodeCount() const { |
|||
return static_cast<uint_fast64_t>(this->cuddAdd.nodeCount()); |
|||
} |
|||
|
|||
double Dd<CUDD>::getMin() const { |
|||
ADD constantMinAdd = this->getCuddAdd().FindMin(); |
|||
return static_cast<double>(Cudd_V(constantMinAdd.getNode())); |
|||
} |
|||
|
|||
double Dd<CUDD>::getMax() const { |
|||
ADD constantMaxAdd = this->getCuddAdd().FindMax(); |
|||
return static_cast<double>(Cudd_V(constantMaxAdd.getNode())); |
|||
} |
|||
|
|||
void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { |
|||
std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap; |
|||
metaVariableNameToValueMap.emplace(metaVariableName, variableValue); |
|||
this->setValue(metaVariableNameToValueMap, targetValue); |
|||
} |
|||
|
|||
void Dd<CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) { |
|||
std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap; |
|||
metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1); |
|||
metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2); |
|||
this->setValue(metaVariableNameToValueMap, targetValue); |
|||
} |
|||
|
|||
void Dd<CUDD>::setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) { |
|||
Dd<CUDD> valueEncoding(this->getDdManager()->getOne()); |
|||
for (auto const& nameValuePair : metaVariableNameToValueMap) { |
|||
valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); |
|||
} |
|||
|
|||
this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); |
|||
} |
|||
|
|||
bool Dd<CUDD>::isOne() const { |
|||
return *this == this->getDdManager()->getOne(); |
|||
} |
|||
|
|||
bool Dd<CUDD>::isZero() const { |
|||
return *this == this->getDdManager()->getZero(); |
|||
} |
|||
|
|||
bool Dd<CUDD>::containsMetaVariable(std::string const& metaVariableName) const { |
|||
auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); |
|||
return metaVariable != containedMetaVariableNames.end(); |
|||
} |
|||
|
|||
bool Dd<CUDD>::containsMetaVariables(std::set<std::string> metaVariableNames) const { |
|||
for (auto const& metaVariableName : metaVariableNames) { |
|||
auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); |
|||
|
|||
if (metaVariable == containedMetaVariableNames.end()) { |
|||
return false; |
|||
} |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
std::set<std::string> const& Dd<CUDD>::getContainedMetaVariableNames() const { |
|||
return this->containedMetaVariableNames; |
|||
} |
|||
|
|||
std::set<std::string>& Dd<CUDD>::getContainedMetaVariableNames() { |
|||
return this->containedMetaVariableNames; |
|||
} |
|||
|
|||
void Dd<CUDD>::exportToDot(std::string const& filename) const { |
|||
FILE* filePointer = fopen(filename.c_str() , "w"); |
|||
this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer); |
|||
fclose(filePointer); |
|||
} |
|||
|
|||
ADD Dd<CUDD>::getCuddAdd() { |
|||
return this->cuddAdd; |
|||
} |
|||
|
|||
ADD const& Dd<CUDD>::getCuddAdd() const { |
|||
return this->cuddAdd; |
|||
} |
|||
|
|||
void Dd<CUDD>::addContainedMetaVariable(std::string const& metaVariableName) { |
|||
this->getContainedMetaVariableNames().insert(metaVariableName); |
|||
} |
|||
|
|||
void Dd<CUDD>::removeContainedMetaVariable(std::string const& metaVariableName) { |
|||
this->getContainedMetaVariableNames().erase(metaVariableName); |
|||
} |
|||
|
|||
std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const { |
|||
return this->ddManager; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,407 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDDD_H_ |
|||
#define STORM_STORAGE_DD_CUDDDD_H_ |
|||
|
|||
#include <unordered_map> |
|||
#include <set> |
|||
#include <memory> |
|||
|
|||
#include "src/storage/dd/Dd.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
// Include the C++-interface of CUDD. |
|||
#include "cuddObj.hh" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
// Forward-declare the DdManager class. |
|||
template<DdType Type> class DdManager; |
|||
|
|||
template<> |
|||
class Dd<CUDD> { |
|||
public: |
|||
// Declare the DdManager class as friend so it can access the internals of a DD. |
|||
friend class DdManager<CUDD>; |
|||
|
|||
// Instantiate all copy/move constructors/assignments with the default implementation. |
|||
Dd() = default; |
|||
Dd(Dd<CUDD> const& other) = default; |
|||
Dd& operator=(Dd<CUDD> const& other) = default; |
|||
#ifndef WINDOWS |
|||
Dd(Dd<CUDD>&& other) = default; |
|||
Dd& operator=(Dd<CUDD>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Retrieves whether the two DDs represent the same function. |
|||
* |
|||
* @param other The DD that is to be compared with the current one. |
|||
*/ |
|||
bool operator==(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* 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); |
|||
|
|||
/*! |
|||
* Subtracts the DD from the constant zero function. |
|||
* |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> minus() const; |
|||
|
|||
/*! |
|||
* 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. |
|||
* |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<CUDD>& complement(); |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one that have an identical function values. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> equals(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one that have distinct function values. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> notEquals(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are less |
|||
* than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> less(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are less or |
|||
* equal than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> lessOrEqual(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are greater |
|||
* than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> greater(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are greater |
|||
* or equal than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<CUDD> greaterOrEqual(Dd<CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Existentially abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariableNames The names of all meta variables from which to abstract. |
|||
*/ |
|||
void existsAbstract(std::set<std::string> const& metaVariableNames); |
|||
|
|||
/*! |
|||
* Sum-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariableNames The names of all meta variables from which to abstract. |
|||
*/ |
|||
void sumAbstract(std::set<std::string> const& metaVariableNames); |
|||
|
|||
/*! |
|||
* Min-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariableNames The names of all meta variables from which to abstract. |
|||
*/ |
|||
void minAbstract(std::set<std::string> const& metaVariableNames); |
|||
|
|||
/*! |
|||
* Max-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariableNames The names of all meta variables from which to abstract. |
|||
*/ |
|||
void maxAbstract(std::set<std::string> const& metaVariableNames); |
|||
|
|||
/*! |
|||
* Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have |
|||
* the same number of underlying DD variables. |
|||
* |
|||
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. |
|||
*/ |
|||
void swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs); |
|||
|
|||
/*! |
|||
* Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta |
|||
* variables. |
|||
* |
|||
* @param otherMatrix The matrix with which to multiply. |
|||
* @param summationMetaVariableNames The names of the meta variables over which to sum during the matrix- |
|||
* matrix multiplication. |
|||
* @return A DD representing the result of the matrix-matrix multiplication. |
|||
*/ |
|||
Dd<CUDD> multiplyMatrix(Dd<CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames); |
|||
|
|||
/*! |
|||
* Retrieves the number of encodings that are mapped to a non-zero value. |
|||
* |
|||
* @return The number of encodings that are mapped to a non-zero value. |
|||
*/ |
|||
uint_fast64_t getNonZeroCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of leaves of the DD. |
|||
* |
|||
* @return The number of leaves of the DD. |
|||
*/ |
|||
uint_fast64_t getLeafCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of nodes necessary to represent the DD. |
|||
* |
|||
* @return The number of nodes in this DD. |
|||
*/ |
|||
uint_fast64_t getNodeCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the lowest function value of any encoding. |
|||
* |
|||
* @return The lowest function value of any encoding. |
|||
*/ |
|||
double getMin() const; |
|||
|
|||
/*! |
|||
* Retrieves the highest function value of any encoding. |
|||
* |
|||
* @return The highest function value of any encoding. |
|||
*/ |
|||
double getMax() const; |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given value of the meta variable to the given |
|||
* target value. |
|||
* |
|||
* @param metaVariableName The name of the meta variable that has to be equal to the given value. |
|||
* @param variableValue The value that the meta variable is supposed to have. This must be within the range |
|||
* of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the two meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariableName1 The name of the first meta variable that has to be equal to the first given |
|||
* value. |
|||
* @param variableValue1 The value that the first meta variable is supposed to have. This must be within the |
|||
* range of the meta variable. |
|||
* @param metaVariableName2 The name of the first meta variable that has to be equal to the second given |
|||
* value. |
|||
* @param variableValue2 The value that the second meta variable is supposed to have. This must be within |
|||
* the range of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the given meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariableNameToValueMap A mapping of meta variable names to the values they are supposed to |
|||
* have. All values must be within the range of the respective meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue); |
|||
|
|||
/*! |
|||
* Retrieves whether this DD represents the constant one function. |
|||
* |
|||
* @return True if this DD represents the constant one function. |
|||
*/ |
|||
bool isOne() const; |
|||
|
|||
/*! |
|||
* Retrieves whether this DD represents the constant zero function. |
|||
* |
|||
* @return True if this DD represents the constant zero function. |
|||
*/ |
|||
bool isZero() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given meta variable is contained in the DD. |
|||
* |
|||
* @param metaVariableName The name of the meta variable for which to query membership. |
|||
* @return True iff the meta variable is contained in the DD. |
|||
*/ |
|||
bool containsMetaVariable(std::string const& metaVariableName) const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given meta variables are all contained in the DD. |
|||
* |
|||
* @param metaVariableNames The names of the meta variable for which to query membership. |
|||
* @return True iff all meta variables are contained in the DD. |
|||
*/ |
|||
bool containsMetaVariables(std::set<std::string> metaVariableNames) const; |
|||
|
|||
/*! |
|||
* Retrieves the set of all names of meta variables contained in the DD. |
|||
* |
|||
* @return The set of names of all meta variables contained in the DD. |
|||
*/ |
|||
std::set<std::string> const& getContainedMetaVariableNames() const; |
|||
|
|||
/*! |
|||
* Retrieves the set of all names of meta variables contained in the DD. |
|||
* |
|||
* @return The set of names of all meta variables contained in the DD. |
|||
*/ |
|||
std::set<std::string>& getContainedMetaVariableNames(); |
|||
|
|||
/*! |
|||
* Exports the DD to the given file in the dot format. |
|||
* |
|||
* @param filename The name of the file to which the DD is to be exported. |
|||
*/ |
|||
void exportToDot(std::string const& filename) const; |
|||
|
|||
/*! |
|||
* 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: |
|||
/*! |
|||
* Retrieves the CUDD ADD object associated with this DD. |
|||
* |
|||
* @return The CUDD ADD object assoicated with this DD. |
|||
*/ |
|||
ADD getCuddAdd(); |
|||
|
|||
/*! |
|||
* Retrieves the CUDD ADD object associated with this DD. |
|||
* |
|||
* @return The CUDD ADD object assoicated with this DD. |
|||
*/ |
|||
ADD const& getCuddAdd() const; |
|||
|
|||
/*! |
|||
* Adds the given meta variable name to the set of meta variables that are contained in this DD. |
|||
* |
|||
* @param metaVariableName The name of the meta variable to add. |
|||
*/ |
|||
void addContainedMetaVariable(std::string const& metaVariableName); |
|||
|
|||
/*! |
|||
* Removes the given meta variable name to the set of meta variables that are contained in this DD. |
|||
* |
|||
* @param metaVariableName The name of the meta variable to remove. |
|||
*/ |
|||
void removeContainedMetaVariable(std::string const& metaVariableName); |
|||
|
|||
/*! |
|||
* Creates a DD that encapsulates the given CUDD ADD. |
|||
* |
|||
* @param ddManager The manager responsible for this DD. |
|||
* @param cuddAdd The CUDD ADD to store. |
|||
* @param |
|||
*/ |
|||
Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>()); |
|||
|
|||
// 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::set<std::string> containedMetaVariableNames; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ |
|||
@ -0,0 +1,149 @@ |
|||
#include <cmath>
|
|||
#include <algorithm>
|
|||
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
#include <iostream>
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
DdManager<CUDD>::DdManager() : metaVariableMap(), cuddManager() { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
Dd<CUDD> DdManager<CUDD>::getOne() { |
|||
return Dd<CUDD>(this->shared_from_this(), cuddManager.addOne()); |
|||
} |
|||
|
|||
Dd<CUDD> DdManager<CUDD>::getZero() { |
|||
return Dd<CUDD>(this->shared_from_this(), cuddManager.addZero()); |
|||
} |
|||
|
|||
Dd<CUDD> DdManager<CUDD>::getConstant(double value) { |
|||
return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value)); |
|||
} |
|||
|
|||
Dd<CUDD> DdManager<CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) { |
|||
std::vector<Dd<CUDD>> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); |
|||
|
|||
Dd<CUDD> result; |
|||
if (value & (1ull << (ddVariables.size() - 1))) { |
|||
result = ddVariables[0]; |
|||
} else { |
|||
result = ddVariables[0]; |
|||
} |
|||
|
|||
for (std::size_t i = 1; i < ddVariables.size(); ++i) { |
|||
if (value & (1ull << (ddVariables.size() - i - 1))) { |
|||
result *= ddVariables[i]; |
|||
} else { |
|||
result *= ~ddVariables[i]; |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
Dd<CUDD> DdManager<CUDD>::getRange(std::string const metaVariableName) { |
|||
storm::dd::DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName); |
|||
|
|||
Dd<CUDD> result = this->getZero(); |
|||
for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { |
|||
result.setValue(metaVariableName, value - metaVariable.getLow(), static_cast<double>(value)); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
void DdManager<CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { |
|||
// Check whether a meta variable already exists.
|
|||
if (this->hasMetaVariable(name)) { |
|||
throw 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."; |
|||
} |
|||
|
|||
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1))); |
|||
|
|||
std::vector<Dd<CUDD>> variables; |
|||
for (std::size_t i = 0; i < numberOfBits; ++i) { |
|||
variables.emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {name})); |
|||
} |
|||
|
|||
metaVariableMap.emplace(name, DdMetaVariable<CUDD>(name, low, high, variables, this->shared_from_this())); |
|||
} |
|||
|
|||
void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) { |
|||
// 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."; |
|||
} |
|||
|
|||
// 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<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<CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]})); |
|||
} |
|||
} |
|||
|
|||
// Now add the meta variables.
|
|||
for (uint_fast64_t i = 0; i < names.size(); ++i) { |
|||
metaVariableMap.emplace(names[i], DdMetaVariable<CUDD>(names[i], low, high, variables[i], this->shared_from_this())); |
|||
} |
|||
} |
|||
|
|||
DdMetaVariable<CUDD> const& DdManager<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."; |
|||
} |
|||
|
|||
return nameVariablePair->second; |
|||
} |
|||
|
|||
std::set<std::string> DdManager<CUDD>::getAllMetaVariableNames() const { |
|||
std::set<std::string> result; |
|||
for (auto const& nameValuePair : metaVariableMap) { |
|||
result.insert(nameValuePair.first); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
std::size_t DdManager<CUDD>::getNumberOfMetaVariables() const { |
|||
return this->metaVariableMap.size(); |
|||
} |
|||
|
|||
bool DdManager<CUDD>::hasMetaVariable(std::string const& metaVariableName) const { |
|||
return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end(); |
|||
} |
|||
|
|||
Cudd& DdManager<CUDD>::getCuddManager() { |
|||
return this->cuddManager; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,141 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ |
|||
#define STORM_STORAGE_DD_CUDDDDMANAGER_H_ |
|||
|
|||
#include <unordered_map> |
|||
|
|||
#include "src/storage/dd/DdManager.h" |
|||
#include "src/storage/dd/DdMetaVariable.h" |
|||
#include "src/storage/dd/CuddDd.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
// Include the C++-interface of CUDD. |
|||
#include "cuddObj.hh" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<> |
|||
class DdManager<CUDD> : public std::enable_shared_from_this<DdManager<CUDD>> { |
|||
public: |
|||
// To break the cylic dependencies, we need to forward-declare the other DD-related classes. |
|||
friend class Dd<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<CUDD>& operator=(DdManager<CUDD> const& other) = delete; |
|||
#ifndef WINDOWS |
|||
DdManager(DdManager<CUDD>&& other) = default; |
|||
DdManager<CUDD>& operator=(DdManager<CUDD>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* 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); |
|||
|
|||
/*! |
|||
* Retrieves the DD representing the function that maps all inputs which have the given meta variable equal |
|||
* to the given value one. |
|||
* |
|||
* @param metaVariableName The meta variable that is supposed to have the given value. |
|||
* @param value The value the meta variable is supposed to have. |
|||
* @return The DD representing the function that maps all inputs which have the given meta variable equal |
|||
* to the given value one. |
|||
*/ |
|||
Dd<CUDD> getEncoding(std::string const& metaVariableName, int_fast64_t value); |
|||
|
|||
/*! |
|||
* Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values |
|||
* of the range of the meta variable to one. |
|||
* |
|||
* @param metaVariableName The name of the meta variable whose range to retrieve. |
|||
* @return The range of the meta variable |
|||
*/ |
|||
Dd<CUDD> getRange(std::string const metaVariableName); |
|||
|
|||
/*! |
|||
* 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. |
|||
*/ |
|||
void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high); |
|||
|
|||
/*! |
|||
* Adds 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. |
|||
*/ |
|||
void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high); |
|||
|
|||
/*! |
|||
* 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 names of all meta variables that have been added to the manager. |
|||
* |
|||
* @return The set of all meta variable names of the manager. |
|||
*/ |
|||
std::set<std::string> getAllMetaVariableNames() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of meta variables that are contained in this manager. |
|||
* |
|||
* @return The number of meta variables contained in this manager. |
|||
*/ |
|||
std::size_t getNumberOfMetaVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given meta variable name is already in use. |
|||
* |
|||
* @param metaVariableName The meta variable name whose membership to query. |
|||
* @return True if the given meta variable name is managed by this manager. |
|||
*/ |
|||
bool hasMetaVariable(std::string const& metaVariableName) const; |
|||
|
|||
private: |
|||
/*! |
|||
* Retrieves the underlying CUDD manager. |
|||
* |
|||
* @return The underlying CUDD manager. |
|||
*/ |
|||
Cudd& getCuddManager(); |
|||
|
|||
// 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_ */ |
|||
@ -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_ */ |
|||
@ -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_ */ |
|||
@ -0,0 +1,52 @@ |
|||
#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), 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> |
|||
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::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<CUDD>; |
|||
} |
|||
} |
|||
@ -0,0 +1,114 @@ |
|||
#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" |
|||
|
|||
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>; |
|||
|
|||
/*! |
|||
* 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& 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 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 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_ */ |
|||
@ -0,0 +1,12 @@ |
|||
#ifndef STORM_STORAGE_DD_DDTYPE_H_ |
|||
#define STORM_STORAGE_DD_DDTYPE_H_ |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
enum DdType { |
|||
CUDD |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_DDTYPE_H_ */ |
|||
@ -0,0 +1,12 @@ |
|||
#ifndef STORM_GENERATED_VERSION_H_ |
|||
#define STORM_GENERATED_VERSION_H_ |
|||
|
|||
// Version Information |
|||
#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ // The major version of StoRM |
|||
#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ // The minor version of StoRM |
|||
#define STORM_CPP_VERSION_PATCH @STORM_CPP_VERSION_PATCH@ // The patch version of StoRM |
|||
#define STORM_CPP_VERSION_COMMITS_AHEAD @STORM_CPP_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set |
|||
#define STORM_CPP_VERSION_HASH "@STORM_CPP_VERSION_HASH@" // The short hash of the git commit this build is bases on |
|||
#define STORM_CPP_VERSION_DIRTY @STORM_CPP_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else |
|||
|
|||
#endif |
|||
@ -0,0 +1,71 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
#include "src/storage/dd/CuddDd.h"
|
|||
#include "src/storage/dd/DdMetaVariable.h"
|
|||
|
|||
TEST(CuddDdManager, Constants) { |
|||
std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>()); |
|||
|
|||
storm::dd::Dd<storm::dd::CUDD> zero; |
|||
ASSERT_NO_THROW(zero = manager->getZero()); |
|||
|
|||
EXPECT_EQ(0, zero.getNonZeroCount()); |
|||
EXPECT_EQ(1, zero.getLeafCount()); |
|||
EXPECT_EQ(1, zero.getNodeCount()); |
|||
EXPECT_EQ(0, zero.getMin()); |
|||
EXPECT_EQ(0, zero.getMax()); |
|||
|
|||
storm::dd::Dd<storm::dd::CUDD> one; |
|||
ASSERT_NO_THROW(one = manager->getOne()); |
|||
|
|||
EXPECT_EQ(1, one.getNonZeroCount()); |
|||
EXPECT_EQ(1, one.getLeafCount()); |
|||
EXPECT_EQ(1, one.getNodeCount()); |
|||
EXPECT_EQ(1, one.getMin()); |
|||
EXPECT_EQ(1, one.getMax()); |
|||
|
|||
storm::dd::Dd<storm::dd::CUDD> two; |
|||
ASSERT_NO_THROW(two = manager->getConstant(2)); |
|||
|
|||
EXPECT_EQ(1, two.getNonZeroCount()); |
|||
EXPECT_EQ(1, two.getLeafCount()); |
|||
EXPECT_EQ(1, two.getNodeCount()); |
|||
EXPECT_EQ(2, two.getMin()); |
|||
EXPECT_EQ(2, two.getMax()); |
|||
} |
|||
|
|||
TEST(CuddDdManager, MetaVariableTest) { |
|||
std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>()); |
|||
|
|||
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); |
|||
EXPECT_EQ(1, manager->getNumberOfMetaVariables()); |
|||
|
|||
std::vector<std::string> names = {"x", "x'"}; |
|||
ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); |
|||
|
|||
names = {"y", "y"}; |
|||
ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); |
|||
|
|||
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("y'")); |
|||
|
|||
std::set<std::string> metaVariableSet = {"x", "y", "y'"}; |
|||
EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); |
|||
|
|||
ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException); |
|||
ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x")); |
|||
storm::dd::DdMetaVariable<storm::dd::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()); |
|||
} |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue