From 95b95d9c643c80368748538e9caf721f082c35cc Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 27 Jun 2016 23:23:45 +0200 Subject: [PATCH] fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact Former-commit-id: de103e19adfdd3ccbe5d174fcb5a89e3800b0c85 --- .../csl/helper/SparseCtmcCslHelper.cpp | 10 ++-- .../helper/SparseMarkovAutomatonCslHelper.cpp | 8 ++-- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 10 ++-- .../prctl/helper/HybridMdpPrctlHelper.cpp | 10 ++-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 12 ++--- .../prctl/helper/SparseMdpPrctlHelper.cpp | 14 +++--- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 10 ++-- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 10 ++-- src/solver/EigenLinearEquationSolver.cpp | 48 ++----------------- src/solver/EigenLinearEquationSolver.h | 5 +- .../EliminationLinearEquationSolver.cpp | 4 +- src/solver/EliminationLinearEquationSolver.h | 4 +- src/solver/GmmxxLinearEquationSolver.cpp | 4 +- src/solver/GmmxxLinearEquationSolver.h | 4 +- src/solver/LinearEquationSolver.cpp | 4 +- src/solver/LinearEquationSolver.h | 6 +-- src/solver/MinMaxLinearEquationSolver.cpp | 8 ++-- src/solver/MinMaxLinearEquationSolver.h | 12 ++--- src/solver/NativeLinearEquationSolver.cpp | 4 +- src/solver/NativeLinearEquationSolver.h | 4 +- .../StandardMinMaxLinearEquationSolver.cpp | 22 +++++---- .../StandardMinMaxLinearEquationSolver.h | 8 ++-- src/solver/SymbolicLinearEquationSolver.cpp | 4 +- src/solver/SymbolicLinearEquationSolver.h | 4 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 4 +- .../SymbolicMinMaxLinearEquationSolver.h | 4 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 6 +-- .../TopologicalMinMaxLinearEquationSolver.h | 4 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 2 +- .../solver/EigenLinearEquationSolverTest.cpp | 28 +++++------ .../EliminationLinearEquationSolverTest.cpp | 4 +- .../solver/GmmxxLinearEquationSolverTest.cpp | 16 +++---- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 30 ++++++------ .../solver/NativeLinearEquationSolverTest.cpp | 4 +- .../NativeMinMaxLinearEquationSolverTest.cpp | 20 ++++---- 35 files changed, 156 insertions(+), 195 deletions(-) diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 0f6f7535f..4ccf61e64 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -456,7 +456,7 @@ namespace storm { { std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(bsccEquationSystem)); - solver->solveEquationSystem(bsccEquationSystemSolution, bsccEquationSystemRightSide); + solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide); } // If exit rates were given, we need to 'fix' the results to also account for the timing behaviour. @@ -527,7 +527,7 @@ namespace storm { { std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(rewardEquationSystemMatrix)); - solver->solveEquationSystem(rewardSolution, rewardRightSide); + solver->solveEquations(rewardSolution, rewardRightSide); } } @@ -633,13 +633,13 @@ namespace storm { if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) { // Perform the matrix-vector multiplications (without adding). - solver->performMatrixVectorMultiplication(values, addVector, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); + solver->repeatedMultiply(values, addVector, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); } else if (useMixedPoissonProbabilities) { std::function addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; // For the iterations below the left truncation point, we need to add and scale the result with the uniformization rate. for (uint_fast64_t index = 1; index < startingIteration; ++index) { - solver->performMatrixVectorMultiplication(values, nullptr, 1, &multiplicationResult); + solver->repeatedMultiply(values, nullptr, 1, &multiplicationResult); storm::utility::vector::applyPointwise(result, values, result, addAndScale); } } @@ -649,7 +649,7 @@ namespace storm { ValueType weight = 0; std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { - solver->performMatrixVectorMultiplication(values, addVector, 1, &multiplicationResult); + solver->repeatedMultiply(values, addVector, 1, &multiplicationResult); weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; storm::utility::vector::applyPointwise(result, values, result, addAndScale); diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 1d037c5da..e56b21d66 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -102,7 +102,7 @@ namespace storm { storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); // Now perform the inner value iteration for probabilistic states. - solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquations(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); @@ -115,7 +115,7 @@ namespace storm { // After the loop, perform one more step of the value iteration for PS states. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); - solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquations(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); } template @@ -333,7 +333,7 @@ namespace storm { std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); - solver->solveEquationSystem(dir, x, b); + solver->solveEquations(dir, x, b); // Prepare result vector. std::vector result(numberOfStates); @@ -431,7 +431,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(submatrix); - solver->solveEquationSystem(dir, x, b); + solver->solveEquations(dir, x, b); // Set values of resulting vector according to previous result and return the result. storm::utility::vector::setVectorValues(result, maybeStates, x); diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 03ceec430..e9fe53f2e 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -72,7 +72,7 @@ namespace storm { std::vector b = subvector.toVector(odd); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); - solver->solveEquationSystem(x, b); + solver->solveEquations(x, b); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd(), maybeStates, odd, x)); @@ -130,7 +130,7 @@ namespace storm { std::vector b = subvector.toVector(odd); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); - solver->performMatrixVectorMultiplication(x, &b, stepBound); + solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); @@ -156,7 +156,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); - solver->performMatrixVectorMultiplication(x, nullptr, stepBound); + solver->repeatedMultiply(x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); @@ -182,7 +182,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); - solver->performMatrixVectorMultiplication(x, &b, stepBound); + solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); @@ -237,7 +237,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); - solver->solveEquationSystem(x, b); + solver->solveEquations(x, b); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index f65f0506a..4863c1daf 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -76,7 +76,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); - solver->solveEquationSystem(dir, x, explicitRepresentation.second); + solver->solveEquations(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd(), maybeStates, odd, x)); @@ -141,7 +141,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); - solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); + solver->multiply(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); @@ -166,7 +166,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitMatrix)); - solver->performMatrixVectorMultiplication(dir, x, nullptr, stepBound); + solver->multiply(dir, x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); @@ -195,7 +195,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); - solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); + solver->multiply(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); @@ -262,7 +262,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); - solver->solveEquationSystem(dir, x, explicitRepresentation.second); + solver->solveEquations(dir, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 391bd994d..916d24d53 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -37,7 +37,7 @@ namespace storm { // Perform the matrix vector multiplication as often as required by the formula bound. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); - solver->performMatrixVectorMultiplication(subresult, &b, stepBound); + solver->repeatedMultiply(subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -90,7 +90,7 @@ namespace storm { // Now solve the created system of linear equations. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); - solver->solveEquationSystem(x, b); + solver->solveEquations(x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -121,7 +121,7 @@ namespace storm { // Perform one single matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(result); + solver->repeatedMultiply(result); return result; } @@ -135,7 +135,7 @@ namespace storm { // Perform the matrix vector multiplication as often as required by the formula bound. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(result, &totalRewardVector, stepBound); + solver->repeatedMultiply(result, &totalRewardVector, stepBound); return result; } @@ -150,7 +150,7 @@ namespace storm { // Perform the matrix vector multiplication as often as required by the formula bound. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(result, nullptr, stepCount); + solver->repeatedMultiply(result, nullptr, stepCount); return result; } @@ -210,7 +210,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); - solver->solveEquationSystem(x, b); + solver->solveEquations(x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 0b43a524b..8c09b96b8 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -49,7 +49,7 @@ namespace storm { std::vector subresult(maybeStates.getNumberOfSetBits()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); - solver->performMatrixVectorMultiplication(dir, subresult, &b, stepBound); + solver->multiply(dir, subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -67,7 +67,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(dir, result); + solver->multiply(dir, result); return result; } @@ -164,7 +164,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); solver->setTrackScheduler(produceScheduler); - solver->solveEquationSystem(x, b); + solver->solveEquations(x, b); if (produceScheduler) { scheduler = solver->getScheduler(); @@ -211,7 +211,7 @@ namespace storm { std::vector result(rewardModel.getStateRewardVector()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(dir, result, nullptr, stepCount); + solver->multiply(dir, result, nullptr, stepCount); return result; } @@ -235,7 +235,7 @@ namespace storm { } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->performMatrixVectorMultiplication(dir, result, &totalRewardVector, stepBound); + solver->multiply(dir, result, &totalRewardVector, stepBound); return result; } @@ -335,7 +335,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); - solver->solveEquationSystem(dir, x, b); + solver->solveEquations(dir, x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -482,7 +482,7 @@ namespace storm { std::vector sspResult(numberOfStatesNotInMecs + mecDecomposition.size()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(sspMatrix)); - solver->solveEquationSystem(dir, sspResult, b); + solver->solveEquations(dir, sspResult, b); // Prepare result vector. std::vector result(numberOfStates, zero); diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 06581d841..b5adb7e15 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -58,7 +58,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); return statesWithProbability01.second.template toAdd() + result; } else { @@ -106,7 +106,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(model.getManager().template getAddZero(), &subvector, stepBound); + storm::dd::Add result = solver->multiply(model.getManager().template getAddZero(), &subvector, stepBound); return psiStates.template toAdd() + result; } else { @@ -124,7 +124,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - return solver->performMatrixVectorMultiplication(model.getManager().template getAddZero(), &totalRewardVector, stepBound); + return solver->multiply(model.getManager().template getAddZero(), &totalRewardVector, stepBound); } template @@ -134,7 +134,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - return solver->performMatrixVectorMultiplication(rewardModel.getStateRewardVector(), nullptr, stepBound); + return solver->multiply(rewardModel.getStateRewardVector(), nullptr, stepBound); } template @@ -175,7 +175,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); } else { diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 329591bf1..d3cec71e4 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -66,7 +66,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + result)); } else { @@ -118,7 +118,7 @@ namespace storm { submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &subvector, stepBound); + storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &subvector, stepBound); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd() + result)); } else { @@ -133,7 +133,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); + storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } @@ -148,7 +148,7 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); + storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } @@ -202,7 +202,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result))); } else { diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp index a910801f3..c00fe97b0 100644 --- a/src/solver/EigenLinearEquationSolver.cpp +++ b/src/solver/EigenLinearEquationSolver.cpp @@ -114,7 +114,7 @@ namespace storm { } template - void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); @@ -197,7 +197,7 @@ namespace storm { } template - void EigenLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b) const { + void EigenLinearEquationSolver::multiply(std::vector& x, std::vector& result, std::vector const* b) const { // Typedef the map-type so we don't have to spell it out. typedef decltype(Eigen::Matrix::Map(b->data(), b->size())) MapType; @@ -224,46 +224,6 @@ namespace storm { } } -// template -// void EigenLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { -// // Typedef the map-type so we don't have to spell it out. -// typedef decltype(Eigen::Matrix::Map(b->data(), b->size())) MapType; -// -// bool multiplyResultProvided = multiplyResult != nullptr; -// if (!multiplyResult) { -// multiplyResult = new std::vector(eigenA->cols()); -// } -// auto eigenMultiplyResult = Eigen::Matrix::Map(multiplyResult->data(), multiplyResult->size()); -// -// // Map the input vectors x and b to Eigen's format. -// std::unique_ptr eigenB; -// if (b != nullptr) { -// eigenB = std::make_unique(Eigen::Matrix::Map(b->data(), b->size())); -// } -// auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); -// -// // Perform n matrix-vector multiplications. -// auto currentX = &eigenX; -// auto nextX = &eigenMultiplyResult; -// for (uint64_t iteration = 0; iteration < n; ++iteration) { -// if (eigenB) { -// nextX->noalias() = *eigenA * *currentX + *eigenB; -// } else { -// nextX->noalias() = *eigenA * *currentX; -// } -// std::swap(nextX, currentX); -// } -// -// // If the last result we obtained is not the one in the input vector x, we swap the result there. -// if (currentX != &eigenX) { -// std::swap(*nextX, *currentX); -// } -// -// if (!multiplyResultProvided) { -// delete multiplyResult; -// } -// } - template EigenLinearEquationSolverSettings& EigenLinearEquationSolver::getSettings() { return settings; @@ -277,7 +237,7 @@ namespace storm { // Specialization form storm::RationalNumber template<> - void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); @@ -290,7 +250,7 @@ namespace storm { // Specialization form storm::RationalFunction template<> - void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); diff --git a/src/solver/EigenLinearEquationSolver.h b/src/solver/EigenLinearEquationSolver.h index 2f3f4ca23..43e34427e 100644 --- a/src/solver/EigenLinearEquationSolver.h +++ b/src/solver/EigenLinearEquationSolver.h @@ -61,9 +61,8 @@ namespace storm { EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; -// virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; + virtual void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + virtual void multiply(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; EigenLinearEquationSolverSettings& getSettings(); EigenLinearEquationSolverSettings const& getSettings() const; diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index a56e1e584..75340d6ba 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -44,7 +44,7 @@ namespace storm { } template - void EliminationLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void EliminationLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { STORM_LOG_WARN_COND(multiplyResult == nullptr, "Providing scratch memory will not improve the performance of this solver."); // FIXME: This solver will not work for all input systems. More concretely, the current implementation will @@ -101,7 +101,7 @@ namespace storm { } template - void EliminationLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b) const { + void EliminationLinearEquationSolver::multiply(std::vector& x, std::vector& result, std::vector const* b) const { if (&x != &result) { A.multiplyWithVector(x, result); if (b != nullptr) { diff --git a/src/solver/EliminationLinearEquationSolver.h b/src/solver/EliminationLinearEquationSolver.h index 580a77438..15a1e5c25 100644 --- a/src/solver/EliminationLinearEquationSolver.h +++ b/src/solver/EliminationLinearEquationSolver.h @@ -29,8 +29,8 @@ namespace storm { EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); EliminationLinearEquationSolver(storm::storage::SparseMatrix&& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; + virtual void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + virtual void multiply(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; EliminationLinearEquationSolverSettings& getSettings(); EliminationLinearEquationSolverSettings const& getSettings() const; diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 53e643741..d29cda389 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -121,7 +121,7 @@ namespace storm { } template - void GmmxxLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void GmmxxLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { auto method = this->getSettings().getSolutionMethod(); auto preconditioner = this->getSettings().getPreconditioner(); STORM_LOG_INFO("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations)."); @@ -178,7 +178,7 @@ namespace storm { } template - void GmmxxLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b) const { + void GmmxxLinearEquationSolver::multiply(std::vector& x, std::vector& result, std::vector const* b) const { if (b) { gmm::mult_add(*gmmxxMatrix, x, *b, result); } else { diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index da57e8325..4425ec940 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -89,8 +89,8 @@ namespace storm { GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); GmmxxLinearEquationSolver(storm::storage::SparseMatrix&& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; + virtual void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + virtual void multiply(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; GmmxxLinearEquationSolverSettings& getSettings(); GmmxxLinearEquationSolverSettings const& getSettings() const; diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp index b7f15d90d..84f5f84e5 100644 --- a/src/solver/LinearEquationSolver.cpp +++ b/src/solver/LinearEquationSolver.cpp @@ -14,7 +14,7 @@ namespace storm { namespace solver { template - void LinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { + void LinearEquationSolver::repeatedMultiply(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. @@ -30,7 +30,7 @@ namespace storm { // Now perform matrix-vector multiplication as long as we meet the bound. for (uint_fast64_t i = 0; i < n; ++i) { - this->performMatrixVectorMultiplication(*currentX, *nextX, b); + this->multiply(*currentX, *nextX, b); std::swap(nextX, currentX); } diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index e12fa6eb5..9632ddb2b 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -32,7 +32,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; + virtual void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; /*! * Performs on matrix-vector multiplication x' = A*x + b. @@ -44,7 +44,7 @@ namespace storm { * @param b If non-null, this vector is added after the multiplication. If given, its length must be equal * to the number of rows of A. */ - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b = nullptr) const = 0; + virtual void multiply(std::vector& x, std::vector& result, std::vector const* b = nullptr) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -58,7 +58,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const; + void repeatedMultiply(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const; }; template diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index f068b75aa..bd522834f 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -28,15 +28,15 @@ namespace storm { } template - void MinMaxLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void MinMaxLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set."); - solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX); + solveEquations(convert(this->direction), x, b, multiplyResult, newX); } template - void MinMaxLinearEquationSolver::performMatrixVectorMultiplication( std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void MinMaxLinearEquationSolver::multiply( std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set."); - return performMatrixVectorMultiplication(convert(this->direction), x, b, n, multiplyResult); + return multiply(convert(this->direction), x, b, n, multiplyResult); } template diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 5371f9916..358ef0be1 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -46,14 +46,14 @@ namespace storm { * vector must be equal to the length of the vector x (and thus to the number of columns of A). * @return The solution vector x of the system of linear equations as the content of the parameter x. */ - virtual void solveEquationSystem(OptimizationDirection d, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; + virtual void solveEquations(OptimizationDirection d, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; /*! - * Behaves the same as the other variant of solveEquationSystem, with the distinction that + * Behaves the same as the other variant of solveEquations, with the distinction that * instead of providing the optimization direction as an argument, the internally set optimization direction * is used. Note: this method can only be called after setting the optimization direction. */ - void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const; + void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const; /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes @@ -72,14 +72,14 @@ namespace storm { * vector must be equal to the number of rows of A. * @return The result of the repeated matrix-vector multiplication as the content of the vector x. */ - virtual void performMatrixVectorMultiplication(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + virtual void multiply(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; /*! - * Behaves the same as the other variant of performMatrixVectorMultiplication, with the + * Behaves the same as the other variant of multiply, with the * distinction that instead of providing the optimization direction as an argument, the internally set * optimization direction is used. Note: this method can only be called after setting the optimization direction. */ - virtual void performMatrixVectorMultiplication( std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const; + virtual void multiply( std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const; /*! * Sets an optimization direction to use for calls to methods that do not explicitly provide one. diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index ef4e1c2ff..b24c9dde4 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -94,7 +94,7 @@ namespace storm { } template - void NativeLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + void NativeLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::GaussSeidel) { // Define the omega used for SOR. ValueType omega = this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR ? this->getSettings().getOmega() : storm::utility::one(); @@ -183,7 +183,7 @@ namespace storm { } template - void NativeLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b) const { + void NativeLinearEquationSolver::multiply(std::vector& x, std::vector& result, std::vector const* b) const { if (&x != &result) { A.multiplyWithVector(x, result); if (b != nullptr) { diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index 6d6125741..235985df6 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -46,8 +46,8 @@ namespace storm { NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); NativeLinearEquationSolver(storm::storage::SparseMatrix&& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; + virtual void solveEquations(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + virtual void multiply(std::vector& x, std::vector& result, std::vector const* b = nullptr) const override; NativeLinearEquationSolverSettings& getSettings(); NativeLinearEquationSolverSettings const& getSettings() const; diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index f485e0de2..db507ef68 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -84,15 +84,15 @@ namespace storm { } template - void StandardMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void StandardMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { switch (this->getSettings().getSolutionMethod()) { - case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: solveEquationSystemValueIteration(dir, x, b, multiplyResult, newX); break; - case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: solveEquationSystemPolicyIteration(dir, x, b, multiplyResult, newX); break; + case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: solveEquationsValueIteration(dir, x, b, multiplyResult, newX); break; + case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: solveEquationsPolicyIteration(dir, x, b, multiplyResult, newX); break; } } template - void StandardMinMaxLinearEquationSolver::solveEquationSystemPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void StandardMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { // Create scratch memory if none was provided. bool multiplyResultMemoryProvided = multiplyResult != nullptr; @@ -121,8 +121,8 @@ namespace storm { // FIXME: we need to remove the 0- and 1- states to make the solution unique. // HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying // within illegal MECs will never strictly improve the value. Is this true? - auto solver = linearEquationSolverFactory->create(submatrix); - solver->solveEquationSystem(x, subB, &deterministicMultiplyResult); + auto solver = linearEquationSolverFactory->create(std::move(submatrix)); + solver->solveEquations(x, subB, &deterministicMultiplyResult); // Go through the multiplication result and see whether we can improve any of the choices. bool schedulerImproved = false; @@ -186,7 +186,7 @@ namespace storm { } template - void StandardMinMaxLinearEquationSolver::solveEquationSystemValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { std::unique_ptr> solver = linearEquationSolverFactory->create(A); // Create scratch memory if none was provided. @@ -209,7 +209,7 @@ namespace storm { Status status = Status::InProgress; while (status == Status::InProgress) { // Compute x' = A*x + b. - solver->performMatrixVectorMultiplication(*currentX, *multiplyResult, &b); + solver->multiply(*currentX, *multiplyResult, &b); // Reduce the vector x' by applying min/max for all non-deterministic choices. storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices()); @@ -243,7 +243,7 @@ namespace storm { } template - void StandardMinMaxLinearEquationSolver::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void StandardMinMaxLinearEquationSolver::multiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { std::unique_ptr> solver = linearEquationSolverFactory->create(A); // If scratch memory was not provided, we create it. @@ -253,7 +253,7 @@ namespace storm { } for (uint64_t i = 0; i < n; ++i) { - solver->performMatrixVectorMultiplication(x, *multiplyResult, b); + solver->multiply(x, *multiplyResult, b); // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. @@ -381,6 +381,7 @@ namespace storm { // Intentionally left empty. } + template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class GmmxxMinMaxLinearEquationSolverFactory; @@ -388,6 +389,7 @@ namespace storm { template class NativeMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; + template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; diff --git a/src/solver/StandardMinMaxLinearEquationSolver.h b/src/solver/StandardMinMaxLinearEquationSolver.h index 0bf4349be..36b2aa458 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/solver/StandardMinMaxLinearEquationSolver.h @@ -38,15 +38,15 @@ namespace storm { StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings()); StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings()); - virtual void solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; - virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual void solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void multiply(OptimizationDirection dir, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; StandardMinMaxLinearEquationSolverSettings const& getSettings() const; StandardMinMaxLinearEquationSolverSettings& getSettings(); private: - void solveEquationSystemPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const; - void solveEquationSystemValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const; + void solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const; + void solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index 3e8dd0c55..338d7400e 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -26,7 +26,7 @@ namespace storm { } template - storm::dd::Add SymbolicLinearEquationSolver::solveEquationSystem(storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add SymbolicLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { // Start by computing the Jacobi decomposition of the matrix A. storm::dd::Bdd diagonal = x.getDdManager().getBddOne(); for (auto const& pair : rowColumnMetaVariablePairs) { @@ -68,7 +68,7 @@ namespace storm { } template - storm::dd::Add SymbolicLinearEquationSolver::performMatrixVectorMultiplication(storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { + storm::dd::Add SymbolicLinearEquationSolver::multiply(storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { storm::dd::Add xCopy = x; // Perform matrix-vector multiplication while the bound is met. diff --git a/src/solver/SymbolicLinearEquationSolver.h b/src/solver/SymbolicLinearEquationSolver.h index 9a8f983df..97a07b64d 100644 --- a/src/solver/SymbolicLinearEquationSolver.h +++ b/src/solver/SymbolicLinearEquationSolver.h @@ -66,7 +66,7 @@ namespace storm { * @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A. * @return The solution of the equation system. */ - virtual storm::dd::Add solveEquationSystem(storm::dd::Add const& x, storm::dd::Add const& b) const; + virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -79,7 +79,7 @@ namespace storm { * to the number of rows of A. * @return The solution of the equation system. */ - virtual storm::dd::Add performMatrixVectorMultiplication(storm::dd::Add const& x, storm::dd::Add const* b = nullptr, uint_fast64_t n = 1) const; + virtual storm::dd::Add multiply(storm::dd::Add const& x, storm::dd::Add const* b = nullptr, uint_fast64_t n = 1) const; protected: // The matrix defining the coefficients of the linear equation system. diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index 7cce11554..ed14fff57 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -30,7 +30,7 @@ namespace storm { } template - storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquations(bool minimize, storm::dd::Add const& x, storm::dd::Add const& b) const { // Set up the environment. storm::dd::Add xCopy = x; uint_fast64_t iterations = 0; @@ -66,7 +66,7 @@ namespace storm { } template - storm::dd::Add SymbolicMinMaxLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { + storm::dd::Add SymbolicMinMaxLinearEquationSolver::multiply(bool minimize, storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { storm::dd::Add xCopy = x; // Perform matrix-vector multiplication while the bound is met. diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.h b/src/solver/SymbolicMinMaxLinearEquationSolver.h index d78a60867..98cb94102 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.h @@ -72,7 +72,7 @@ namespace storm { * of A. * @return The solution of the equation system. */ - virtual storm::dd::Add solveEquationSystem(bool minimize, storm::dd::Add const& x, storm::dd::Add const& b) const; + virtual storm::dd::Add solveEquations(bool minimize, storm::dd::Add const& x, storm::dd::Add const& b) const; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -87,7 +87,7 @@ namespace storm { * to the number of row groups of A. * @return The solution of the equation system. */ - virtual storm::dd::Add performMatrixVectorMultiplication(bool minimize, storm::dd::Add const& x, storm::dd::Add const* b = nullptr, uint_fast64_t n = 1) const; + virtual storm::dd::Add multiply(bool minimize, storm::dd::Add const& x, storm::dd::Add const* b = nullptr, uint_fast64_t n = 1) const; protected: // The matrix defining the coefficients of the linear equation system. diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index dd0404ab7..6ef7d231e 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -33,7 +33,7 @@ namespace storm { } template - void TopologicalMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { + void TopologicalMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { #ifdef GPU_USE_FLOAT #define __FORCE_FLOAT_CALCULATION true @@ -49,7 +49,7 @@ namespace storm { std::vector new_x = storm::utility::vector::toValueType(x); std::vector const new_b = storm::utility::vector::toValueType(b); - newSolver.solveEquationSystem(dir, new_x, new_b, nullptr, nullptr); + newSolver.solveEquations(dir, new_x, new_b, nullptr, nullptr); for (size_t i = 0, size = new_x.size(); i < size; ++i) { x.at(i) = new_x.at(i); @@ -422,7 +422,7 @@ namespace storm { } template - void TopologicalMinMaxLinearEquationSolver::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void TopologicalMinMaxLinearEquationSolver::multiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h index 7f8dbfe78..e6cc87997 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -32,9 +32,9 @@ namespace storm { */ TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true); - virtual void solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; - virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const override; + virtual void multiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const override; private: storm::storage::SparseMatrix const& A; diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index b97e938bd..f647c722f 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -210,7 +210,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { EXPECT_EQ(7ul, mdp->getNumberOfChoices()); auto solverFactory = std::make_unique>(); - solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); diff --git a/test/functional/solver/EigenLinearEquationSolverTest.cpp b/test/functional/solver/EigenLinearEquationSolverTest.cpp index 0139e627a..33d073c62 100644 --- a/test/functional/solver/EigenLinearEquationSolverTest.cpp +++ b/test/functional/solver/EigenLinearEquationSolverTest.cpp @@ -29,7 +29,7 @@ TEST(EigenLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A)); storm::solver::EigenLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -58,7 +58,7 @@ TEST(EigenLinearEquationSolver, SparseLU) { solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::SparseLU); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -84,7 +84,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) { std::vector b = {16, -4, -7}; storm::solver::EigenLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_TRUE(storm::utility::isOne(x[0])); ASSERT_TRUE(x[1] == 3); ASSERT_TRUE(x[2] == -1); @@ -110,7 +110,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) { std::vector b = {storm::RationalFunction(16), storm::RationalFunction(-4), storm::RationalFunction(-7)}; storm::solver::EigenLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_TRUE(storm::utility::isOne(x[0])); ASSERT_TRUE(x[1] == storm::RationalFunction(3)); ASSERT_TRUE(x[2] == storm::RationalFunction(-1)); @@ -142,7 +142,7 @@ TEST(EigenLinearEquationSolver, DGMRES) { solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); solver.getSettings().setNumberOfIterationsUntilRestart(50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -172,7 +172,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Ilu); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -202,7 +202,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Diagonal); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -234,7 +234,7 @@ TEST(EigenLinearEquationSolver, GMRES) { solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); solver.getSettings().setNumberOfIterationsUntilRestart(50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -264,7 +264,7 @@ TEST(EigenLinearEquationSolver, GMRES_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Ilu); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -294,7 +294,7 @@ TEST(EigenLinearEquationSolver, GMRES_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Diagonal); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -325,7 +325,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB) { solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -355,7 +355,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Ilu); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -385,7 +385,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Diagonal); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -410,6 +410,6 @@ TEST(EigenLinearEquationSolver, MatrixVectorMultiplication) { x[4] = 1; storm::solver::EigenLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(x, nullptr, 4)); + ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/EliminationLinearEquationSolverTest.cpp b/test/functional/solver/EliminationLinearEquationSolverTest.cpp index 7a964a1d6..65c5d4e13 100644 --- a/test/functional/solver/EliminationLinearEquationSolverTest.cpp +++ b/test/functional/solver/EliminationLinearEquationSolverTest.cpp @@ -28,7 +28,7 @@ TEST(EliminationLinearEquationSolver, Solve) { ASSERT_NO_THROW(storm::solver::EliminationLinearEquationSolver solver(A)); storm::solver::EliminationLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), 1e-15); ASSERT_LT(std::abs(x[1] - 3), 1e-15); ASSERT_LT(std::abs(x[2] - (-1)), 1e-15); @@ -53,6 +53,6 @@ TEST(EliminationLinearEquationSolver, MatrixVectorMultiplication) { x[4] = 1; storm::solver::EliminationLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(x, nullptr, 4)); + ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp index 44282f522..4cf07d6ec 100644 --- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp @@ -28,7 +28,7 @@ TEST(GmmxxLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A)); storm::solver::GmmxxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -60,7 +60,7 @@ TEST(GmmxxLinearEquationSolver, gmres) { solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); solver.getSettings().setNumberOfIterationsUntilRestart(50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -97,7 +97,7 @@ TEST(GmmxxLinearEquationSolver, qmr) { solver2.getSettings().setMaximalNumberOfIterations(10000); solver2.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); - ASSERT_NO_THROW(solver2.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver2.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -128,7 +128,7 @@ TEST(GmmxxLinearEquationSolver, bicgstab) { solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -158,7 +158,7 @@ TEST(GmmxxLinearEquationSolver, jacobi) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -189,7 +189,7 @@ TEST(GmmxxLinearEquationSolver, gmresilu) { solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::Ilu); solver.getSettings().setNumberOfIterationsUntilRestart(50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -221,7 +221,7 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) { solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal); solver.getSettings().setNumberOfIterationsUntilRestart(50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -246,6 +246,6 @@ TEST(GmmxxLinearEquationSolver, MatrixVectorMultiplication) { x[4] = 1; storm::solver::GmmxxLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(x, nullptr, 4)); + ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 724dfba7f..4f86c25b1 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -19,10 +19,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::getModule().getPrecision()); } @@ -43,17 +43,17 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); - solver->setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); + solver->setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::getModule().getPrecision()); bound = 0.6; - solver->setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); + solver->setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true)); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::getModule().getPrecision()); } @@ -78,23 +78,23 @@ TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 1)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 2)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 2)); ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 20)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 1)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Maximize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 20)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Maximize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::getModule().getPrecision()); } @@ -110,12 +110,12 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); - factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/NativeLinearEquationSolverTest.cpp b/test/functional/solver/NativeLinearEquationSolverTest.cpp index cfe61741c..c3c114cbc 100644 --- a/test/functional/solver/NativeLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeLinearEquationSolverTest.cpp @@ -28,7 +28,7 @@ TEST(NativeLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::solver::NativeLinearEquationSolver solver(A)); storm::solver::NativeLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -53,6 +53,6 @@ TEST(NativeLinearEquationSolver, MatrixVectorMultiplication) { x[4] = 1; storm::solver::NativeLinearEquationSolver solver(A); - ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(x, nullptr, 4)); + ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); } \ No newline at end of file diff --git a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index 93482227d..fdf595193 100644 --- a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -21,10 +21,10 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::getModule().getPrecision()); } @@ -49,23 +49,23 @@ TEST(NativeMinMaxLinearEquationSolver, MatrixVectorMultiplication) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 1)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 2)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 2)); ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Minimize, x, nullptr, 20)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Minimize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 1)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Maximize, x, nullptr, 1)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); x = {0, 1, 0}; - ASSERT_NO_THROW(solver->performMatrixVectorMultiplication(storm::OptimizationDirection::Maximize, x, nullptr, 20)); + ASSERT_NO_THROW(solver->multiply(storm::OptimizationDirection::Maximize, x, nullptr, 20)); ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::getModule().getPrecision()); } @@ -81,12 +81,12 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(); - factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); auto solver = factory.create(A); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); - ASSERT_NO_THROW(solver->solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule().getPrecision()); } \ No newline at end of file