Browse Source

Equation system based CTMC LRA solving: For the 'inner' linear equation system solver, also set whether the solver type has been set from default. This avoids potentially using unsound/inexact equation solvers.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
88c31b36d0
  1. 4
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

4
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -831,7 +831,7 @@ namespace storm {
auto subEnv = env;
if (subEnv.solver().getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological) {
// Topological solver does not make any sense since the BSCC is connected.
subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType());
subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault());
}
subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion());
@ -926,7 +926,7 @@ namespace storm {
auto subEnv = env;
if (subEnv.solver().getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological) {
// Topological solver does not make any sense since the BSCC is connected.
subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType());
subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault());
}
subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion());

Loading…
Cancel
Save