sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Another step towards generating explicit data structures from DDs using ODDs. 

Former-commit-id: 5b7e3e8680
tempestpy_adaptions
dehnert 11 years ago
parent
f12ff82baf
commit
236e7fa290
3 changed files with 181 additions and 66 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 174
      src/storage/dd/CuddDd.cpp
  2. 40
      src/storage/dd/CuddDd.h
  3. 33
      test/functional/storage/CuddDdTest.cpp

174
src/storage/dd/CuddDd.cpp
View File

@ -119,138 +119,141 @@ namespace storm {
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.Equals(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.NotEquals(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.LessThan(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.LessThanOrEqual(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.GreaterThan(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result.cuddAdd = result.cuddAdd.GreaterThanOrEqual(other.getCuddAdd());
return result;
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames);
}
void Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) {
Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
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);
newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
void Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) {
Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
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);
newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd());
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
void Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
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);
newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->cuddAdd = this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd());
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
void Dd<DdType::CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) {
Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
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);
newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->cuddAdd = this->cuddAdd.MinAbstract(cubeDd.getCuddAdd());
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
void Dd<DdType::CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) {
Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<std::string> newMetaVariables = this->getContainedMetaVariableNames();
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);
newMetaVariables.erase(metaVariableName);
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd());
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables);
}
bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> const& other, double precision, bool relative) const {
@ -410,7 +413,7 @@ namespace storm {
}
Dd<DdType::CUDD> value = *this * valueEncoding;
value.sumAbstract(this->getContainedMetaVariableNames());
value = value.sumAbstract(this->getContainedMetaVariableNames());
return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
}
@ -430,18 +433,19 @@ namespace storm {
return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
}
std::vector<double> Dd<DdType::CUDD>::toDoubleVector() const {
return this->toDoubleVector(Odd<DdType::CUDD>(*this));
std::vector<double> Dd<DdType::CUDD>::toVector() const {
return this->toVector(Odd<DdType::CUDD>(*this));
}
std::vector<double> Dd<DdType::CUDD>::toDoubleVector(Odd<DdType::CUDD> const& odd) const {
std::vector<double> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& odd) const {
std::vector<double> result(odd.getTotalOffset());
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
toDoubleVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices);
toVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices);
return result;
}
void Dd<DdType::CUDD>::toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const {
void Dd<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const {
// For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
return;
}
@ -452,12 +456,92 @@ namespace storm {
} else if (ddVariableIndices[currentLevel] < dd->index) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
toDoubleVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
toDoubleVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
toVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
toVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
} else {
// Otherwise, we simply recursively call the function for both (different) cases.
toDoubleVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
toDoubleVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
toVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
toVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
}
}
storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
std::set<std::string> rowVariables;
std::set<std::string> columnVariables;
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
for (auto const& variableName : this->getContainedMetaVariableNames()) {
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variableName);
if (variableName.size() > 0 && variableName.back() == '\'') {
columnVariables.insert(variableName);
for (auto const& ddVariable : metaVariable.getDdVariables()) {
ddColumnVariableIndices.push_back(ddVariable.getIndex());
}
} else {
rowVariables.insert(variableName);
for (auto const& ddVariable : metaVariable.getDdVariables()) {
ddRowVariableIndices.push_back(ddVariable.getIndex());
}
}
}
Odd<DdType::CUDD> columnOdd(this->existsAbstract(rowVariables));
Odd<DdType::CUDD> rowOdd(this->existsAbstract(columnVariables));
storm::storage::SparseMatrixBuilder<double> builder;
toMatrixRec(this->getCuddAdd().getNode(), builder, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices);
return builder.build();
}
void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, storm::storage::SparseMatrixBuilder<double>& builder, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const {
// FIXME: this method currently assumes a strict interleaved order, which does not seem necessary.
// For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
return;
}
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel + currentColumnLevel == maxLevel) {
builder.addNextValue(currentRowOffset, currentColumnOffset, Cudd_V(dd));
} else {
DdNode const* elseElse;
DdNode const* elseThen;
DdNode const* thenElse;
DdNode const* thenThen;
if (ddColumnVariableIndices[currentColumnLevel] < dd->index) {
elseElse = elseThen = thenElse = thenThen = dd;
} else if (ddRowVariableIndices[currentColumnLevel] < dd->index) {
elseElse = thenElse = Cudd_E(dd);
elseThen = thenThen = Cudd_T(dd);
} else {
DdNode const* elseNode = Cudd_E(dd);
if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) {
elseElse = elseThen = elseNode;
} else {
elseElse = Cudd_E(elseNode);
elseThen = Cudd_T(elseNode);
}
DdNode const* thenNode = Cudd_T(dd);
if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) {
thenElse = thenThen = thenNode;
} else {
thenElse = Cudd_E(thenNode);
thenThen = Cudd_T(thenNode);
}
}
// Visit else-else.
toMatrixRec(elseElse, builder, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices);
// Visit else-then.
toMatrixRec(elseThen, builder, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices);
// Visit then-else.
toMatrixRec(thenElse, builder, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices);
// Visit then-then.
toMatrixRec(thenThen, builder, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices);
}
}

