better logging

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()) {

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>

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();