From 8d99ae4f4c4205dfff370f8346b0afbd41a9fee6 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 4 Oct 2019 12:12:22 +0200
Subject: [PATCH] Added some more trace output for sound value iteration.

---
 src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp | 1 +
 src/storm/solver/helper/SoundValueIterationHelper.cpp      | 5 +++++
 2 files changed, 6 insertions(+)

diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
index d98902694..32f18ca0a 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -81,6 +81,7 @@ namespace storm {
                     if (scc.size() == 1) {
                         returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
                     } else {
+                        STORM_LOG_TRACE("Solving SCC of size " << scc.size() << ".");
                         sccRowGroupsAsBitVector.clear();
                         sccRowsAsBitVector.clear();
                         for (auto const& group : scc) {
diff --git a/src/storm/solver/helper/SoundValueIterationHelper.cpp b/src/storm/solver/helper/SoundValueIterationHelper.cpp
index 78c541af9..9a3527d04 100644
--- a/src/storm/solver/helper/SoundValueIterationHelper.cpp
+++ b/src/storm/solver/helper/SoundValueIterationHelper.cpp
@@ -54,12 +54,14 @@ namespace storm {
             
             template<typename ValueType>
             void SoundValueIterationHelper<ValueType>::setLowerBound(ValueType const& value) {
+                STORM_LOG_TRACE("Set lower bound to " << value << ".");
                 hasLowerBound = true;
                 lowerBound = value;
             }
             
             template<typename ValueType>
             void SoundValueIterationHelper<ValueType>::setUpperBound(ValueType const& value) {
+                STORM_LOG_TRACE("Set upper bound to " << value << ".");
                 hasUpperBound = true;
                 upperBound = value;
             }
@@ -223,6 +225,7 @@ namespace storm {
                                 ValueType newDecisionValue = (xTmp[i] - xBest) / deltaY;
                                 if (!hasDecisionValue || better<dir>(newDecisionValue, decisionValue)) {
                                     decisionValue = std::move(newDecisionValue);
+                                    STORM_LOG_TRACE("Update decision value to " << decisionValue);
                                     hasDecisionValue = true;
                                 }
                             }
@@ -347,6 +350,7 @@ namespace storm {
                         }
                     }
                 }
+                STORM_LOG_TRACE("Phase 1 converged: all y values are < 1.");
                 convergencePhase1 = false;
                 return true;
             }
@@ -415,6 +419,7 @@ namespace storm {
                 if (!decisionValueBlocks && hasDecisionValue && better<dir>(decisionValue, getPrimaryBound<dir>())) {
                     getPrimaryBound<dir>() = decisionValue;
                     decisionValueBlocks = true;
+                    STORM_LOG_TRACE("Decision value blocks primary bound to " << decisionValue << ".");
                 }
             }