From 7d8e9aa5d44604e6e6ec52c5b9317588f7b97eaf Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 19 May 2018 08:30:25 +0200
Subject: [PATCH] adding more output infos for game-based

---
 src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp           | 2 +-
 src/storm/abstraction/prism/PrismMenuGameAbstractor.h           | 2 +-
 src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
index ffa590a57..be4e33d8e 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
+++ b/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>;
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
index 5815c915a..a9ef79413 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/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;
                 
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index c6fd3cf6b..2b545a54b 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/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();