From e79fa509998e29e3905c4cbf947af504d21e69bf Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 31 May 2014 21:29:18 +0200
Subject: [PATCH] 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: 771312ac31357dae28db63a98ad55dcd86ad1b18
---
 src/storage/dd/CuddDd.h          |  7 ++++---
 src/storage/dd/CuddDdManager.cpp | 10 ++++++++--
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index bf879fa34..279b2c2fa 100644
--- a/src/storage/dd/CuddDd.h
+++ b/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>());
             
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index fd26a782c..f23734ad2 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/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));
+                    }
                 }
             }