From 7150354b9d407280108e63bd813a6d7bcb824d9c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 Mar 2018 14:32:41 +0100 Subject: [PATCH] fixing issue related to vector swapping in (explicit) value iteration and power method --- .../csl/helper/HybridCtmcCslHelper.cpp | 1 + .../IterativeMinMaxLinearEquationSolver.cpp | 16 +++++------ .../solver/NativeLinearEquationSolver.cpp | 28 +++++++++---------- .../TopologicalMinMaxLinearEquationSolver.cpp | 2 +- 4 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 841088ac2..d76a28884 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -322,6 +322,7 @@ namespace storm { // Then compute the state reward vector to use in the computation. storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false); + conversionWatch.start(); std::vector explicitTotalRewardVector = totalRewardVector.toVector(odd); conversionWatch.stop(); STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 406dd46bb..decf30b34 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -288,8 +288,6 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. uint64_t iterations = currentIterations; - std::vector* originalX = currentX; - SolverStatus status = SolverStatus::InProgress; while (status == SolverStatus::InProgress) { // Compute x' = min/max(A*x + b). @@ -315,11 +313,6 @@ namespace storm { this->showProgressIterative(iterations); } - // Swap the pointers so that the output is always in currentX. - if (originalX == newX) { - std::swap(currentX, newX); - } - return ValueIterationResult(iterations - currentIterations, status); } @@ -1282,7 +1275,9 @@ namespace storm { template template bool IterativeMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, IterativeMinMaxLinearEquationSolver const& impreciseSolver, storm::storage::SparseMatrix const& rationalA, std::vector& rationalX, std::vector const& rationalB, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector& tmpX) const { - + + std::vector const* originalX = &x; + std::vector* currentX = &x; std::vector* newX = &tmpX; @@ -1324,6 +1319,11 @@ namespace storm { } } + // Swap the two vectors if the current result is not in the original x. + if (currentX != originalX) { + std::swap(x, tmpX); + } + if (status == SolverStatus::InProgress && overallIterations == env.solver().minMax().getMaximalNumberOfIterations()) { status = SolverStatus::MaximalIterationsExceeded; } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 4251589ea..897b6522a 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -307,8 +307,6 @@ namespace storm { bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel; - std::vector* originalX = currentX; - bool converged = false; bool terminate = this->terminateNow(*currentX, guarantee); uint64_t iterations = currentIterations; @@ -320,21 +318,16 @@ namespace storm { this->multiplier->multiply(env, *currentX, &b, *newX); } - // Now check for termination. + // Check for convergence. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); + + // Check for termination. + std::swap(currentX, newX); + ++iterations; terminate = this->terminateNow(*currentX, guarantee); // Potentially show progress. this->showProgressIterative(iterations); - - // Set up next iteration. - std::swap(currentX, newX); - ++iterations; - } - - // Swap the pointers so that the output is always in currentX. - if (originalX == newX) { - std::swap(currentX, newX); } return PowerIterationResult(iterations - currentIterations, converged ? SolverStatus::Converged : (terminate ? SolverStatus::TerminatedEarly : SolverStatus::MaximalIterationsExceeded)); @@ -883,6 +876,8 @@ namespace storm { bool relative = env.solver().native().getRelativeTerminationCriterion(); auto multiplicationStyle = env.solver().native().getPowerMethodMultiplicationStyle(); + std::vector const* originalX = &x; + std::vector* currentX = &x; std::vector* newX = &tmpX; @@ -907,10 +902,10 @@ namespace storm { // Make sure that currentX and rationalX are not aliased. std::vector* temporaryRational = TemporaryHelper::getTemporary(rationalX, currentX, newX); - + // Sharpen solution and place it in the temporary rational. bool foundSolution = sharpen(p, rationalA, *currentX, rationalB, *temporaryRational); - + // After sharpen, if a solution was found, it is contained in the free rational. if (foundSolution) { @@ -923,6 +918,11 @@ namespace storm { } } + // Swap the two vectors if the current result is not in the original x. + if (currentX != originalX) { + std::swap(x, tmpX); + } + if (status == SolverStatus::InProgress && overallIterations == maxIter) { status = SolverStatus::MaximalIterationsExceeded; } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 2c8951fc3..19a2f0aef 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -58,7 +58,7 @@ namespace storm { storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); - std::cout << "Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "." << std::endl; + STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { std::cout << "Longest SCC chain size is " << this->longestSccChainSize.get() << std::endl; }