From 507331d8a92fbf3dc8e45bf16a8013347cbb9bbd Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 14:47:56 +0200
Subject: [PATCH] more debug output

Former-commit-id: acb7f9ea2f17ee903b05436aa3088640d92feb2a
---
 src/builder/DdPrismModelBuilder.cpp | 4 +---
 src/storage/dd/CuddAdd.cpp          | 8 +++++++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 69aea3119..2d94be7cc 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -623,6 +623,7 @@ namespace storm {
             transitionMatrix.exportToDot("trans.dot");
             std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
             std::cout << "node: " << transitionMatrix.getNodeCount() << std::endl;
+            std::cout << "trans: " << transitionMatrix << std::endl;
             ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
             
             // Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because
@@ -653,9 +654,6 @@ namespace storm {
                 transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
             }
             storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
-            reachableStates.exportToDot("reach.dot");
-            std::cout << "reach nnz: " << reachableStates.getNonZeroCount() << std::endl;
-            std::cout << "reach node: " << reachableStates.getNodeCount() << std::endl;
             storm::dd::Add<Type> reachableStatesAdd = reachableStates.toAdd();
             transitionMatrix *= reachableStatesAdd;
             if (stateAndTransitionRewards) {
diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp
index 5eaded696..dbee2e94a 100644
--- a/src/storage/dd/CuddAdd.cpp
+++ b/src/storage/dd/CuddAdd.cpp
@@ -1,5 +1,6 @@
 #include <cstring>
 #include <algorithm>
+#include <boost/algorithm/string/join.hpp>
 
 #include "src/storage/dd/CuddAdd.h"
 #include "src/storage/dd/CuddBdd.h"
@@ -1055,7 +1056,12 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& out, const Add<DdType::CUDD>& add) {
-            add.exportToDot();
+            out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl;
+            std::vector<std::string> variableNames;
+            for (auto const& variable : add.getContainedMetaVariables()) {
+                variableNames.push_back(variable.getName());
+            }
+            out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl;
             return out;
         }