From 49f59052f835a42e944af32702c7264f7a4dcd40 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Jun 2016 18:27:20 +0200 Subject: [PATCH] made model checkers give up possession of matrix to solver when possible Former-commit-id: 8d689470bdc807da7ddd029f674e14b01ae21e10 --- src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 6 +++--- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 10 +++++----- src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp | 10 +++++----- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 6 +++--- src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 6 +++--- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 0dddea5cb..f5a057d6f 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -283,7 +283,7 @@ namespace storm { } std::vector multiplicationResult(result.size()); - std::unique_ptr> solver = linearEquationSolverFactory.create(uniformizedMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix)); if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) { // Perform the matrix-vector multiplications (without adding). @@ -557,7 +557,7 @@ namespace storm { bsccEquationSystem = builder.build(); { - std::unique_ptr> solver = linearEquationSolverFactory.create(bsccEquationSystem); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(bsccEquationSystem)); solver->solveEquationSystem(bsccEquationSystemSolution, bsccEquationSystemRightSide); } @@ -628,7 +628,7 @@ namespace storm { rewardSolution = std::vector(rewardEquationSystemMatrix.getColumnCount(), one); { - std::unique_ptr> solver = linearEquationSolverFactory.create(rewardEquationSystemMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(rewardEquationSystemMatrix)); solver->solveEquationSystem(rewardSolution, rewardRightSide); } } diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 73bd63088..03ceec430 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -71,7 +71,7 @@ namespace storm { storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); solver->solveEquationSystem(x, b); // Return a hybrid check result that stores the numerical values explicitly. @@ -129,7 +129,7 @@ namespace storm { storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); solver->performMatrixVectorMultiplication(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -155,7 +155,7 @@ namespace storm { storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); solver->performMatrixVectorMultiplication(x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -181,7 +181,7 @@ namespace storm { std::vector b = totalRewardVector.toVector(odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); solver->performMatrixVectorMultiplication(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -236,7 +236,7 @@ namespace storm { std::vector b = subvector.toVector(odd); // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); solver->solveEquationSystem(x, b); // Return a hybrid check result that stores the numerical values explicitly. diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index fcbe3c018..0756e5edb 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -75,7 +75,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->solveEquationSystem(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. @@ -140,7 +140,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -165,7 +165,7 @@ namespace storm { std::vector x = rewardModel.getStateRewardVector().toVector(odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); solver->performMatrixVectorMultiplication(dir, x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -194,7 +194,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = transitionMatrix.toMatrixVector(totalRewardVector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. @@ -261,7 +261,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->solveEquationSystem(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 7e9d03c6d..c46a76af5 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -36,7 +36,7 @@ namespace storm { std::vector subresult(maybeStates.getNumberOfSetBits()); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); solver->performMatrixVectorMultiplication(subresult, &b, stepBound); // Set the values of the resulting vector accordingly. @@ -89,7 +89,7 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Now solve the created system of linear equations. - std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); solver->solveEquationSystem(x, b); // Set values of resulting vector according to result. @@ -209,7 +209,7 @@ namespace storm { std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); solver->solveEquationSystem(x, b); // Set values of resulting vector according to result. diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index a9ca1fe2d..ada5e4e2a 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -47,7 +47,7 @@ namespace storm { // Create the vector with which to multiply. std::vector subresult(maybeStates.getNumberOfSetBits()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); solver->performMatrixVectorMultiplication(dir, subresult, &b, stepBound); // Set the values of the resulting vector accordingly. @@ -329,7 +329,7 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::zero()); // Solve the corresponding system of equations. - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); solver->solveEquationSystem(dir, x, b); // Set values of resulting vector according to result. @@ -476,7 +476,7 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice); std::vector sspResult(numberOfStatesNotInMecs + mecDecomposition.size()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(sspMatrix)); solver->solveEquationSystem(dir, sspResult, b); // Prepare result vector.