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

Former-commit-id: ff8f9b5a81717d597e1b423f82d7f77b22af84eb
---
 src/builder/DdPrismModelBuilder.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 07a5f1100..69aea3119 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -621,6 +621,8 @@ namespace storm {
             std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
             storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
             transitionMatrix.exportToDot("trans.dot");
+            std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
+            std::cout << "node: " << transitionMatrix.getNodeCount() << 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
@@ -651,6 +653,9 @@ 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) {