Browse Source

more debug output

Former-commit-id: ff8f9b5a81
tempestpy_adaptions
dehnert 9 years ago
parent
commit
b2cec6395a
  1. 5
      src/builder/DdPrismModelBuilder.cpp

5
src/builder/DdPrismModelBuilder.cpp

@ -621,6 +621,8 @@ namespace storm {
std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first; storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
transitionMatrix.exportToDot("trans.dot"); transitionMatrix.exportToDot("trans.dot");
std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
std::cout << "node: " << transitionMatrix.getNodeCount() << std::endl;
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
// Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because // 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); transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
} }
storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); 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(); storm::dd::Add<Type> reachableStatesAdd = reachableStates.toAdd();
transitionMatrix *= reachableStatesAdd; transitionMatrix *= reachableStatesAdd;
if (stateAndTransitionRewards) { if (stateAndTransitionRewards) {

Loading…
Cancel
Save