Browse Source

fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact

Former-commit-id: de103e19ad
tempestpy_adaptions
dehnert 8 years ago
parent
commit
95b95d9c64
  1. 10
      src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 8
      src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  3. 10
      src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  4. 10
      src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  5. 12
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  6. 14
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  7. 10
      src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
  8. 10
      src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  9. 48
      src/solver/EigenLinearEquationSolver.cpp
  10. 5
      src/solver/EigenLinearEquationSolver.h
  11. 4
      src/solver/EliminationLinearEquationSolver.cpp
  12. 4
      src/solver/EliminationLinearEquationSolver.h
  13. 4
      src/solver/GmmxxLinearEquationSolver.cpp
  14. 4
      src/solver/GmmxxLinearEquationSolver.h
  15. 4
      src/solver/LinearEquationSolver.cpp
  16. 6
      src/solver/LinearEquationSolver.h
  17. 8
      src/solver/MinMaxLinearEquationSolver.cpp
  18. 12
      src/solver/MinMaxLinearEquationSolver.h
  19. 4
      src/solver/NativeLinearEquationSolver.cpp
  20. 4
      src/solver/NativeLinearEquationSolver.h
  21. 22
      src/solver/StandardMinMaxLinearEquationSolver.cpp
  22. 8
      src/solver/StandardMinMaxLinearEquationSolver.h
  23. 4
      src/solver/SymbolicLinearEquationSolver.cpp
  24. 4
      src/solver/SymbolicLinearEquationSolver.h
  25. 4
      src/solver/SymbolicMinMaxLinearEquationSolver.cpp
  26. 4
      src/solver/SymbolicMinMaxLinearEquationSolver.h
  27. 6
      src/solver/TopologicalMinMaxLinearEquationSolver.cpp
  28. 4
      src/solver/TopologicalMinMaxLinearEquationSolver.h
  29. 2
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  30. 28
      test/functional/solver/EigenLinearEquationSolverTest.cpp
  31. 4
      test/functional/solver/EliminationLinearEquationSolverTest.cpp
  32. 16
      test/functional/solver/GmmxxLinearEquationSolverTest.cpp
  33. 30
      test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
  34. 4
      test/functional/solver/NativeLinearEquationSolverTest.cpp
  35. 20
      test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp

10
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -456,7 +456,7 @@ namespace storm {
{
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<storm::solver::LinearEquationSolver<ValueType>> 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<ValueType(ValueType const&, ValueType const&)> 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<ValueType(ValueType const&, ValueType const&)> 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);

8
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<typename ValueType>
@ -333,7 +333,7 @@ namespace storm {
std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
solver->solveEquationSystem(dir, x, b);
solver->solveEquations(dir, x, b);
// Prepare result vector.
std::vector<ValueType> result(numberOfStates);
@ -431,7 +431,7 @@ namespace storm {
// Solve the corresponding system of equations.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);

10
src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@ -72,7 +72,7 @@ namespace storm {
std::vector<ValueType> b = subvector.toVector(odd);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd<ValueType>(), maybeStates, odd, x));
@ -130,7 +130,7 @@ namespace storm {
std::vector<ValueType> b = subvector.toVector(odd);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
@ -156,7 +156,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
@ -182,7 +182,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
@ -237,7 +237,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));

10
src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@ -76,7 +76,7 @@ namespace storm {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd<ValueType>(), maybeStates, odd, x));
@ -141,7 +141,7 @@ namespace storm {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
@ -166,7 +166,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
@ -195,7 +195,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
@ -262,7 +262,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));

