From 6078e074761df613a1890ddf8bf531690038ab25 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 18 Apr 2014 22:07:54 +0200 Subject: [PATCH] First version of DD iterator; small test included. Former-commit-id: 2ec2323886ac67717bb9864a9d2f2c0cbb1d98ae --- .../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 2 +- .../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 2 +- src/storage/dd/CuddDd.cpp | 11 ++ src/storage/dd/CuddDd.h | 16 ++ src/storage/dd/CuddDdForwardIterator.cpp | 148 ++++++++++++++++-- src/storage/dd/CuddDdForwardIterator.h | 102 ++++++++++-- src/storage/dd/CuddDdManager.cpp | 12 ++ src/storage/dd/CuddDdManager.h | 14 +- src/storage/dd/DdMetaVariable.cpp | 15 +- src/storage/dd/DdMetaVariable.h | 25 ++- src/storage/expressions/SimpleValuation.cpp | 11 +- test/functional/storage/CuddDdTest.cpp | 21 +++ 12 files changed, 350 insertions(+), 29 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index d62328ff0..fcec76782 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -5280,7 +5280,7 @@ int ABDD::NextCube( DdGen * gen, int ** cube, - CUDD_VALUE_TYPE * value) const + CUDD_VALUE_TYPE * value) { return Cudd_NextCube(gen, cube, value); diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index d8c2d0722..1162a968c 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -192,7 +192,7 @@ public: const; int CountLeaves() const; DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const; - int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value) const; + static int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value); double Density(int nvars) const; }; // ABDD diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 313a2b4d8..d07696d08 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -434,6 +434,17 @@ namespace storm { return this->ddManager; } + DdForwardIterator Dd::begin() const { + int* cube; + double value; + DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); + return DdForwardIterator(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames()); + } + + DdForwardIterator Dd::end() const { + return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr); + } + std::ostream & operator<<(std::ostream& out, const Dd& dd) { dd.exportToDot(); return out; diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index fa780f263..33318ed38 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -7,6 +7,7 @@ #include #include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddDdForwardIterator.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -22,6 +23,7 @@ namespace storm { public: // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; + friend class DdForwardIterator; // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; @@ -405,6 +407,20 @@ namespace storm { */ std::shared_ptr> getDdManager() const; + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + DdForwardIterator begin() const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @return An iterator that points past the end of the container. + */ + DdForwardIterator end() const; + friend std::ostream & operator<<(std::ostream& out, const Dd& dd); private: /*! diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index fc66895dd..c0e754c8b 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -1,24 +1,152 @@ #include "src/storage/dd/CuddDdForwardIterator.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/DdMetaVariable.h" +#include "src/exceptions/ExceptionMacros.h" namespace storm { namespace dd { - DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, ADD cuddAdd) : ddManager(ddManager), value(0), cube(nullptr), cuddAdd(cuddAdd), isAtEnd(false), generator(nullptr) { - // Start by getting the first cube. - this->generator = this->cuddAdd.FirstCube(&cube, &value); - - // If the generator is already empty, we set the corresponding flag. - this->isAtEnd = Cudd_IsGenEmpty(generator); + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + // If the given generator is not yet at its end, we need to create the current valuation from the cube from + // scratch. + if (!this->isAtEnd) { + // Start by registering all meta variables in the valuation with the appropriate type. + for (auto const& metaVariableName : *this->metaVariables) { + auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); + switch (metaVariable.getType()) { + case DdMetaVariable::MetaVariableType::Bool: currentValuation.addBooleanIdentifier(metaVariableName); break; + case DdMetaVariable::MetaVariableType::Int: currentValuation.addIntegerIdentifier(metaVariableName); break; + } + } + + // And then get ready for treating the first cube. + this->treatNewCube(); + } + } + + DdForwardIterator::DdForwardIterator(DdForwardIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { + // Null-out the pointers of which we took possession. + other.cube = nullptr; + other.generator = nullptr; + } + + DdForwardIterator& DdForwardIterator::operator=(DdForwardIterator&& other) { + if (this != &other) { + this->ddManager = other.ddManager; + this->generator = other.generator; + this->cube = other.cube; + this->value = other.value; + this->isAtEnd = other.isAtEnd; + this->metaVariables = other.metaVariables; + this->cubeCounter = other.cubeCounter; + this->relevantDontCareDdVariables = other.relevantDontCareDdVariables; + this->currentValuation = other.currentValuation; + + // Null-out the pointers of which we took possession. + other.cube = nullptr; + other.generator = nullptr; + } + return *this; + } + + DdForwardIterator::~DdForwardIterator() { + if (this->cube != nullptr) { + free(this->cube); + } + if (this->generator != nullptr) { + free(this->generator); + } } DdForwardIterator& DdForwardIterator::operator++() { - // TODO: eliminate current + LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end."); + + // If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the + // found solutions and get the next "first" cube. + if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { + // Get the next cube and check for emptiness. + ABDD::NextCube(generator, &cube, &value); + this->isAtEnd = Cudd_IsGenEmpty(generator); + + // In case we are not done yet, we get ready to treat the next cube. + if (!this->isAtEnd) { + this->treatNewCube(); + } + } else { + // Treat the next solution of the cube. + this->treatNextInCube(); + } + + return *this; + } + + void DdForwardIterator::treatNextInCube() { + // Start by increasing the counter and check which bits we need to set/unset in the new valuation. + ++this->cubeCounter; + + for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { + auto const& metaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); + if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setBooleanValue(metaVariable.getName(), true); + } else { + currentValuation.setBooleanValue(metaVariable.getName(), false); + } + } else { + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + } else { + currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + } + } + } + } + + void DdForwardIterator::treatNewCube() { + this->relevantDontCareDdVariables.clear(); + + // Now loop through the bits of all meta variables and check whether they need to be set, not set or are + // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete + // valuations later. + for (auto const& metaVariableName : *this->metaVariables) { + auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); + if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { + currentValuation.setBooleanValue(metaVariableName, false); + } else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { + currentValuation.setBooleanValue(metaVariableName, true); + } else { + relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0)); + } + } else { + int_fast64_t intValue = 0; + for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) { + if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { + // Leave bit unset. + } else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { + intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1); + } else { + // Temporarily leave bit unset so we can iterate trough the other option later. + // Add the bit to the relevant don't care bits. + this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1)); + } + } + currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow()); + } + } + + // Finally, reset the cube counter. + this->cubeCounter = 0; } bool DdForwardIterator::operator==(DdForwardIterator const& other) const { if (this->isAtEnd && other.isAtEnd) { return true; } else { - return this->cuddAdd == other.cuddAdd; + return this->ddManager.get() == other.ddManager.get() && this->generator == other.generator + && this->cube == other.cube && this->value == other.value && this->isAtEnd == other.isAtEnd + && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter + && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables + && this->currentValuation == other.currentValuation; } } @@ -26,8 +154,8 @@ namespace storm { return !(*this == other); } - storm::expressions::SimpleValuation DdForwardIterator::operator*() const { - // FIXME: construct valuation and return it. + std::pair DdForwardIterator::operator*() const { + return std::make_pair(currentValuation, value); } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 09c627b14..054438d2e 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -3,6 +3,9 @@ #include #include +#include +#include +#include #include "src/storage/dd/DdForwardIterator.h" #include "src/storage/expressions/SimpleValuation.h" @@ -12,33 +15,114 @@ namespace storm { namespace dd { + // Forward-declare the DdManager class. + template class DdManager; + template class Dd; + template<> class DdForwardIterator { public: - // Forward-declare the DdManager class. - template class DdManager; + friend class Dd; + + // Default-instantiate the constructor. + DdForwardIterator() = default; + + // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. + DdForwardIterator(DdForwardIterator const& other) = delete; + DdForwardIterator& operator=(DdForwardIterator const& other) = delete; + + // Provide move-construction and move-assignment, though. + DdForwardIterator(DdForwardIterator&& other); + DdForwardIterator& operator=(DdForwardIterator&& other); + /*! + * Destroys the forward iterator and frees the generator as well as the cube if they are not the nullptr. + */ + ~DdForwardIterator(); + + /*! + * Moves the iterator one position forward. + */ DdForwardIterator& operator++(); - storm::expressions::SimpleValuation operator*() const; + + /*! + * Returns a pair consisting of a valuation of meta variables and the value to which this valuation is + * mapped. Note that the result is returned by value. + * + * @return A pair of a valuation and the function value. + */ + std::pair operator*() const; + + /*! + * Compares the iterator with the given one. Two iterators are considered equal when all their underlying + * data members are the same or they both are at their end. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered equal. + */ bool operator==(DdForwardIterator const& other) const; + + /*! + * Compares the iterator with the given one. Two iterators are considered unequal iff they are not + * considered equal. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered unequal. + */ bool operator!=(DdForwardIterator const& other) const; private: - DdForwardIterator(std::shared_ptr> ddManager, ADD cuddAdd, std::vector const& relevantDdVariables); + /*! + * Constructs a forward iterator using the given generator with the given set of relevant meta variables. + * + * @param ddManager The manager responsible for the DD over which to iterate. + * @param generator The generator used to enumerate the cubes of the DD. + * @param cube The cube as represented by CUDD. + * @param value The value the cube is mapped to. + * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any + * more. + * @param metaVariables The meta variables that appear in the DD. + */ + DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr); + + /*! + * Recreates the internal information when a new cube needs to be treated. + */ + void treatNewCube(); + + /*! + * Updates the internal information when the next solution of the current cube needs to be treated. + */ + void treatNextInCube(); + // The manager responsible for the meta variables (and therefore the underlying DD). std::shared_ptr> ddManager; - double value; + // The CUDD generator used to enumerate the cubes of the DD. + DdGen* generator; + // The currently considered cube of the DD. int* cube; - - uint_fast64_t positionInCube; - ADD cuddAdd; + // The function value of the current cube. + double value; + // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used + // for the check against the end iterator. bool isAtEnd; - DdGen* generator; + // The set of meta variables appearing in the DD. + std::set const* metaVariables; + + // A number that represents how many assignments of the current cube have already been returned previously. + // This is needed, because cubes may represent many assignments (if they have don't care variables). + uint_fast64_t cubeCounter; + + // A vector of tuples of the form . + std::vector> relevantDontCareDdVariables; + + // The current valuation of meta variables. + storm::expressions::SimpleValuation currentValuation; }; } } diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 2d77c6350..c75a7c211 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -111,6 +111,18 @@ namespace storm { metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); } + void DdManager::addMetaVariable(std::string const& name) { + // Check whether a meta variable already exists. + if (this->hasMetaVariable(name)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; + } + + std::vector> variables; + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); + + metaVariableMap.emplace(name, DdMetaVariable(name, variables, this->shared_from_this())); + } + void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { // Make sure that at least one meta variable is added. if (names.size() == 0) { diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 96daeb34a..6df3dc25c 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -5,7 +5,6 @@ #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. @@ -16,7 +15,6 @@ namespace storm { template<> class DdManager : public std::enable_shared_from_this> { public: - // To break the cylic dependencies, we need to forward-declare the other DD-related classes. friend class Dd; /*! @@ -83,7 +81,7 @@ namespace storm { Dd getIdentity(std::string const& metaVariableName); /*! - * Adds a meta variable with the given name and range. + * Adds an integer 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. @@ -92,7 +90,15 @@ namespace storm { 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. + * Adds a boolean meta variable with the given name. + * + * @param name The 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. diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 9132eab03..453b83cc8 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,7 +4,15 @@ namespace storm { namespace dd { template - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> 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 + DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> 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; @@ -16,6 +24,11 @@ namespace storm { return this->name; } + template + typename DdMetaVariable::MetaVariableType DdMetaVariable::getType() const { + return this->type; + } + template int_fast64_t DdMetaVariable::getLow() const { return this->low; diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index f6c90cc21..47936d805 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -8,6 +8,7 @@ #include "utility/OsDetection.h" #include "src/storage/dd/CuddDd.h" +#include "src/storage/expressions/Expression.h" namespace storm { namespace dd { @@ -20,9 +21,13 @@ namespace storm { // Declare the DdManager class as friend so it can access the internals of a meta variable. friend class DdManager; friend class Dd; + friend class DdForwardIterator; + + // An enumeration for all legal types of meta variables. + enum class MetaVariableType { Bool, Int }; /*! - * Creates a meta variable with the given name, range bounds. + * 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. @@ -32,6 +37,14 @@ namespace storm { */ DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> 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> const& ddVariables, std::shared_ptr> manager); + // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; DdMetaVariable& operator=(DdMetaVariable const& other) = default; @@ -47,6 +60,13 @@ namespace storm { */ 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. * @@ -93,6 +113,9 @@ namespace storm { // 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; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index fb6f0088c..c1d4862a6 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -1,6 +1,7 @@ -#include "src/storage/expressions/SimpleValuation.h" - #include +#include "src/storage/expressions/SimpleValuation.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace expressions { @@ -13,16 +14,22 @@ namespace storm { } void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Boolean identifier '" << name << "' already registered."); + this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size()); this->booleanValues.push_back(false); } void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Integer identifier '" << name << "' already registered."); + this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size()); this->integerValues.push_back(initialValue); } void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Double identifier '" << name << "' already registered."); + this->doubleIdentifierToIndexMap->emplace(name, this->doubleValues.size()); this->doubleValues.push_back(initialValue); } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index c405006d8..3ca7c0ce1 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -273,3 +273,24 @@ TEST(CuddDd, GetSetValueTest) { metaVariableToValueMap.emplace("x", 4); EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); } + +TEST(CuddDd, ForwardIteratorTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + manager->addMetaVariable("x", 1, 9); + manager->addMetaVariable("y", 0, 3); + + storm::dd::Dd dd; + ASSERT_NO_THROW(dd = manager->getRange("x")); + + storm::dd::DdForwardIterator it, ite; + ASSERT_NO_THROW(it = dd.begin()); + ASSERT_NO_THROW(ite = dd.end()); + std::pair valuationValuePair; + uint_fast64_t numberOfValuations = 0; + while (it != ite) { + ASSERT_NO_THROW(valuationValuePair = *it); + ASSERT_NO_THROW(++it); + ++numberOfValuations; + } + EXPECT_EQ(9, numberOfValuations); +}