diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 43fb7f0a2..bcbc41085 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -29,11 +29,7 @@ namespace storm { ++counter; } - if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) { - newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), 3); - } else { - newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), metaVariable.getLow(), metaVariable.getHigh(), 3); - } + newMetaVariables = ddManager.cloneVariable(metaVariablePair.first, newMetaVariableName + std::to_string(counter), 3); newRowVariables.insert(newMetaVariables[0]); newColumnVariables.insert(newMetaVariables[1]); diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index a27e86dea..58d6f20f6 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -7,6 +7,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -75,7 +76,7 @@ namespace storm { Bdd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool mostSignificantBitAtTop) const { DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); + STORM_LOG_THROW(metaVariable.canRepresent(value), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); // Now compute the encoding relative to the low value of the meta variable. value -= metaVariable.getLow(); @@ -121,6 +122,7 @@ namespace storm { template Bdd DdManager::getRange(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create range for meta variable."); Bdd result = this->getBddZero(); @@ -135,6 +137,7 @@ namespace storm { template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create identity for meta variable."); Add result = this->getAddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { @@ -158,6 +161,20 @@ namespace storm { return result; } + template + std::vector DdManager::cloneVariable(storm::expressions::Variable const& variable, std::string const& newMetaVariableName, boost::optional const& numberOfLayers) { + std::vector newMetaVariables; + auto const& ddMetaVariable = this->getMetaVariable(variable); + if (ddMetaVariable.getType() == storm::dd::MetaVariableType::Bool) { + newMetaVariables = this->addMetaVariable(newMetaVariableName, 3); + } else if (ddMetaVariable.getType() == storm::dd::MetaVariableType::Int) { + newMetaVariables = this->addMetaVariable(newMetaVariableName, ddMetaVariable.getLow(), ddMetaVariable.getHigh(), 3); + } else if (ddMetaVariable.getType() == storm::dd::MetaVariableType::BitVector) { + newMetaVariables = this->addBitVectorMetaVariable(newMetaVariableName, ddMetaVariable.getNumberOfDdVariables(), 3); + } + return newMetaVariables; + } + template std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional> const& position) { std::vector result = addMetaVariable(name, low, high, 2, position); @@ -166,87 +183,33 @@ namespace storm { template std::vector DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, uint64_t numberOfLayers, boost::optional> const& position) { - // Check whether number of layers is legal. - STORM_LOG_THROW(numberOfLayers >= 1, storm::exceptions::InvalidArgumentException, "Layers must be at least 1."); - - // Check whether the variable name is legal. - STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); - - // Check whether a meta variable already exists. - STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); - - // Check that the range is legal. - STORM_LOG_THROW(high >= low, storm::exceptions::InvalidArgumentException, "Illegal empty range for meta variable."); - - std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); - - // If a specific position was requested, we compute it now. - boost::optional level; - if (position) { - storm::dd::DdMetaVariable beforeVariable = this->getMetaVariable(position.get().second); - level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits::max() : std::numeric_limits::min(); - for (auto const& ddVariable : beforeVariable.getDdVariables()) { - level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel()); - } - if (position.get().first == MetaVariablePosition::Below) { - ++level.get(); - } - } - - // For the case where low and high coincide, we need to have a single bit. - if (numberOfBits == 0) { - ++numberOfBits; - } - - STORM_LOG_TRACE("Creating meta variable with " << numberOfBits << " bit(s) and " << numberOfLayers << " layer(s)."); - - std::stringstream tmp1; - std::vector result; - for (uint64 layer = 0; layer < numberOfLayers; ++layer) { - result.emplace_back(manager->declareBitVectorVariable(name + tmp1.str(), numberOfBits)); - tmp1 << "'"; - } - - std::vector>> variables(numberOfLayers); - - for (std::size_t i = 0; i < numberOfBits; ++i) { - std::vector> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level); - for (uint64 layer = 0; layer < numberOfLayers; ++layer) { - variables[layer].emplace_back(Bdd(*this, ddVariables[layer], {result[layer]})); - } - - // If we are inserting the variable at a specific level, we need to prepare the level for the next pair - // of variables. - if (level) { - level.get() += numberOfLayers; - } - } - - std::stringstream tmp2; - for (uint64_t layer = 0; layer < numberOfLayers; ++layer) { - metaVariableMap.emplace(result[layer], DdMetaVariable(name + tmp2.str(), low, high, variables[layer])); - tmp2 << "'"; - } - - return result; + return this->addMetaVariableHelper(MetaVariableType::Int, name, std::max(static_cast(std::ceil(std::log2(high - low + 1))), 1ull), numberOfLayers, position, std::make_pair(low, high)); } template std::vector DdManager::addBitVectorMetaVariable(std::string const& variableName, uint64_t bits, uint64_t numberOfLayers, boost::optional> const& position) { - return this->addMetaVariable(variableName, 0, (1ull << bits) - 1, numberOfLayers, position); + return this->addMetaVariableHelper(MetaVariableType::BitVector, variableName, bits, numberOfLayers, position); } template std::pair DdManager::addMetaVariable(std::string const& name, boost::optional> const& position) { - std::vector result = addMetaVariable(name, 2, position); + std::vector result = this->addMetaVariableHelper(MetaVariableType::Bool, name, 1, 2, position); return std::make_pair(result[0], result[1]); } template std::vector DdManager::addMetaVariable(std::string const& name, uint64_t numberOfLayers, boost::optional> const& position) { + return this->addMetaVariableHelper(MetaVariableType::Bool, name, 1, numberOfLayers, position); + } + + template + std::vector DdManager::addMetaVariableHelper(MetaVariableType const& type, std::string const& name, uint64_t numberOfDdVariables, uint64_t numberOfLayers, boost::optional> const& position, boost::optional> const& bounds) { // Check whether number of layers is legal. STORM_LOG_THROW(numberOfLayers >= 1, storm::exceptions::InvalidArgumentException, "Layers must be at least 1."); - + + // Check that the number of DD variables is legal. + STORM_LOG_THROW(numberOfDdVariables >= 1, storm::exceptions::InvalidArgumentException, "Illegal number of DD variables."); + // Check whether the variable name is legal. STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); @@ -256,7 +219,6 @@ namespace storm { // If a specific position was requested, we compute it now. boost::optional level; if (position) { - STORM_LOG_THROW(this->supportsOrderedInsertion(), storm::exceptions::NotSupportedException, "Cannot add meta variable at position, because the manager does not support ordered insertion."); storm::dd::DdMetaVariable beforeVariable = this->getMetaVariable(position.get().second); level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits::max() : std::numeric_limits::min(); for (auto const& ddVariable : beforeVariable.getDdVariables()) { @@ -267,27 +229,45 @@ namespace storm { } } + STORM_LOG_TRACE("Creating meta variable with " << numberOfDdVariables << " bit(s) and " << numberOfLayers << " layer(s)."); + std::stringstream tmp1; std::vector result; for (uint64 layer = 0; layer < numberOfLayers; ++layer) { - result.emplace_back(manager->declareBooleanVariable(name + tmp1.str())); + if (type == MetaVariableType::Int) { + result.emplace_back(manager->declareIntegerVariable(name + tmp1.str())); + } else if (type == MetaVariableType::Bool) { + result.emplace_back(manager->declareBooleanVariable(name + tmp1.str())); + } else if (type == MetaVariableType::BitVector) { + result.emplace_back(manager->declareBitVectorVariable(name + tmp1.str(), numberOfDdVariables)); + } tmp1 << "'"; } std::vector>> variables(numberOfLayers); - - std::vector> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level); - - for (uint64_t layer = 0; layer < numberOfLayers; ++layer) { - variables[layer].emplace_back(Bdd(*this, ddVariables[layer], {result[layer]})); + for (std::size_t i = 0; i < numberOfDdVariables; ++i) { + std::vector> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level); + for (uint64 layer = 0; layer < numberOfLayers; ++layer) { + variables[layer].emplace_back(Bdd(*this, ddVariables[layer], {result[layer]})); + } + + // If we are inserting the variable at a specific level, we need to prepare the level for the next pair + // of variables. + if (level) { + level.get() += numberOfLayers; + } } std::stringstream tmp2; for (uint64_t layer = 0; layer < numberOfLayers; ++layer) { - metaVariableMap.emplace(result[layer], DdMetaVariable(name + tmp2.str(), variables[layer])); + if (bounds) { + metaVariableMap.emplace(result[layer], DdMetaVariable(name + tmp2.str(), bounds.get().first, bounds.get().second, variables[layer])); + } else { + metaVariableMap.emplace(result[layer], DdMetaVariable(type, name + tmp2.str(), variables[layer])); + } tmp2 << "'"; } - + return result; } diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index 2d2405bb6..3332d1b88 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -147,6 +147,15 @@ namespace storm { */ Bdd getCube(std::set const& variables) const; + /*! + * Clones the given meta variable and optionally changes the number of layers of the variable. + * + * @param variable The variable to clone. + * @param newVariableName The name of the variable to crate. + * @param numberOfLayers The number of layers of the variable to crate + */ + std::vector cloneVariable(storm::expressions::Variable const& variable, std::string const& newVariableName, boost::optional const& numberOfLayers = boost::none); + /*! * Adds an integer meta variable with the given range with two layers (a 'normal' and a 'primed' one). * @@ -297,6 +306,15 @@ namespace storm { void debugCheck() const; private: + /*! + * Creates a meta variable with the given number of DD variables and layers. + * + * @param type The type of the meta variable to create. + * @param name The name of the variable. + * @param numberOfLayers The number of layers of this variable (must be greater or equal 1). + */ + std::vector addMetaVariableHelper(MetaVariableType const& type, std::string const& name, uint64_t numberOfDdVariables, uint64_t numberOfLayers, boost::optional> const& position = boost::none, boost::optional> const& bounds = boost::none); + /*! * Retrieves a list of names of the DD variables in the order of their index. * diff --git a/src/storm/storage/dd/DdMetaVariable.cpp b/src/storm/storage/dd/DdMetaVariable.cpp index 9cebd15cb..f05ad31b4 100644 --- a/src/storm/storage/dd/DdMetaVariable.cpp +++ b/src/storm/storage/dd/DdMetaVariable.cpp @@ -10,7 +10,16 @@ namespace storm { } template - DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables) { + DdMetaVariable::DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector> const& ddVariables) : name(name), type(type), low(0), ddVariables(ddVariables) { + STORM_LOG_ASSERT(type == MetaVariableType::Bool || type == MetaVariableType::BitVector, "Cannot create this type of meta variable in this constructor."); + if (ddVariables.size() < 63) { + this->high = (1ull << ddVariables.size()) - 1; + } + + // Correct type in the case of boolean variables. + if (ddVariables.size() == 1) { + this->type = MetaVariableType::Bool; + } this->createCube(); } @@ -31,7 +40,21 @@ namespace storm { template int_fast64_t DdMetaVariable::getHigh() const { - return this->high; + return this->high.get(); + } + + template + bool DdMetaVariable::hasHigh() const { + return static_cast(this->high); + } + + template + bool DdMetaVariable::canRepresent(int_fast64_t value) const { + bool result = value >= this->low; + if (result && high) { + return value <= this->high; + } + return false; } template diff --git a/src/storm/storage/dd/DdMetaVariable.h b/src/storm/storage/dd/DdMetaVariable.h index c18f9fa44..3bb0144cc 100644 --- a/src/storm/storage/dd/DdMetaVariable.h +++ b/src/storm/storage/dd/DdMetaVariable.h @@ -16,7 +16,7 @@ namespace storm { class Add; // An enumeration for all legal types of meta variables. - enum class MetaVariableType { Bool, Int }; + enum class MetaVariableType { Bool, Int, BitVector }; // Declare DdMetaVariable class so we can then specialize it for the different DD types. template @@ -52,6 +52,13 @@ namespace storm { */ int_fast64_t getLow() const; + /*! + * Retrieves whether the variable has an upper bound. + * + * @return True iff the variable has an upper bound. + */ + bool hasHigh() const; + /*! * Retrieves the highest value of the range of the variable. * @@ -59,6 +66,14 @@ namespace storm { */ int_fast64_t getHigh() const; + /*! + * Retrieves whether the meta variable can represent the given value. + * + * @param value The value to check for legality. + * @return True iff the value is legal. + */ + bool canRepresent(int_fast64_t value) const; + /*! * Retrieves the number of DD variables for this meta variable. * @@ -99,14 +114,15 @@ namespace storm { * @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> const& ddVariables); - + /*! * Creates a boolean meta variable with the given name. + * @param type The type of the meta variable. * @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); + DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector> const& ddVariables); /*! * Retrieves the variables used to encode the meta variable. @@ -130,7 +146,7 @@ namespace storm { int_fast64_t low; // The highest value of the range of the variable. - int_fast64_t high; + boost::optional high; // The vector of variables that are used to encode the meta variable. std::vector> ddVariables; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index c1b1c06d5..efd8f63b8 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -291,7 +291,7 @@ namespace storm { } } - void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, uint64_t factor = 1) { + void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, ValueType factor = 1) { // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero // as all states of the model have to be contained. if (transitionMatrixNode == Cudd_ReadZero(ddman)) { @@ -392,7 +392,7 @@ namespace storm { if (!skippedInTargetPartition) { extractTransitionMatrixRec(et, sourceE, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor); } - extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedInTargetPartition ? factor << 1 : factor); + extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedInTargetPartition ? 2 * factor : factor); } }