12
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<storm::solver::LinearEquationSolver<ValueType>> 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<storm::solver::LinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);
@ -121,7 +121,7 @@ namespace storm {
// Perform one single matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<storm::solver::LinearEquationSolver<ValueType>> 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<storm::solver::LinearEquationSolver<ValueType>> 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<storm::solver::LinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);

14
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -49,7 +49,7 @@ namespace storm {
std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType>());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType> result(rewardModel.getStateRewardVector());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType>(result, maybeStates, x);
@ -482,7 +482,7 @@ namespace storm {
std::vector<ValueType> sspResult(numberOfStatesNotInMecs + mecDecomposition.size());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(std::move(sspMatrix));
solver->solveEquationSystem(dir, sspResult, b);
solver->solveEquations(dir, sspResult, b);
// Prepare result vector.
std::vector<ValueType> result(numberOfStates, zero);

10
src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@ -58,7 +58,7 @@ namespace storm {
// Solve the equation system.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
return statesWithProbability01.second.template toAdd<ValueType>() + result;
} else {
@ -106,7 +106,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->performMatrixVectorMultiplication(model.getManager().template getAddZero<ValueType>(), &subvector, stepBound);
storm::dd::Add<DdType, ValueType> result = solver->multiply(model.getManager().template getAddZero<ValueType>(), &subvector, stepBound);
return psiStates.template toAdd<ValueType>() + result;
} else {
@ -124,7 +124,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
return solver->performMatrixVectorMultiplication(model.getManager().template getAddZero<ValueType>(), &totalRewardVector, stepBound);
return solver->multiply(model.getManager().template getAddZero<ValueType>(), &totalRewardVector, stepBound);
}
template<storm::dd::DdType DdType, typename ValueType>
@ -134,7 +134,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> 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<storm::dd::DdType DdType, typename ValueType>
@ -175,7 +175,7 @@ namespace storm {
// Solve the equation system.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result);
} else {

10
src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@ -66,7 +66,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), subvector);
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + result));
} else {
@ -118,7 +118,7 @@ namespace storm {
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), &subvector, stepBound);
storm::dd::Add<DdType, ValueType> result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), &subvector, stepBound);
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.template toAdd<ValueType>() + result));
} else {
@ -133,7 +133,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound);
storm::dd::Add<DdType, ValueType> result = solver->multiply(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound);
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result));
}
@ -148,7 +148,7 @@ namespace storm {
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), &totalRewardVector, stepBound);
storm::dd::Add<DdType, ValueType> result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), &totalRewardVector, stepBound);
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result));
}
@ -202,7 +202,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero<ValueType>(), subvector);
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result)));
} else {

48
src/solver/EigenLinearEquationSolver.cpp

@ -114,7 +114,7 @@ namespace storm {
}
template<typename ValueType>
void EigenLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
void EigenLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b.data(), b.size());
@ -197,7 +197,7 @@ namespace storm {
}
template<typename ValueType>
void EigenLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
void EigenLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
// Typedef the map-type so we don't have to spell it out.
typedef decltype(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
@ -224,46 +224,6 @@ namespace storm {
}
}
// template<typename ValueType>
// void EigenLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// // Typedef the map-type so we don't have to spell it out.
// typedef decltype(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size())) MapType;
//
// bool multiplyResultProvided = multiplyResult != nullptr;
// if (!multiplyResult) {
// multiplyResult = new std::vector<ValueType>(eigenA->cols());
// }
// auto eigenMultiplyResult = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(multiplyResult->data(), multiplyResult->size());
//
// // Map the input vectors x and b to Eigen's format.
// std::unique_ptr<MapType> eigenB;
// if (b != nullptr) {
// eigenB = std::make_unique<MapType>(Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b->data(), b->size()));
// }
// auto eigenX = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::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<typename ValueType>
EigenLinearEquationSolverSettings<ValueType>& EigenLinearEquationSolver<ValueType>::getSettings() {
return settings;
@ -277,7 +237,7 @@ namespace storm {
// Specialization form storm::RationalNumber
template<>
void EigenLinearEquationSolver<storm::RationalNumber>::solveEquationSystem(std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> const& b, std::vector<storm::RationalNumber>* multiplyResult) const {
void EigenLinearEquationSolver<storm::RationalNumber>::solveEquations(std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> const& b, std::vector<storm::RationalNumber>* multiplyResult) const {
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(b.data(), b.size());
@ -290,7 +250,7 @@ namespace storm {
// Specialization form storm::RationalFunction
template<>
void EigenLinearEquationSolver<storm::RationalFunction>::solveEquationSystem(std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> const& b, std::vector<storm::RationalFunction>* multiplyResult) const {
void EigenLinearEquationSolver<storm::RationalFunction>::solveEquations(std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> const& b, std::vector<storm::RationalFunction>* multiplyResult) const {
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(b.data(), b.size());

5
src/solver/EigenLinearEquationSolver.h

@ -61,9 +61,8 @@ namespace storm {
EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
// virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
EigenLinearEquationSolverSettings<ValueType>& getSettings();
EigenLinearEquationSolverSettings<ValueType> const& getSettings() const;

4
src/solver/EliminationLinearEquationSolver.cpp

@ -44,7 +44,7 @@ namespace storm {
}
template<typename ValueType>
void EliminationLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
void EliminationLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* 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<typename ValueType>
void EliminationLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
void EliminationLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
if (&x != &result) {
A.multiplyWithVector(x, result);
if (b != nullptr) {

4
src/solver/EliminationLinearEquationSolver.h

@ -29,8 +29,8 @@ namespace storm {
EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
EliminationLinearEquationSolverSettings<ValueType>& getSettings();
EliminationLinearEquationSolverSettings<ValueType> const& getSettings() const;

4
src/solver/GmmxxLinearEquationSolver.cpp

@ -121,7 +121,7 @@ namespace storm {
}
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
void GmmxxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* 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<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
void GmmxxLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
if (b) {
gmm::mult_add(*gmmxxMatrix, x, *b, result);
} else {

4
src/solver/GmmxxLinearEquationSolver.h

@ -89,8 +89,8 @@ namespace storm {
GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
GmmxxLinearEquationSolverSettings<ValueType>& getSettings();
GmmxxLinearEquationSolverSettings<ValueType> const& getSettings() const;

4
src/solver/LinearEquationSolver.cpp

@ -14,7 +14,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
void LinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void LinearEquationSolver<ValueType>::repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* 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);
}

6
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<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* 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<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const = 0;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> 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<ValueType>& x, std::vector<ValueType> const* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
void repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
};
template<typename ValueType>

8
src/solver/MinMaxLinearEquationSolver.cpp

@ -28,15 +28,15 @@ namespace storm {
}
template<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void MinMaxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* 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<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication( std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void MinMaxLinearEquationSolver<ValueType>::multiply( std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* 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<typename ValueType>

12
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<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const = 0;
virtual void solveEquations(OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const = 0;
/*!
* Behaves the same as the other variant of <code>solveEquationSystem</code>, with the distinction that
* Behaves the same as the other variant of <code>solveEquations</code>, 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<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const;
void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* 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<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
virtual void multiply(OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
/*!
* Behaves the same as the other variant of <code>performMatrixVectorMultiplication</code>, with the
* Behaves the same as the other variant of <code>multiply</code>, 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<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
virtual void multiply( std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const;
/*!
* Sets an optimization direction to use for calls to methods that do not explicitly provide one.

4
src/solver/NativeLinearEquationSolver.cpp

@ -94,7 +94,7 @@ namespace storm {
}
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
void NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::GaussSeidel) {
// Define the omega used for SOR.
ValueType omega = this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SOR ? this->getSettings().getOmega() : storm::utility::one<ValueType>();
@ -183,7 +183,7 @@ namespace storm {
}
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
void NativeLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b) const {
if (&x != &result) {
A.multiplyWithVector(x, result);
if (b != nullptr) {

4
src/solver/NativeLinearEquationSolver.h

@ -46,8 +46,8 @@ namespace storm {
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType>& result, std::vector<ValueType> const* b = nullptr) const override;
NativeLinearEquationSolverSettings<ValueType>& getSettings();
NativeLinearEquationSolverSettings<ValueType> const& getSettings() const;

22
src/solver/StandardMinMaxLinearEquationSolver.cpp

@ -84,15 +84,15 @@ namespace storm {
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
switch (this->getSettings().getSolutionMethod()) {
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: solveEquationSystemValueIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: solveEquationSystemPolicyIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: solveEquationsValueIteration(dir, x, b, multiplyResult, newX); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: solveEquationsPolicyIteration(dir, x, b, multiplyResult, newX); break;
}
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationSystemPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* 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<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationSystemValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void StandardMinMaxLinearEquationSolver<ValueType>::multiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<double>;
template class StandardMinMaxLinearEquationSolver<double>;
template class StandardMinMaxLinearEquationSolverFactory<double>;
template class GmmxxMinMaxLinearEquationSolverFactory<double>;
@ -388,6 +389,7 @@ namespace storm {
template class NativeMinMaxLinearEquationSolverFactory<double>;
template class EliminationMinMaxLinearEquationSolverFactory<double>;
template class StandardMinMaxLinearEquationSolverSettings<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolver<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EigenMinMaxLinearEquationSolverFactory<storm::RationalNumber>;

8
src/solver/StandardMinMaxLinearEquationSolver.h

@ -38,15 +38,15 @@ namespace storm {
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
virtual void solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void multiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
StandardMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
StandardMinMaxLinearEquationSolverSettings<ValueType>& getSettings();
private:
void solveEquationSystemPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const;
void solveEquationSystemValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const;
void solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const;
void solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const;
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;

4
src/solver/SymbolicLinearEquationSolver.cpp

@ -26,7 +26,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::solveEquationSystem(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
// Start by computing the Jacobi decomposition of the matrix A.
storm::dd::Bdd<DdType> diagonal = x.getDdManager().getBddOne();
for (auto const& pair : rowColumnMetaVariablePairs) {
@ -68,7 +68,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::performMatrixVectorMultiplication(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b, uint_fast64_t n) const {
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::multiply(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b, uint_fast64_t n) const {
storm::dd::Add<DdType, ValueType> xCopy = x;
// Perform matrix-vector multiplication while the bound is met.

4
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<DdType, ValueType> solveEquationSystem(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
virtual storm::dd::Add<DdType, ValueType> solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> 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<DdType, ValueType> performMatrixVectorMultiplication(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b = nullptr, uint_fast64_t n = 1) const;
virtual storm::dd::Add<DdType, ValueType> multiply(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b = nullptr, uint_fast64_t n = 1) const;
protected:
// The matrix defining the coefficients of the linear equation system.

4
src/solver/SymbolicMinMaxLinearEquationSolver.cpp

@ -30,7 +30,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationSystem(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquations(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
// Set up the environment.
storm::dd::Add<DdType, ValueType> xCopy = x;
uint_fast64_t iterations = 0;
@ -66,7 +66,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::performMatrixVectorMultiplication(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b, uint_fast64_t n) const {
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::multiply(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b, uint_fast64_t n) const {
storm::dd::Add<DdType, ValueType> xCopy = x;
// Perform matrix-vector multiplication while the bound is met.

4
src/solver/SymbolicMinMaxLinearEquationSolver.h

@ -72,7 +72,7 @@ namespace storm {
* of A.
* @return The solution of the equation system.
*/
virtual storm::dd::Add<DdType, ValueType> solveEquationSystem(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
virtual storm::dd::Add<DdType, ValueType> solveEquations(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> 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<DdType, ValueType> performMatrixVectorMultiplication(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b = nullptr, uint_fast64_t n = 1) const;
virtual storm::dd::Add<DdType, ValueType> multiply(bool minimize, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b = nullptr, uint_fast64_t n = 1) const;
protected:
// The matrix defining the coefficients of the linear equation system.

6
src/solver/TopologicalMinMaxLinearEquationSolver.cpp

@ -33,7 +33,7 @@ namespace storm {
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
#ifdef GPU_USE_FLOAT
#define __FORCE_FLOAT_CALCULATION true
@ -49,7 +49,7 @@ namespace storm {
std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
std::vector<float> const new_b = storm::utility::vector::toValueType<float>(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<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void TopologicalMinMaxLinearEquationSolver<ValueType>::multiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;

4
src/solver/TopologicalMinMaxLinearEquationSolver.h

@ -32,9 +32,9 @@ namespace storm {
*/
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
virtual void solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const override;
virtual void multiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const override;
private:
storm::storage::SparseMatrix<ValueType> const& A;

2
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -210,7 +210,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
EXPECT_EQ(7ul, mdp->getNumberOfChoices());
auto solverFactory = std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>();
solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration);
solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<double>::SolutionMethod::PolicyIteration);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]");

28
test/functional/solver/EigenLinearEquationSolverTest.cpp

@ -29,7 +29,7 @@ TEST(EigenLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver<double> solver(A));
storm::solver::EigenLinearEquationSolver<double> 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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -58,7 +58,7 @@ TEST(EigenLinearEquationSolver, SparseLU) {
solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings<double>::SolutionMethod::SparseLU);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -84,7 +84,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) {
std::vector<storm::RationalNumber> b = {16, -4, -7};
storm::solver::EigenLinearEquationSolver<storm::RationalNumber> 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<storm::RationalFunction> b = {storm::RationalFunction(16), storm::RationalFunction(-4), storm::RationalFunction(-7)};
storm::solver::EigenLinearEquationSolver<storm::RationalFunction> 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<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -172,7 +172,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -202,7 +202,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -234,7 +234,7 @@ TEST(EigenLinearEquationSolver, GMRES) {
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -264,7 +264,7 @@ TEST(EigenLinearEquationSolver, GMRES_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -294,7 +294,7 @@ TEST(EigenLinearEquationSolver, GMRES_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -325,7 +325,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB) {
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -355,7 +355,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -385,7 +385,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -410,6 +410,6 @@ TEST(EigenLinearEquationSolver, MatrixVectorMultiplication) {
x[4] = 1;
storm::solver::EigenLinearEquationSolver<double> 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<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
}

4
test/functional/solver/EliminationLinearEquationSolverTest.cpp

@ -28,7 +28,7 @@ TEST(EliminationLinearEquationSolver, Solve) {
ASSERT_NO_THROW(storm::solver::EliminationLinearEquationSolver<double> solver(A));
storm::solver::EliminationLinearEquationSolver<double> 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<double> 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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}

16
test/functional/solver/GmmxxLinearEquationSolverTest.cpp

@ -28,7 +28,7 @@ TEST(GmmxxLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(A));
storm::solver::GmmxxLinearEquationSolver<double> 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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -60,7 +60,7 @@ TEST(GmmxxLinearEquationSolver, gmres) {
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -97,7 +97,7 @@ TEST(GmmxxLinearEquationSolver, qmr) {
solver2.getSettings().setMaximalNumberOfIterations(10000);
solver2.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -128,7 +128,7 @@ TEST(GmmxxLinearEquationSolver, bicgstab) {
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -158,7 +158,7 @@ TEST(GmmxxLinearEquationSolver, jacobi) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -189,7 +189,7 @@ TEST(GmmxxLinearEquationSolver, gmresilu) {
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -221,7 +221,7 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) {
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -246,6 +246,6 @@ TEST(GmmxxLinearEquationSolver, MatrixVectorMultiplication) {
x[4] = 1;
storm::solver::GmmxxLinearEquationSolver<double> 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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}

30
test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp

@ -19,10 +19,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) {
auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}
@ -43,17 +43,17 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio
auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
auto solver = factory.create(A);
solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(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::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
bound = 0.6;
solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true));
solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}
@ -78,23 +78,23 @@ TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) {
auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}
@ -110,12 +110,12 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
std::vector<double> b = { 0.099, 0.5 };
auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration);
factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<double>::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<storm::settings::modules::GmmxxEquationSolverSettings>().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<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}

4
test/functional/solver/NativeLinearEquationSolverTest.cpp

@ -28,7 +28,7 @@ TEST(NativeLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::solver::NativeLinearEquationSolver<double> solver(A));
storm::solver::NativeLinearEquationSolver<double> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@ -53,6 +53,6 @@ TEST(NativeLinearEquationSolver, MatrixVectorMultiplication) {
x[4] = 1;
storm::solver::NativeLinearEquationSolver<double> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}

20
test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp

@ -21,10 +21,10 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) {
auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
@ -49,23 +49,23 @@ TEST(NativeMinMaxLinearEquationSolver, MatrixVectorMultiplication) {
auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
@ -81,12 +81,12 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
std::vector<double> b = { 0.099, 0.5 };
auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>();
factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration);
factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<double>::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<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
Loading…
Cancel
Save