Browse Source

adding more output infos for game-based

tempestpy_adaptions
dehnert 7 years ago
parent
commit
7d8e9aa5d4
  1. 2
      src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
  2. 2
      src/storm/abstraction/prism/PrismMenuGameAbstractor.h
  3. 2
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

2
src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@ -275,7 +275,7 @@ namespace storm {
automaton.notifyGuardsArePredicates();
}
}
// Explicitly instantiate the class.
template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

2
src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@ -124,7 +124,7 @@ namespace storm {
virtual void addTerminalStates(storm::expressions::Expression const& expression) override;
virtual void notifyGuardsArePredicates() override;
protected:
using MenuGameAbstractor<DdType, ValueType>::exportToDot;

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 (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() << " predicates << (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