diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 7612f16ec..add033af0 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -23,7 +23,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration", "topological"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "topological"}; this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); @@ -55,13 +55,16 @@ namespace storm { return storm::solver::MinMaxMethod::PolicyIteration; } else if (minMaxEquationSolvingTechnique == "linear-programming" || minMaxEquationSolvingTechnique == "lp") { return storm::solver::MinMaxMethod::LinearProgramming; - } else if (minMaxEquationSolvingTechnique == "ratsearch") { + } else if (minMaxEquationSolvingTechnique == "ratsearch" || minMaxEquationSolvingTechnique == "rs") { return storm::solver::MinMaxMethod::RationalSearch; - } else if (minMaxEquationSolvingTechnique == "quick-value-iteration" || minMaxEquationSolvingTechnique == "qvi") { - return storm::solver::MinMaxMethod::QuickValueIteration; + } else if (minMaxEquationSolvingTechnique == "interval-iteration" || minMaxEquationSolvingTechnique == "ii") { + return storm::solver::MinMaxMethod::IntervalIteration; + } else if (minMaxEquationSolvingTechnique == "sound-value-iteration" || minMaxEquationSolvingTechnique == "svi") { + return storm::solver::MinMaxMethod::SoundValueIteration; } else if (minMaxEquationSolvingTechnique == "topological") { return storm::solver::MinMaxMethod::Topological; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp index d088b2879..88a0c48fd 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp @@ -29,7 +29,7 @@ namespace storm { std::vector linearEquationSolver = {"gmm++", "native", "eigen", "elimination"}; this->addOption(storm::settings::OptionBuilder(moduleName, underlyingEquationSolverOptionName, true, "Sets which solver is considered for solving the underlying equation systems.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration"}; this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true, "Sets which minmax method is considered for solving the underlying minmax equation systems.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("value-iteration").build()).build()); } @@ -66,17 +66,23 @@ namespace storm { storm::solver::MinMaxMethod TopologicalEquationSolverSettings::getUnderlyingMinMaxMethod() const { std::string minMaxEquationSolvingTechnique = this->getOption(underlyingMinMaxMethodOptionName).getArgumentByName("name").getValueAsString(); - if (minMaxEquationSolvingTechnique == "value-iteration" || minMaxEquationSolvingTechnique == "vi") { + if (minMaxEquationSolvingTechnique == "value-iteration" || minMaxEquationSolvingTechnique == "vi") { return storm::solver::MinMaxMethod::ValueIteration; } else if (minMaxEquationSolvingTechnique == "policy-iteration" || minMaxEquationSolvingTechnique == "pi") { return storm::solver::MinMaxMethod::PolicyIteration; } else if (minMaxEquationSolvingTechnique == "linear-programming" || minMaxEquationSolvingTechnique == "lp") { return storm::solver::MinMaxMethod::LinearProgramming; - } else if (minMaxEquationSolvingTechnique == "ratsearch") { + } else if (minMaxEquationSolvingTechnique == "ratsearch" || minMaxEquationSolvingTechnique == "rs") { return storm::solver::MinMaxMethod::RationalSearch; - } else if (minMaxEquationSolvingTechnique == "quick-value-iteration" || minMaxEquationSolvingTechnique == "qvi") { - return storm::solver::MinMaxMethod::QuickValueIteration; + } else if (minMaxEquationSolvingTechnique == "interval-iteration" || minMaxEquationSolvingTechnique == "ii") { + return storm::solver::MinMaxMethod::IntervalIteration; + } else if (minMaxEquationSolvingTechnique == "sound-value-iteration" || minMaxEquationSolvingTechnique == "svi") { + return storm::solver::MinMaxMethod::SoundValueIteration; } + + + + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index cd6810a14..2aa60ded3 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -38,7 +38,7 @@ namespace storm { template MinMaxMethod IterativeMinMaxLinearEquationSolver::getMethod(Environment const& env, bool isExactMode) const { - // Adjust the method if none was specified and we are using rational numbers. + // Adjust the method if none was specified and we want exact or sound computations. auto method = env.solver().minMax().getMethod(); if (isExactMode && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) { @@ -48,8 +48,15 @@ namespace storm { } else { STORM_LOG_WARN("The selected solution method does not guarantee exact results."); } + } else if (env.solver().isForceSoundness() && method != MinMaxMethod::SoundValueIteration && method != MinMaxMethod::IntervalIteration && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) { + if (env.solver().minMax().isMethodSetFromDefault()) { + STORM_LOG_INFO("Selecting 'sound value iteration' as the solution technique to guarantee sound results. If you want to override this, please explicitly specify a different method."); + method = MinMaxMethod::SoundValueIteration; + } else { + STORM_LOG_WARN("The selected solution method does not guarantee sound results."); + } } - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::IntervalIteration, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); return method; } @@ -58,11 +65,7 @@ namespace storm { bool result = false; switch (getMethod(env, storm::NumberTraits::IsExact)) { case MinMaxMethod::ValueIteration: - if (env.solver().isForceSoundness()) { - result = solveEquationsSoundValueIteration(env, dir, x, b); - } else { - result = solveEquationsValueIteration(env, dir, x, b); - } + result = solveEquationsValueIteration(env, dir, x, b); break; case MinMaxMethod::PolicyIteration: result = solveEquationsPolicyIteration(env, dir, x, b); @@ -70,8 +73,11 @@ namespace storm { case MinMaxMethod::RationalSearch: result = solveEquationsRationalSearch(env, dir, x, b); break; - case MinMaxMethod::QuickValueIteration: - result = solveEquationsQuickSoundValueIteration(env, dir, x, b); + case MinMaxMethod::IntervalIteration: + result = solveEquationsIntervalIteration(env, dir, x, b); + break; + case MinMaxMethod::SoundValueIteration: + result = solveEquationsSoundValueIteration(env, dir, x, b); break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "This solver does not implement the selected solution method"); @@ -217,7 +223,7 @@ namespace storm { // Start by getting the requirements of the linear equation solver. LinearEquationSolverTask linEqTask = LinearEquationSolverTask::Unspecified; - if ((method == MinMaxMethod::ValueIteration && !this->hasInitialScheduler() && !hasInitialScheduler) || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { + if ((method == MinMaxMethod::ValueIteration && !this->hasInitialScheduler() && !hasInitialScheduler) || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::SoundValueIteration) { linEqTask = LinearEquationSolverTask::Multiply; } MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, linEqTask)); @@ -254,7 +260,7 @@ namespace storm { if (!this->hasUniqueSolution()) { requirements.requireValidInitialScheduler(); } - } else if (method == MinMaxMethod::QuickValueIteration) { + } else if (method == MinMaxMethod::SoundValueIteration) { if (!this->hasUniqueSolution()) { requirements.requireNoEndComponents(); } @@ -434,7 +440,7 @@ namespace storm { * Model Checker: Interval Iteration for Markov Decision Processes, CAV 2017). */ template - bool IterativeMinMaxLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + bool IterativeMinMaxLinearEquationSolver::solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given."); if (!this->linEqSolverA) { @@ -609,16 +615,11 @@ namespace storm { } template - class QuickValueIterationHelper { + class SoundValueIterationHelper { public: - QuickValueIterationHelper(std::vector& x, std::vector& y, bool relative, ValueType const& precision, uint64_t sizeOfLargestRowGroup) : x(x), y(y), hasLowerBound(false), hasUpperBound(false), minIndex(0), maxIndex(0), relative(relative), precision(precision) { + SoundValueIterationHelper(std::vector& x, std::vector& y, bool relative, ValueType const& precision, uint64_t sizeOfLargestRowGroup) : x(x), y(y), hasLowerBound(false), hasUpperBound(false), minIndex(0), maxIndex(0), relative(relative), precision(precision) { xTmp.resize(sizeOfLargestRowGroup); yTmp.resize(sizeOfLargestRowGroup); - - restart(); - } - - void restart() { x.assign(x.size(), storm::utility::zero()); y.assign(x.size(), storm::utility::one()); hasDecisionValue = false; @@ -627,6 +628,7 @@ namespace storm { firstIndexViolatingConvergence = 0; } + inline void setLowerBound(ValueType const& value) { hasLowerBound = true; lowerBound = value; @@ -834,7 +836,7 @@ namespace storm { ValueType meanBound = (upperBound + lowerBound) / storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(x, y, x, [&meanBound] (ValueType const& xi, ValueType const& yi) { return xi + yi * meanBound; }); - STORM_LOG_INFO("Quick Value Iteration terminated with lower value bound " + STORM_LOG_INFO("Sound Value Iteration terminated with lower value bound " << (hasLowerBound ? lowerBound : storm::utility::zero()) << (hasLowerBound ? "" : "(none)") << " and upper value bound " << (hasUpperBound ? upperBound : storm::utility::zero()) << (hasUpperBound ? "" : "(none)") @@ -968,7 +970,7 @@ namespace storm { }; template - bool IterativeMinMaxLinearEquationSolver::solveEquationsQuickSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + bool IterativeMinMaxLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Prepare the solution vectors. assert(x.size() == this->A->getRowGroupCount()); @@ -976,7 +978,7 @@ namespace storm { this->auxiliaryRowGroupVector = std::make_unique>(); } - QuickValueIterationHelper helper(x, *this->auxiliaryRowGroupVector, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), this->A->getSizeOfLargestRowGroup()); + SoundValueIterationHelper helper(x, *this->auxiliaryRowGroupVector, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), this->A->getSizeOfLargestRowGroup()); // Prepare initial bounds for the solution (if given) if (this->hasLowerBound()) { @@ -1394,7 +1396,7 @@ namespace storm { STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); auto method = env.solver().minMax().getMethod(); - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); std::unique_ptr> result = std::make_unique>(this->linearEquationSolverFactory->clone()); result->setRequirementsChecked(this->isRequirementsCheckedSet()); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index f8943a57a..5806ec4a2 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -37,8 +37,8 @@ namespace storm { bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; bool solveEquationsValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; - bool solveEquationsQuickSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index b543925e8..20194ec6b 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -197,7 +197,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(Environment const& env) const { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(); @@ -216,7 +216,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(Environment const& env) const { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::LinearProgramming) { result = std::make_unique>(std::make_unique>(), std::make_unique>()); diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index f2537f1a4..7344dde0a 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -14,8 +14,10 @@ namespace storm { return "topological"; case MinMaxMethod::RationalSearch: return "ratsearch"; - case MinMaxMethod::QuickValueIteration: - return "QuickValueIteration"; + case MinMaxMethod::IntervalIteration: + return "intervaliteration"; + case MinMaxMethod::SoundValueIteration: + return "soundvalueiteration"; case MinMaxMethod::TopologicalCuda: return "topologicalcuda"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index e2ffdb5dd..a4bc6d614 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -6,7 +6,7 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, QuickValueIteration, TopologicalCuda) + ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration) diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index a377689e4..57120ef77 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -113,7 +113,7 @@ namespace storm { std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(Environment const& env) const { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { result = std::make_unique>(this->linearEquationSolverFactory->clone()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected min max method is not supported by this solver."); diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index 668a94796..0538fa081 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -40,7 +40,7 @@ namespace { return env; } }; - class SparseDoubleSoundValueIterationEnvironment { + class SparseDoubleIntervalIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; @@ -50,13 +50,13 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); env.solver().minMax().setRelativeTerminationCriterion(false); return env; } }; - class SparseDoubleQuickValueIterationEnvironment { + class SparseDoubleSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; @@ -66,7 +66,7 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::QuickValueIteration); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); env.solver().minMax().setRelativeTerminationCriterion(false); return env; @@ -101,7 +101,7 @@ namespace { storm::Environment env; env.solver().setForceSoundness(true); env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); - env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::SoundValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); env.solver().minMax().setRelativeTerminationCriterion(false); return env; @@ -172,7 +172,7 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); env.solver().minMax().setRelativeTerminationCriterion(false); return env; @@ -335,8 +335,8 @@ namespace { typedef ::testing::Types< SparseDoubleValueIterationEnvironment, + SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment, - SparseDoubleQuickValueIterationEnvironment, SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment, SparseRationalPolicyIterationEnvironment,