From 88c31b36d04cc2e77913cc3dcf1847fb87cab49e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 20 Apr 2020 08:09:29 +0200 Subject: [PATCH] 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. --- src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 55cae421b..ab8912c5d 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/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());