From 3a206784a374f0769e4e7248f84205379f6f261d Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Tue, 2 Jun 2020 19:44:27 -0700
Subject: [PATCH] better logging

---
 src/storm-pomdp-cli/storm-pomdp.cpp           |  5 +++--
 .../MemlessStrategySearchQualitative.cpp      | 20 +++++++++----------
 .../MemlessStrategySearchQualitative.h        |  1 +
 3 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 891426d49..7607c356c 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -143,7 +143,9 @@ namespace storm {
             void performQualitativeAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& origpomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) {
                 auto const& qualSettings = storm::settings::getModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
                 auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
-
+                std::stringstream sstr;
+                origpomdp->printModelInformationToStream(sstr);
+                STORM_LOG_INFO(sstr.str());
                 STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type.");
                 STORM_LOG_TRACE("Run qualitative preprocessing...");
                 storm::models::sparse::Pomdp<ValueType> pomdp(*origpomdp);
@@ -161,7 +163,6 @@ namespace storm {
                 if (lookahead == 0) {
                     lookahead = pomdp.getNumberOfStates();
                 }
-                STORM_LOG_TRACE("target states: "  << targetStates);
                 if (qualSettings.getMemlessSearchMethod() == "one-shot") {
                     storm::pomdp::QualitativeStrategySearchNaive<ValueType> memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
                     if (qualSettings.isWinningRegionSet()) {
diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
index 4b69bc7d8..1eb9f4c85 100644
--- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
+++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
@@ -35,16 +35,16 @@ namespace storm {
 
         template <typename ValueType>
         void MemlessStrategySearchQualitative<ValueType>::Statistics::print() const {
-            STORM_PRINT_AND_LOG("Total time: " << totalTimer << std::endl);
-            STORM_PRINT_AND_LOG("SAT Calls " << satCalls << std::endl);
-            STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer << std::endl);
-            STORM_PRINT_AND_LOG("Outer iterations: " << outerIterations << std::endl);
-            STORM_PRINT_AND_LOG("Solver initialization time: " << initializeSolverTimer << std::endl);
-            STORM_PRINT_AND_LOG("Obtain partial scheduler time: " << evaluateExtensionSolverTime << std::endl);
-            STORM_PRINT_AND_LOG("Update solver to extend partial scheduler time: " << encodeExtensionSolverTime << std::endl);
-            STORM_PRINT_AND_LOG("Update solver with new scheduler time: " << updateNewStrategySolverTime << std::endl);
-            STORM_PRINT_AND_LOG("Winning regions update time: " << winningRegionUpdatesTimer << std::endl);
-            STORM_PRINT_AND_LOG("Graph search time: " << graphSearchTime << std::endl);
+            STORM_PRINT_AND_LOG("Total time: " << totalTimer);
+            STORM_PRINT_AND_LOG("SAT Calls " << satCalls);
+            STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer);
+            STORM_PRINT_AND_LOG("Outer iterations: " << outerIterations);
+            STORM_PRINT_AND_LOG("Solver initialization time: " << initializeSolverTimer);
+            STORM_PRINT_AND_LOG("Obtain partial scheduler time: " << evaluateExtensionSolverTime);
+            STORM_PRINT_AND_LOG("Update solver to extend partial scheduler time: " << encodeExtensionSolverTime);
+            STORM_PRINT_AND_LOG("Update solver with new scheduler time: " << updateNewStrategySolverTime);
+            STORM_PRINT_AND_LOG("Winning regions update time: " << winningRegionUpdatesTimer);
+            STORM_PRINT_AND_LOG("Graph search time: " << graphSearchTime);
         }
 
         template <typename ValueType>
diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h
index c60117602..ec292af1c 100644
--- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h
+++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h
@@ -207,6 +207,7 @@ namespace pomdp {
         storm::expressions::Expression const& getDoneActionExpression(uint64_t obs) const;
 
         void reset () {
+            STORM_LOG_INFO("Reset solver to restart with current winning region");
             schedulerForObs.clear();
             finalSchedulers.clear();
             smtSolver->reset();