From dc8612b75157a58f2874b67322d0021875b22293 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 22 Oct 2020 15:55:56 +0200 Subject: [PATCH] Fixed not always using the acyclic solver within LRA and multi-objective time-bounded reachability computations. --- .../helper/infinitehorizon/internal/LraViHelper.cpp | 8 ++------ .../pcaa/StandardMaPcaaWeightVectorChecker.cpp | 6 ++---- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index eb8c002ed..2a4f6950a 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -259,12 +259,8 @@ namespace storm { bool isAcyclic = !storm::utility::graph::hasCycle(_IsTransitions); if (isAcyclic) { STORM_LOG_INFO("Instant transitions are acyclic."); - if (_IsSolverEnv->solver().minMax().isMethodSetFromDefault()) { - _IsSolverEnv->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic); - } - if (_IsSolverEnv->solver().isLinearEquationSolverTypeSetFromDefaultValue()) { - _IsSolverEnv->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic); - } + _IsSolverEnv->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic); + _IsSolverEnv->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic); } if (nondetIs()) { storm::solver::GeneralMinMaxLinearEquationSolverFactory factory; diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 029e8244f..42ddf97e3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -332,8 +332,7 @@ namespace storm { std::unique_ptr result(new MinMaxSolverData()); result->env = std::make_unique(env); // For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified) - if (acyclic && result->env->solver().minMax().isMethodSetFromDefault() && result->env->solver().minMax().getMethod() != storm::solver::MinMaxMethod::Acyclic) { - STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver."); + if (acyclic) { result->env->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic); } storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; @@ -372,8 +371,7 @@ namespace storm { result->env = std::make_unique(env); result->acyclic = acyclic; // For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified) - if (acyclic && result->env->solver().isLinearEquationSolverTypeSetFromDefaultValue() && result->env->solver().getLinearEquationSolverType() != storm::solver::EquationSolverType::Acyclic) { - STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver."); + if (acyclic) { result->env->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic); } result->factory = std::make_unique>();