Browse Source

Changed naming of DD variables belonging to one meta variable slightly: only integer-valued meta variables now get a '.i' suffix to denote their i-th bit.

Former-commit-id: 771312ac31
tempestpy_adaptions
dehnert 11 years ago
parent
commit
e79fa50999
  1. 7
      src/storage/dd/CuddDd.h
  2. 10
      src/storage/dd/CuddDdManager.cpp

7
src/storage/dd/CuddDd.h

@ -511,8 +511,9 @@ namespace storm {
/*!
* Converts the DD into a (heavily nested) if-then-else expression that represents the very same function.
* The variable names used in the expression are derived from the meta variable name with a suffix ".i"
* expressing that the variable is the i-th bit of the meta variable.
* The variable names used in the expression are derived from the meta variable name and are extended with a
* suffix ".i" if the meta variable is integer-valued, expressing that the variable is the i-th bit of the
* meta variable.
*
* @return The resulting expression.
*/
@ -562,7 +563,7 @@ namespace storm {
*
* @param ddManager The manager responsible for this DD.
* @param cuddAdd The CUDD ADD to store.
* @param
* @param containedMetaVariableNames The names of the meta variables that appear in the DD.
*/
Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>());

10
src/storage/dd/CuddDdManager.cpp

@ -183,8 +183,14 @@ namespace storm {
std::vector<std::pair<ADD, std::string>> variableNamePairs;
for (auto const& nameMetaVariablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> const& metaVariable = nameMetaVariablePair.second;
for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex));
// If the meta variable is of type bool, we don't need to suffix it with the bit number.
if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
variableNamePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), metaVariable.getName());
} else {
// For integer-valued meta variables, we, however, have to add the suffix.
for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex));
}
}
}

Loading…
Cancel
Save