diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 5615ed47e..d86107386 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -229,8 +229,6 @@ namespace storm { } } - - template MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { auto method = getMethod(env, storm::NumberTraits::IsExact); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index df0fef614..0378e0cce 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -203,7 +203,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::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::ViToPi) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::OptimisticValueIteration || method == MinMaxMethod::ViToPi) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(); @@ -222,7 +222,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::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::ViToPi) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::OptimisticValueIteration || method == MinMaxMethod::ViToPi) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::LinearProgramming) { result = std::make_unique>(std::make_unique>()); diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index f635b5a38..0b6836b8a 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -18,6 +18,8 @@ namespace storm { return "intervaliteration"; case MinMaxMethod::SoundValueIteration: return "soundvalueiteration"; + case MinMaxMethod::OptimisticValueIteration: + return "optimisticvalueiteration"; case MinMaxMethod::TopologicalCuda: return "topologicalcuda"; case MinMaxMethod::ViToPi: diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 8c1a39e51..bad126df8 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -6,7 +6,7 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxMethod, ValueIteration, OptimisticValueIteration, PolicyIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda, ViToPi) + ExtendEnumsWithSelectionField(MinMaxMethod, ValueIteration, PolicyIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, OptimisticValueIteration, TopologicalCuda, ViToPi) ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration, GainBiasEquations, LraDistributionEquations) diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index f1adc99ee..acc9f3679 100755 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -92,6 +92,7 @@ namespace { return env; } }; + class SparseDoubleSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models @@ -109,6 +110,23 @@ namespace { } }; + class SparseDoubleOptimisticValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MdpEngine engine = MdpEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; + class SparseDoubleTopologicalValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models @@ -229,6 +247,22 @@ namespace { return env; } }; + class HybridCuddDoubleOptimisticValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const MdpEngine engine = MdpEngine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; class HybridSylvanRationalPolicyIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; @@ -418,6 +452,7 @@ namespace { JitSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment, + SparseDoubleOptimisticValueIterationEnvironment, SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment, SparseRationalPolicyIterationEnvironment, @@ -426,6 +461,7 @@ namespace { HybridCuddDoubleValueIterationEnvironment, HybridSylvanDoubleValueIterationEnvironment, HybridCuddDoubleSoundValueIterationEnvironment, + HybridCuddDoubleOptimisticValueIterationEnvironment, HybridSylvanRationalPolicyIterationEnvironment, DdCuddDoubleValueIterationEnvironment, JaniDdCuddDoubleValueIterationEnvironment, diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp index 6c027da73..df0cb62fe 100644 --- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp @@ -23,6 +23,7 @@ namespace { return env; } }; + class DoubleSoundViEnvironment { public: typedef double ValueType; @@ -48,6 +49,19 @@ namespace { return env; } }; + + class DoubleOptimisticViEnvironment { + public: + typedef double ValueType; + static const bool isExact = false; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration); + env.solver().setForceSoundness(true); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + }; class DoubleTopologicalViEnvironment { public: @@ -124,6 +138,7 @@ namespace { DoubleViEnvironment, DoubleSoundViEnvironment, DoubleIntervalIterationEnvironment, + DoubleOptimisticViEnvironment, DoubleTopologicalViEnvironment, DoubleTopologicalCudaViEnvironment, DoublePIEnvironment,