From 3919c475add8d4ca5d0c045bc5f8ea96fcd9b848 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:32:51 +0200 Subject: [PATCH] Added some progress information in topological solvers. --- .../solver/TopologicalLinearEquationSolver.cpp | 13 ++++++++++--- .../TopologicalMinMaxLinearEquationSolver.cpp | 11 ++++++++++- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index ba1a6e2db..76e4ce3ea 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -4,6 +4,8 @@ #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -61,7 +63,10 @@ namespace storm { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); + storm::utility::Stopwatch sccSw(true); createSortedSccDecomposition(needAdaptPrecision); + sccSw.stop(); + STORM_LOG_INFO("SCC decomposition computed in " << sccSw << ". Found " << this->sortedSccDecomposition->size() << " SCC(s) containing a total of " << x.size() << " states. Average SCC size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); } // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) @@ -69,7 +74,6 @@ namespace storm { storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); - STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get() << "."); } @@ -79,8 +83,12 @@ namespace storm { if (this->sortedSccDecomposition->size() == 1) { returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b); } else { + // Solve each SCC individually storm::storage::BitVector sccAsBitVector(x.size(), false); uint64_t sccIndex = 0; + storm::utility::ProgressMeasurement progress("states"); + progress.setMaxCount(x.size()); + progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; @@ -92,6 +100,7 @@ namespace storm { returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue; } ++sccIndex; + progress.updateProgress(sccIndex); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); break; @@ -177,8 +186,6 @@ namespace storm { if (asEquationSystem) { sccA.convertToEquationSystem(); } -// std::cout << "Solving SCC " << scc << std::endl; -// std::cout << "Matrix is " << sccA << std::endl; this->sccSolver->setMatrix(std::move(sccA)); // x Vector diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index e22b53985..7c366e436 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -5,6 +5,8 @@ #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -51,8 +53,10 @@ namespace storm { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); + storm::utility::Stopwatch sccSw(true); createSortedSccDecomposition(needAdaptPrecision); - STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); + sccSw.stop(); + STORM_LOG_INFO("SCC decomposition computed in " << sccSw << ". Found " << this->sortedSccDecomposition->size() << " SCC(s) containing a total of " << x.size() << " states. Average SCC size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); } // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) @@ -69,6 +73,7 @@ namespace storm { // Handle the case where there is just one large SCC returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b); } else { + // Solve each SCC individually if (this->isTrackSchedulerSet()) { if (this->schedulerChoices) { this->schedulerChoices.get().resize(x.size()); @@ -79,6 +84,9 @@ namespace storm { storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false); storm::storage::BitVector sccRowsAsBitVector(b.size(), false); uint64_t sccIndex = 0; + storm::utility::ProgressMeasurement progress("states"); + progress.setMaxCount(x.size()); + progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; @@ -95,6 +103,7 @@ namespace storm { returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue; } ++sccIndex; + progress.updateProgress(sccIndex); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); break;