diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp
index 9825d926b..edde86615 100644
--- a/src/storm/environment/solver/SolverEnvironment.cpp
+++ b/src/storm/environment/solver/SolverEnvironment.cpp
@@ -23,6 +23,7 @@ namespace storm {
SolverEnvironment::SolverEnvironment() {
forceSoundness = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet();
+ forceExact = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet();
linearEquationSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
linearEquationSolverTypeSetFromDefault = storm::settings::getModule<storm::settings::modules::CoreSettings>().isEquationSolverSetFromDefaultValue();
}
@@ -111,6 +112,14 @@ namespace storm {
SolverEnvironment::forceSoundness = value;
}
+ bool SolverEnvironment::isForceExact() const {
+ return forceExact;
+ }
+
+ void SolverEnvironment::setForceExact(bool value) {
+ SolverEnvironment::forceExact = value;
+ }
+
storm::solver::EquationSolverType const& SolverEnvironment::getLinearEquationSolverType() const {
return linearEquationSolverType;
}
diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h
index 4f0a88869..487213918 100644
--- a/src/storm/environment/solver/SolverEnvironment.h
+++ b/src/storm/environment/solver/SolverEnvironment.h
@@ -48,6 +48,8 @@ namespace storm {
bool isForceSoundness() const;
void setForceSoundness(bool value);
+ bool isForceExact() const;
+ void setForceExact(bool value);
storm::solver::EquationSolverType const& getLinearEquationSolverType() const;
void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool isSetFromDefault = false);
@@ -70,6 +72,7 @@ namespace storm {
storm::solver::EquationSolverType linearEquationSolverType;
bool linearEquationSolverTypeSetFromDefault;
bool forceSoundness;
+ bool forceExact;
};
}
diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 6d82a6d79..5911b4044 100644
--- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -576,7 +576,7 @@ namespace storm {
}
storm::solver::LraMethod method = env.solver().lra().getDetLraMethod();
- if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) {
+ if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) {
method = storm::solver::LraMethod::GainBiasEquations;
STORM_LOG_INFO("Selecting " << storm::solver::toString(method) << " as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
} else if (env.solver().isForceSoundness() && env.solver().lra().isDetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 8e6f427ab..0fac47232 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -820,7 +820,7 @@ namespace storm {
// Solve MEC with the method specified in the settings
storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
- if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
+ if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::LinearProgramming;
} else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 0bcc31726..122814633 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -1477,7 +1477,7 @@ namespace storm {
// Solve MEC with the method specified in the settings
storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
- if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
+ if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::LinearProgramming;
} else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {
diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp
index 6c96715cf..0ca9a4554 100644
--- a/src/storm/solver/EigenLinearEquationSolver.cpp
+++ b/src/storm/solver/EigenLinearEquationSolver.cpp
@@ -107,7 +107,7 @@ namespace storm {
auto eigenX = StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1>::Map(b.data(), b.size());
- auto solutionMethod = getMethod(env, false);
+ auto solutionMethod = getMethod(env, env.solver().isForceExact());
if (solutionMethod == EigenLinearEquationSolverMethod::SparseLU) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library).");
StormEigen::SparseLU<StormEigen::SparseMatrix<ValueType>, StormEigen::COLAMDOrdering<int>> solver;
diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp
index 9ce51fa72..a42386c0e 100644
--- a/src/storm/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp
@@ -46,6 +46,7 @@ namespace storm {
template<typename ValueType>
GmmxxLinearEquationSolverMethod GmmxxLinearEquationSolver<ValueType>::getMethod(Environment const& env) const {
STORM_LOG_ERROR_COND(!env.solver().isForceSoundness(), "This linear equation solver does not support sound computations. Using unsound methods now...");
+ STORM_LOG_ERROR_COND(!env.solver().isForceExact(), "This linear equation solver does not support exact computations. Using unsound methods now...");
return env.solver().gmmxx().getMethod();
}
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index df53fb538..44a2ee9a5 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -64,7 +64,7 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool result = false;
- switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
+ switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact())) {
case MinMaxMethod::ValueIteration:
result = solveEquationsValueIteration(env, dir, x, b);
break;
@@ -228,7 +228,7 @@ namespace storm {
template<typename ValueType>
MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
- auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+ auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
// Check whether a linear equation solver is needed and potentially start with its requirements
bool needsLinEqSolver = false;
diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp
index 8207efcff..5d2884d86 100644
--- a/src/storm/solver/LinearEquationSolver.cpp
+++ b/src/storm/solver/LinearEquationSolver.cpp
@@ -128,8 +128,15 @@ namespace storm {
std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
EquationSolverType type = env.solver().getLinearEquationSolverType();
- // Adjust the solver type if none was specified and we want sound computations
- if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
+ // Adjust the solver type if none was specified and we want sound/exact computations
+ if (env.solver().isForceExact() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
+ if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) {
+ type = EquationSolverType::Eigen;
+ STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee exact results. If you want to override this, please explicitly specify a different solver.");
+ } else {
+ STORM_LOG_WARN("The selected solver does not yield exact results.");
+ }
+ } else if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) {
type = EquationSolverType::Native;
STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee sound results. If you want to override this, please explicitly specify a different solver.");
diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp
index ca0142249..a79bc6b3e 100644
--- a/src/storm/solver/NativeLinearEquationSolver.cpp
+++ b/src/storm/solver/NativeLinearEquationSolver.cpp
@@ -922,7 +922,7 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
- switch(getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
+ switch(getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact())) {
case NativeLinearEquationSolverMethod::SOR:
return this->solveEquationsSOR(env, x, b, storm::utility::convertNumber<ValueType>(env.solver().native().getSorOmega()));
case NativeLinearEquationSolverMethod::GaussSeidel:
@@ -946,7 +946,7 @@ namespace storm {
template<typename ValueType>
LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat(Environment const& env) const {
- auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+ auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundValueIteration || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) {
return LinearEquationSolverProblemFormat::FixedPointSystem;
} else {
@@ -957,7 +957,7 @@ namespace storm {
template<typename ValueType>
LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env) const {
LinearEquationSolverRequirements requirements;
- auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+ auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
if (method == NativeLinearEquationSolverMethod::IntervalIteration) {
requirements.requireBounds();
} else if (method == NativeLinearEquationSolverMethod::RationalSearch) {
diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp
index a818f2706..8fcc46a80 100644
--- a/src/storm/solver/StandardGameSolver.cpp
+++ b/src/storm/solver/StandardGameSolver.cpp
@@ -72,7 +72,7 @@ namespace storm {
template<typename ValueType>
bool StandardGameSolver<ValueType>::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices, std::vector<uint64_t>* player2Choices) const {
- auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
+ auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value || env.solver().isForceExact());
STORM_LOG_INFO("Solving stochastic two player game over " << x.size() << " states using " << toString(method) << ".");
switch (method) {
case GameMethod::ValueIteration: