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, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); storm::dd::Add 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 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 reachableStatesAdd = reachableStates.toAdd(); transitionMatrix *= reachableStatesAdd; if (stateAndTransitionRewards) {