diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 068d08b63..e3c734bf0 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -194,7 +194,8 @@ namespace storm { std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero()); solver->solveEquations(env, ecQuotient->auxStateValues, ecQuotient->auxChoiceValues); - + this->overallPerformedIterations += solver->overallPerformedIterations; + solver->overallPerformedIterations = 0; this->weightedResult = std::vector(transitionMatrix.getRowGroupCount()); transformReducedSolutionToOriginalModel(ecQuotient->matrix, ecQuotient->auxStateValues, solver->getSchedulerChoices(), ecQuotient->ecqToOriginalChoiceMapping, ecQuotient->originalToEcqStateMapping, this->weightedResult, this->optimalChoices); @@ -277,6 +278,8 @@ namespace storm { STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); solver->solveEquations(env, x, b); + this->overallPerformedIterations += solver->overallPerformedIterations; + solver->overallPerformedIterations = 0; // Set the result for this objective accordingly storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index 2f0a27f33..10cba6fbc 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -37,7 +37,13 @@ namespace storm { StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~StandardPcaaWeightVectorChecker() = default; + virtual ~StandardPcaaWeightVectorChecker() { + if (overallPerformedIterations != 0) { + std::cout << "PERFORMEDITERATIONS: " << overallPerformedIterations << std::endl; + } + } + + mutable uint64_t overallPerformedIterations = 0; /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 476399bfa..7d9013566 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -3,7 +3,7 @@ #include #include - +#include #include #include "storm/solver/TerminationCondition.h" @@ -17,6 +17,15 @@ namespace storm { public: AbstractEquationSolver(); + virtual ~AbstractEquationSolver() { + if (overallPerformedIterations != 0) { + std::cout << "PERFORMEDITERATIONS: " << overallPerformedIterations << std::endl; + } + } + + mutable uint64_t overallPerformedIterations = 0; + + /*! * Sets a custom termination condition that is used together with the regular termination condition of the * solver. diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 0acb770fe..78faa6a8a 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -582,7 +582,8 @@ namespace storm { } reportStatus(status, iterations); - + this->overallPerformedIterations += iterations; + // We take the means of the lower and upper bound so we guarantee the desired precision. ValueType two = storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(*lowerX, *upperX, *lowerX, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; }); @@ -718,90 +719,6 @@ namespace storm { } } - void performIterationStepMax(storm::storage::SparseMatrix const& A, std::vector const& b) { - if (!decisionValueBlocks) { - performIterationStepUpdateDecisionValueMax(A, b); - } else { - assert(decisionValue == upperBound); - auto xIt = x.rbegin(); - auto yIt = y.rbegin(); - auto groupStartIt = A.getRowGroupIndices().rbegin(); - uint64_t groupEnd = *groupStartIt; - ++groupStartIt; - for (auto groupStartIte = A.getRowGroupIndices().rend(); groupStartIt != groupStartIte; groupEnd = *(groupStartIt++), ++xIt, ++yIt) { - // Perform the iteration for the first row in the group - uint64_t row = *groupStartIt; - ValueType xBest, yBest; - multiplyRow(row, A, b[row], xBest, yBest); - ++row; - // Only do more work if there are still rows in this row group - if (row != groupEnd) { - ValueType xi, yi; - ValueType bestValue = xBest + yBest * upperBound; - for (;row < groupEnd; ++row) { - // Get the multiplication results - multiplyRow(row, A, b[row], xi, yi); - ValueType currentValue = xi + yi * upperBound; - // Check if the current row is better then the previously found one - if (currentValue > bestValue) { - xBest = std::move(xi); - yBest = std::move(yi); - bestValue = std::move(currentValue); - } else if (currentValue == bestValue && yBest > yi) { - // If the value for this row is not strictly better, it might still be equal and have a better y value - xBest = std::move(xi); - yBest = std::move(yi); - } - } - } - *xIt = std::move(xBest); - *yIt = std::move(yBest); - } - } - } - - void performIterationStepMin(storm::storage::SparseMatrix const& A, std::vector const& b) { - if (!decisionValueBlocks) { - performIterationStepUpdateDecisionValueMin(A, b); - } else { - assert(decisionValue == lowerBound); - auto xIt = x.rbegin(); - auto yIt = y.rbegin(); - auto groupStartIt = A.getRowGroupIndices().rbegin(); - uint64_t groupEnd = *groupStartIt; - ++groupStartIt; - for (auto groupStartIte = A.getRowGroupIndices().rend(); groupStartIt != groupStartIte; groupEnd = *(groupStartIt++), ++xIt, ++yIt) { - // Perform the iteration for the first row in the group - uint64_t row = *groupStartIt; - ValueType xBest, yBest; - multiplyRow(row, A, b[row], xBest, yBest); - ++row; - // Only do more work if there are still rows in this row group - if (row != groupEnd) { - ValueType xi, yi; - ValueType bestValue = xBest + yBest * lowerBound; - for (;row < groupEnd; ++row) { - // Get the multiplication results - multiplyRow(row, A, b[row], xi, yi); - ValueType currentValue = xi + yi * lowerBound; - // Check if the current row is better then the previously found one - if (currentValue < bestValue) { - xBest = std::move(xi); - yBest = std::move(yi); - bestValue = std::move(currentValue); - } else if (currentValue == bestValue && yBest > yi) { - // If the value for this row is not strictly better, it might still be equal and have a better y value - xBest = std::move(xi); - yBest = std::move(yi); - } - } - } - *xIt = std::move(xBest); - *yIt = std::move(yBest); - } - } - } - template void performIterationStepUpdateDecisionValue(storm::storage::SparseMatrix const& A, std::vector const& b) { auto xIt = x.rbegin(); @@ -883,166 +800,6 @@ namespace storm { } } - void performIterationStepUpdateDecisionValueMax(storm::storage::SparseMatrix const& A, std::vector const& b) { - auto xIt = x.rbegin(); - auto yIt = y.rbegin(); - auto groupStartIt = A.getRowGroupIndices().rbegin(); - uint64_t groupEnd = *groupStartIt; - ++groupStartIt; - for (auto groupStartIte = A.getRowGroupIndices().rend(); groupStartIt != groupStartIte; groupEnd = *(groupStartIt++), ++xIt, ++yIt) { - // Perform the iteration for the first row in the group - uint64_t row = *groupStartIt; - ValueType xBest, yBest; - multiplyRow(row, A, b[row], xBest, yBest); - ++row; - // Only do more work if there are still rows in this row group - if (row != groupEnd) { - ValueType xi, yi; - uint64_t xyTmpIndex = 0; - if (hasUpperBound) { - ValueType bestValue = xBest + yBest * upperBound; - for (;row < groupEnd; ++row) { - // Get the multiplication results - multiplyRow(row, A, b[row], xi, yi); - ValueType currentValue = xi + yi * upperBound; - // Check if the current row is better then the previously found one - if (currentValue > bestValue) { - if (yBest < yi) { - // We need to store the 'old' best value as it might be relevant for the decision value - xTmp[xyTmpIndex] = std::move(xBest); - yTmp[xyTmpIndex] = std::move(yBest); - ++xyTmpIndex; - } - xBest = std::move(xi); - yBest = std::move(yi); - bestValue = std::move(currentValue); - } else if (yBest > yi) { - // If the value for this row is not strictly better, it might still be equal and have a better y value - if (currentValue == bestValue) { - xBest = std::move(xi); - yBest = std::move(yi); - } else { - xTmp[xyTmpIndex] = std::move(xi); - yTmp[xyTmpIndex] = std::move(yi); - ++xyTmpIndex; - } - } - } - } else { - for (;row < groupEnd; ++row) { - multiplyRow(row, A, b[row], xi, yi); - // Update the best choice - if (yi > yBest || (yi == yBest && xi > xBest)) { - xTmp[xyTmpIndex] = std::move(xBest); - yTmp[xyTmpIndex] = std::move(yBest); - ++xyTmpIndex; - xBest = std::move(xi); - yBest = std::move(yi); - } else { - xTmp[xyTmpIndex] = std::move(xi); - yTmp[xyTmpIndex] = std::move(yi); - ++xyTmpIndex; - } - } - } - - // Update the decision value - for (uint64_t i = 0; i < xyTmpIndex; ++i) { - ValueType deltaY = yBest - yTmp[i]; - if (deltaY > storm::utility::zero()) { - ValueType newDecisionValue = (xTmp[i] - xBest) / deltaY; - if (!hasDecisionValue || newDecisionValue > decisionValue) { - decisionValue = std::move(newDecisionValue); - hasDecisionValue = true; - } - } - } - } - *xIt = std::move(xBest); - *yIt = std::move(yBest); - } - } - - void performIterationStepUpdateDecisionValueMin(storm::storage::SparseMatrix const& A, std::vector const& b) { - auto xIt = x.rbegin(); - auto yIt = y.rbegin(); - auto groupStartIt = A.getRowGroupIndices().rbegin(); - uint64_t groupEnd = *groupStartIt; - ++groupStartIt; - for (auto groupStartIte = A.getRowGroupIndices().rend(); groupStartIt != groupStartIte; groupEnd = *(groupStartIt++), ++xIt, ++yIt) { - // Perform the iteration for the first row in the group - uint64_t row = *groupStartIt; - ValueType xBest, yBest; - multiplyRow(row, A, b[row], xBest, yBest); - ++row; - // Only do more work if there are still rows in this row group - if (row != groupEnd) { - ValueType xi, yi; - uint64_t xyTmpIndex = 0; - if (hasLowerBound) { - ValueType bestValue = xBest + yBest * lowerBound; - for (;row < groupEnd; ++row) { - // Get the multiplication results - multiplyRow(row, A, b[row], xi, yi); - ValueType currentValue = xi + yi * lowerBound; - // Check if the current row is better then the previously found one - if (currentValue < bestValue) { - if (yBest < yi) { - // We need to store the 'old' best value as it might be relevant for the decision value - xTmp[xyTmpIndex] = std::move(xBest); - yTmp[xyTmpIndex] = std::move(yBest); - ++xyTmpIndex; - } - xBest = std::move(xi); - yBest = std::move(yi); - bestValue = std::move(currentValue); - } else if (yBest > yi) { - // If the value for this row is not strictly better, it might still be equal and have a better y value - if (currentValue == bestValue) { - xBest = std::move(xi); - yBest = std::move(yi); - } else { - xTmp[xyTmpIndex] = std::move(xi); - yTmp[xyTmpIndex] = std::move(yi); - ++xyTmpIndex; - } - } - } - } else { - for (;row < groupEnd; ++row) { - multiplyRow(row, A, b[row], xi, yi); - // Update the best choice - if (yi > yBest || (yi == yBest && xi < xBest)) { - xTmp[xyTmpIndex] = std::move(xBest); - yTmp[xyTmpIndex] = std::move(yBest); - ++xyTmpIndex; - xBest = std::move(xi); - yBest = std::move(yi); - } else { - xTmp[xyTmpIndex] = std::move(xi); - yTmp[xyTmpIndex] = std::move(yi); - ++xyTmpIndex; - } - } - } - - // Update the decision value - for (uint64_t i = 0; i < xyTmpIndex; ++i) { - ValueType deltaY = yBest - yTmp[i]; - if (deltaY > storm::utility::zero()) { - ValueType newDecisionValue = (xTmp[i] - xBest) / deltaY; - if (!hasDecisionValue || newDecisionValue < decisionValue) { - decisionValue = std::move(newDecisionValue); - hasDecisionValue = true; - } - } - } - } - *xIt = std::move(xBest); - *yIt = std::move(yBest); - } - } - bool checkRestartCriterion() { return false; // iterations <= restartMaxIterations && (minimize(dir) ? restartThreshold * improvedPrimaryBound > primaryBound : restartThreshold * primaryBound > improvedPrimaryBound @@ -1249,13 +1006,13 @@ namespace storm { while (status == SolverStatus::InProgress && iterations < env.solver().minMax().getMaximalNumberOfIterations()) { if (minimize(dir)) { - helper.template performIterationStepMin(*this->A, b); + helper.template performIterationStep(*this->A, b); if (helper.template checkConvergenceUpdateBounds(iterations, relevantValuesPtr)) { status = SolverStatus::Converged; } } else { assert(maximize(dir)); - helper.template performIterationStepMax(*this->A, b); + helper.template performIterationStep(*this->A, b); if (helper.template checkConvergenceUpdateBounds(iterations, relevantValuesPtr)) { status = SolverStatus::Converged; } @@ -1279,6 +1036,8 @@ namespace storm { reportStatus(status, iterations); + this->overallPerformedIterations += iterations; + if (!this->isCachingEnabled()) { clearCache(); } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index b82737803..ad1c9136c 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -549,7 +549,8 @@ namespace storm { if (!this->isCachingEnabled()) { clearCache(); } - + this->overallPerformedIterations += iterations; + this->logIterations(converged, terminate, iterations); return converged; @@ -734,7 +735,8 @@ namespace storm { if (!this->isCachingEnabled()) { clearCache(); } - + this->overallPerformedIterations += iterations; + this->logIterations(converged, terminate, iterations); STORM_LOG_WARN_COND(hasMinValueBound && hasMaxValueBound, "Could not compute lower or upper bound within the given number of iterations."); STORM_LOG_INFO("Quick Power Iteration terminated with lower value bound " << minValueBound << " and upper value bound " << maxValueBound << "."); diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 83825d562..35994357b 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -91,6 +91,7 @@ namespace storm { for (auto const& scc : *this->sortedSccDecomposition) { if (scc.isTrivial()) { returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; + ++this->overallPerformedIterations; } else { sccAsBitVector.clear(); for (auto const& state : scc) { @@ -101,9 +102,16 @@ namespace storm { } } + if (this->sccSolver) { + this->overallPerformedIterations += this->sccSolver->overallPerformedIterations; + this->sccSolver->overallPerformedIterations = 0; + } if (!this->isCachingEnabled()) { clearCache(); } + + + return returnValue; } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 1ba0c7467..92d909189 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -109,6 +109,7 @@ namespace storm { for (auto const& scc : *this->sortedSccDecomposition) { if (scc.isTrivial()) { returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; + ++this->overallPerformedIterations; } else { sccRowGroupsAsBitVector.clear(); sccRowsAsBitVector.clear(); @@ -132,6 +133,12 @@ namespace storm { } } + if (this->sccSolver) { + this->overallPerformedIterations += this->sccSolver->overallPerformedIterations; + this->sccSolver->overallPerformedIterations = 0; + } + + if (!this->isCachingEnabled()) { clearCache(); }