40
src/storage/dd/CuddDd.h
View File

@ -8,6 +8,7 @@
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/CuddDdForwardIterator.h"
#include "src/storage/SparseMatrix.h"
#include "src/storage/expressions/Expression.h"
#include "src/utility/OsDetection.h"
@ -234,35 +235,35 @@ namespace storm {
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
void existsAbstract(std::set<std::string> const& metaVariableNames);
Dd<DdType::CUDD> existsAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Universally abstracts from the given meta variables.
*
* @param metaVariableNames The names of all meta variables from which to abstract.
*/
void universalAbstract(std::set<std::string> const& metaVariableNames);
Dd<DdType::CUDD> universalAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* 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);
Dd<DdType::CUDD> sumAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* 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);
Dd<DdType::CUDD> minAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* 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);
Dd<DdType::CUDD> maxAbstract(std::set<std::string> const& metaVariableNames) const;
/*!
* Checks whether the current and the given DD represent the same function modulo some given precision.
@ -461,7 +462,13 @@ namespace storm {
*
* @return The double vector that is represented by this DD.
*/
std::vector<double> toDoubleVector() const;
std::vector<double> toVector() const;
/*!
* Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the
* row, whereas all primed variables are assumed to encode the column.
*/
storm::storage::SparseMatrix<double> toMatrix() const;
/*!
* Converts the DD to a double vector using the given ODD (that needs to be constructed for the DD).
@ -469,7 +476,7 @@ namespace storm {
* @param odd The ODD for the DD.
* @return The double vector that is represented by this DD.
*/
std::vector<double> toDoubleVector(Odd<DdType::CUDD> const& odd) const;
std::vector<double> toVector(Odd<DdType::CUDD> const& odd) const;
/*!
* Retrieves whether the given meta variable is contained in the DD.
@ -623,7 +630,24 @@ namespace storm {
* @param currentOffset The current offset.
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
*/
void toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const;
void toVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const;
/*!
* Helper function to convert the DD into a (sparse) matrix.
*
* @param dd The DD to convert.
* @param builder A matrix builder that can be used to insert the nonzero entries.
* @param rowOdd The ODD used for the row translation.
* @param columnOdd The ODD used for the column translation.
* @param currentRowLevel The currently considered row level in the DD.
* @param currentColumnLevel The currently considered row level in the DD.
* @param maxLevel The number of levels that need to be considered.
* @param currentRowOffset The current row offset.
* @param currentColumnOffset The current row offset.
* @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
* @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered.
*/
void toMatrixRec(DdNode const* dd, storm::storage::SparseMatrixBuilder<double>& builder, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const;
/*!
* Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support,

33
test/functional/storage/CuddDdTest.cpp
View File

@ -163,12 +163,12 @@ TEST(CuddDd, OperatorTest) {
dd4 = dd3.minimum(dd1);
dd4 *= manager->getEncoding("x", 2);
dd4.sumAbstract({"x"});
dd4 = dd4.sumAbstract({"x"});
EXPECT_EQ(2, dd4.getValue());
dd4 = dd3.maximum(dd1);
dd4 *= manager->getEncoding("x", 2);
dd4.sumAbstract({"x"});
dd4 = dd4.sumAbstract({"x"});
EXPECT_EQ(5, dd4.getValue());
dd1 = manager->getConstant(0.01);
@ -188,36 +188,36 @@ TEST(CuddDd, AbstractionTest) {
dd2 = manager->getConstant(5);
dd3 = dd1.equals(dd2);
EXPECT_EQ(1, dd3.getNonZeroCount());
ASSERT_THROW(dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3.existsAbstract({"x"}));
ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
EXPECT_EQ(1, dd3.getNonZeroCount());
ASSERT_THROW(dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3.existsAbstract({"x"}));
ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"}));
EXPECT_TRUE(dd3 == manager->getZero());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3.sumAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3.sumAbstract({"x"}));
ASSERT_THROW(dd3 = dd3.sumAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.sumAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3.minAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3.minAbstract({"x"}));
ASSERT_THROW(dd3 = dd3.minAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.minAbstract({"x"}));
EXPECT_EQ(0, dd3.getNonZeroCount());
EXPECT_EQ(0, dd3.getMax());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3.maxAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3.maxAbstract({"x"}));
ASSERT_THROW(dd3 = dd3.maxAbstract({"x'"}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.maxAbstract({"x"}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax());
}
@ -389,9 +389,16 @@ TEST(CuddDd, OddTest) {
EXPECT_EQ(12, odd.getNodeCount());
std::vector<double> ddAsVector;
ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector());
ASSERT_NO_THROW(ddAsVector = dd.toVector());
EXPECT_EQ(9, ddAsVector.size());
for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
EXPECT_TRUE(i+1 == ddAsVector[i]);
}
dd = manager->getIdentity("x").equals(manager->getIdentity("x'")) * manager->getRange("x");
storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = dd.toMatrix());
EXPECT_EQ(9, matrix.getRowCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(9, matrix.getNonzeroEntryCount());
}
Write Preview
Loading…
Cancel
Save