sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added some progress information in topological solvers.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
3f2a5ffa62
commit
3919c475ad
2 changed files with 20 additions and 4 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 13
      src/storm/solver/TopologicalLinearEquationSolver.cpp
  2. 11
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

13
src/storm/solver/TopologicalLinearEquationSolver.cpp
View File

@ -4,6 +4,8 @@
#include "storm/utility/constants.h" #include "storm/utility/constants.h"
#include "storm/utility/vector.h" #include "storm/utility/vector.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/ProgressMeasurement.h"
#include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/UnexpectedException.h"
@ -61,7 +63,10 @@ namespace storm {
if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) {
STORM_LOG_TRACE("Creating SCC decomposition."); STORM_LOG_TRACE("Creating SCC decomposition.");
storm::utility::Stopwatch sccSw(true);
createSortedSccDecomposition(needAdaptPrecision); 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<double>(this->getMatrixRowCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << ".");
} }
// We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) // 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::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision);
STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast<double>(this->getMatrixRowCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << ".");
if (this->longestSccChainSize) { if (this->longestSccChainSize) {
STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get() << "."); STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get() << ".");
} }
@ -79,8 +83,12 @@ namespace storm {
if (this->sortedSccDecomposition->size() == 1) { if (this->sortedSccDecomposition->size() == 1) {
returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b); returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b);
} else { } else {
// Solve each SCC individually
storm::storage::BitVector sccAsBitVector(x.size(), false); storm::storage::BitVector sccAsBitVector(x.size(), false);
uint64_t sccIndex = 0; uint64_t sccIndex = 0;
storm::utility::ProgressMeasurement progress("states");
progress.setMaxCount(x.size());
progress.startNewMeasurement(0);
for (auto const& scc : *this->sortedSccDecomposition) { for (auto const& scc : *this->sortedSccDecomposition) {
if (scc.size() == 1) { if (scc.size() == 1) {
returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue;
@ -92,6 +100,7 @@ namespace storm {
returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue; returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue;
} }
++sccIndex; ++sccIndex;
progress.updateProgress(sccIndex);
if (storm::utility::resources::isTerminate()) { if (storm::utility::resources::isTerminate()) {
STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs.");
break; break;
@ -177,8 +186,6 @@ namespace storm {
if (asEquationSystem) { if (asEquationSystem) {
sccA.convertToEquationSystem(); sccA.convertToEquationSystem();
} }
// std::cout << "Solving SCC " << scc << std::endl;
// std::cout << "Matrix is " << sccA << std::endl;
this->sccSolver->setMatrix(std::move(sccA)); this->sccSolver->setMatrix(std::move(sccA));
// x Vector // x Vector

11
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -5,6 +5,8 @@
#include "storm/utility/constants.h" #include "storm/utility/constants.h"
#include "storm/utility/vector.h" #include "storm/utility/vector.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/ProgressMeasurement.h"
#include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/UnexpectedException.h"
@ -51,8 +53,10 @@ namespace storm {
if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) {
STORM_LOG_TRACE("Creating SCC decomposition."); STORM_LOG_TRACE("Creating SCC decomposition.");
storm::utility::Stopwatch sccSw(true);
createSortedSccDecomposition(needAdaptPrecision); createSortedSccDecomposition(needAdaptPrecision);
STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast<double>(this->A->getRowGroupCount()) / static_cast<double>(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<double>(this->A->getRowGroupCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << ".");
} }
// We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) // 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 // Handle the case where there is just one large SCC
returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b); returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b);
} else { } else {
// Solve each SCC individually
if (this->isTrackSchedulerSet()) { if (this->isTrackSchedulerSet()) {
if (this->schedulerChoices) { if (this->schedulerChoices) {
this->schedulerChoices.get().resize(x.size()); this->schedulerChoices.get().resize(x.size());
@ -79,6 +84,9 @@ namespace storm {
storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false); storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false);
storm::storage::BitVector sccRowsAsBitVector(b.size(), false); storm::storage::BitVector sccRowsAsBitVector(b.size(), false);
uint64_t sccIndex = 0; uint64_t sccIndex = 0;
storm::utility::ProgressMeasurement progress("states");
progress.setMaxCount(x.size());
progress.startNewMeasurement(0);
for (auto const& scc : *this->sortedSccDecomposition) { for (auto const& scc : *this->sortedSccDecomposition) {
if (scc.size() == 1) { if (scc.size() == 1) {
returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
@ -95,6 +103,7 @@ namespace storm {
returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue; returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue;
} }
++sccIndex; ++sccIndex;
progress.updateProgress(sccIndex);
if (storm::utility::resources::isTerminate()) { if (storm::utility::resources::isTerminate()) {
STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs.");
break; break;

Write Preview
Loading…
Cancel
Save