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 void SoundValueIterationHelper::setLowerBound(ValueType const& value) { + STORM_LOG_TRACE("Set lower bound to " << value << "."); hasLowerBound = true; lowerBound = value; } template void SoundValueIterationHelper::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(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(decisionValue, getPrimaryBound())) { getPrimaryBound() = decisionValue; decisionValueBlocks = true; + STORM_LOG_TRACE("Decision value blocks primary bound to " << decisionValue << "."); } }