From 44cd4376a0e46de346c5f5be18d72aa7f7fadb1d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 14 Mar 2017 18:35:21 +0100 Subject: [PATCH] disabled iterative lin eq. solver restarts as this does not significantly improve the runtimes --- src/storm/solver/GameSolver.cpp | 45 +------------- .../StandardMinMaxLinearEquationSolver.cpp | 59 +------------------ .../StandardMinMaxLinearEquationSolver.h | 2 - 3 files changed, 3 insertions(+), 103 deletions(-) diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index d985fe5da..57180a1b6 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -56,49 +56,8 @@ namespace storm { submatrixSolver->setCachingEnabled(true); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } - ValueType linEqPrecision = this->getPrecision(); - uint_fast64_t hintIterations = 0; - std::vector otherTmpResult(tmpResult.size()); - bool vectorsNotEqual = false; - do { - vectorsNotEqual = false; - // Set the precision of the underlying solver - auto* gmmSolver = dynamic_cast*>(submatrixSolver.get()); - auto* nativeSolver = dynamic_cast*>(submatrixSolver.get()); - auto* eigenSolver = dynamic_cast*>(submatrixSolver.get()); - auto* eliminationSolver = dynamic_cast*>(submatrixSolver.get()); - if (gmmSolver) { - auto newSettings = gmmSolver->getSettings(); - newSettings.setPrecision(linEqPrecision); - gmmSolver->setSettings(newSettings); - } else if (nativeSolver) { - auto newSettings = nativeSolver->getSettings(); - newSettings.setPrecision(linEqPrecision); - nativeSolver->setSettings(newSettings); - } else if (eigenSolver) { - eigenSolver->getSettings().setPrecision(linEqPrecision); - } else if (eliminationSolver) { - // elimination solver does not consider a precision so nothing to do - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented"); - } - - // invoke the solver - submatrixSolver->solveEquations(x, tmpResult); - submatrixSolver->multiply(x, nullptr, otherTmpResult); - linEqPrecision *= storm::utility::convertNumber(0.5); - ++hintIterations; - auto otherTmpResIt = otherTmpResult.begin(); - auto xIt = x.begin(); - for(auto tmpResIt = tmpResult.begin(); tmpResIt != tmpResult.end(); ++tmpResIt) { - if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) { - vectorsNotEqual = true; - break; - } - ++otherTmpResIt; ++xIt; - } - } while (vectorsNotEqual); - STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hints in GameSolver"); + // invoke the solver + submatrixSolver->solveEquations(x, tmpResult); } // Now perform the actual value iteration. diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index e4ad81603..224719c50 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -113,7 +113,6 @@ namespace storm { // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. auto solver = linearEquationSolverFactory->create(std::move(submatrix)); - setPrecisionRelativeOfLinearEquationSolver(solver, this->getPrecision(), this->getRelative()); if (this->lowerBound) { solver->setLowerBound(this->lowerBound.get()); } @@ -244,31 +243,7 @@ namespace storm { submatrixSolver->setCachingEnabled(true); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } - ValueType linEqPrecision = this->getPrecision(); - // Temporarily shrink the auxiliary row vector - auxiliaryRowVector->resize(A.getRowGroupCount()); - auxiliaryRowVector->reserve(A.getRowCount()); - uint_fast64_t hintIterations = 0; - bool vectorsNotEqual = false; - do { - vectorsNotEqual = false; - setPrecisionRelativeOfLinearEquationSolver(submatrixSolver, linEqPrecision, this->getRelative()); - submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); - submatrixSolver->multiply(x, nullptr, *auxiliaryRowVector); - linEqPrecision *= storm::utility::convertNumber(0.5); - ++hintIterations; - auto otherTmpResIt = auxiliaryRowVector->begin(); - auto xIt = x.begin(); - for(auto tmpResIt = auxiliaryRowGroupVector->begin(); tmpResIt != auxiliaryRowGroupVector->end(); ++tmpResIt) { - if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) { - vectorsNotEqual = true; - break; - } - ++otherTmpResIt; ++xIt; - } - } while (vectorsNotEqual); - STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hint"); - auxiliaryRowVector->resize(A.getRowCount()); + submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); } std::vector* newX = auxiliaryRowGroupVector.get(); @@ -377,38 +352,6 @@ namespace storm { } } - - template - void StandardMinMaxLinearEquationSolver::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr>& linEqSolver, ValueType precision, bool relative) const { - auto* gmmSolver = dynamic_cast*>(linEqSolver.get()); - auto* nativeSolver = dynamic_cast*>(linEqSolver.get()); - auto* eigenSolver = dynamic_cast*>(linEqSolver.get()); - auto* eliminationSolver = dynamic_cast*>(linEqSolver.get()); - if (gmmSolver) { - auto newSettings = gmmSolver->getSettings(); - newSettings.setPrecision(precision); - newSettings.setRelativeTerminationCriterion(relative); - gmmSolver->setSettings(newSettings); - } else if (nativeSolver) { - auto newSettings = nativeSolver->getSettings(); - newSettings.setPrecision(precision); - newSettings.setRelativeTerminationCriterion(relative); - nativeSolver->setSettings(newSettings); - } else if (eigenSolver) { - eigenSolver->getSettings().setPrecision(precision); - // no relative flag for eigen solver - } else if (eliminationSolver) { - // elimination solver does not consider a precision so nothing to do - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented"); - } - } - - template<> - void StandardMinMaxLinearEquationSolver::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr>& linEqSolver, storm::RationalNumber precision, bool relative) const { - // Intentionally left empty - } - template StandardMinMaxLinearEquationSolverSettings const& StandardMinMaxLinearEquationSolver::getSettings() const { return settings; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index 0b33aef35..f7e1e40c6 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -66,8 +66,6 @@ namespace storm { Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; void reportStatus(Status status, uint64_t iterations) const; - void setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr>& linEqSolver, ValueType precision, bool relative) const; - /// The settings of this solver. StandardMinMaxLinearEquationSolverSettings settings;