Browse Source

overhauled output slightly

tempestpy_adaptions
dehnert 7 years ago
parent
commit
9e0d88e212
  1. 2
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

2
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -564,7 +564,7 @@ namespace storm {
auto abstractionStart = std::chrono::high_resolution_clock::now();
storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
auto abstractionEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states, " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicates << (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
STORM_LOG_INFO("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states, " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
// (2) Prepare initial, constraint and target state BDDs for later use.
storm::dd::Bdd<Type> initialStates = game.getInitialStates();

Loading…
Cancel
Save