From 4a34fb1a7c4190e11a1f6d8097bedd8837d7dbe5 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 4 Mar 2020 16:28:28 +0100
Subject: [PATCH] MaTest: Making sure that the 'inner' MinMax solver for unif+
is allowed to switch the solution method.
---
.../csl/MarkovAutomatonCslModelCheckerTest.cpp | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp
index fea7794ce..31c0ca29c 100755
--- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp
@@ -40,7 +40,7 @@ namespace {
typedef storm::models::sparse::MarkovAutomaton<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
@@ -54,7 +54,7 @@ namespace {
typedef storm::models::sparse::MarkovAutomaton<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
@@ -68,7 +68,7 @@ namespace {
typedef storm::models::sparse::MarkovAutomaton<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
@@ -82,7 +82,7 @@ namespace {
typedef storm::models::symbolic::MarkovAutomaton<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
@@ -97,7 +97,7 @@ namespace {
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration, true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
@@ -112,7 +112,7 @@ namespace {
typedef storm::models::sparse::MarkovAutomaton<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration, true);
return env;
}
};
@@ -125,7 +125,7 @@ namespace {
typedef storm::models::sparse::MarkovAutomaton<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
- env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
+ env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch, true);
return env;
}
};