From feb279c7d1daa44e7abd0cfe6971bd23b2ff9532 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 2 Dec 2019 16:00:43 +0100 Subject: [PATCH] Environment extended to select the model checking algorithm for Markov chains --- src/core/environment.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index f9c1596..ecc46b0 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -19,6 +19,17 @@ void define_environment(py::module& m) { .value("topological", storm::solver::EquationSolverType::Topological) ; + py::enum_(m, "NativeLinearEquationSolverMethod", "Method for linear equation systems with the native solver") + .value("power_iteration", storm::solver::NativeLinearEquationSolverMethod::Power) + .value("sound_value_iteration", storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration) + .value("interval_iteration", storm::solver::NativeLinearEquationSolverMethod::IntervalIteration) + .value("rational_search", storm::solver::NativeLinearEquationSolverMethod::RationalSearch) + .value("jacobi", storm::solver::NativeLinearEquationSolverMethod::Jacobi) + .value("SOR", storm::solver::NativeLinearEquationSolverMethod::SOR) + .value("gauss_seidel", storm::solver::NativeLinearEquationSolverMethod::GaussSeidel) + .value("walker_chae", storm::solver::NativeLinearEquationSolverMethod::WalkerChae) + ; + py::enum_(m, "MinMaxMethod", "Method for min-max equation systems") .value("policy_iteration", storm::solver::MinMaxMethod::PolicyIteration) .value("value_iteration", storm::solver::MinMaxMethod::ValueIteration) @@ -30,7 +41,6 @@ void define_environment(py::module& m) { .value("topological_cuda", storm::solver::MinMaxMethod::TopologicalCuda) ; - py::class_(m, "Environment", "Environment") .def(py::init<>(), "Construct default environment") .def_property_readonly("solver_environment", [](storm::Environment& env) -> auto& {return env.solver();}, "solver part of environment") @@ -40,6 +50,12 @@ void define_environment(py::module& m) { .def("set_force_sound", &storm::SolverEnvironment::setForceSoundness, "force soundness", py::arg("new_value") = true) .def("set_linear_equation_solver_type", &storm::SolverEnvironment::setLinearEquationSolverType, "set solver type to use", py::arg("new_value"), py::arg("set_from_default") = false) .def_property_readonly("minmax_solver_environment", [](storm::SolverEnvironment& senv) -> auto& { return senv.minMax(); }) + .def_property_readonly("native_solver_environment", [](storm::SolverEnvironment& senv) -> auto& {return senv.native(); }) + ; + + py::class_(m, "NativeSolverEnvironment", "Environment for Native solvers") + .def_property("method", &storm::NativeSolverEnvironment::getMethod, [](storm::NativeSolverEnvironment& nsenv, storm::solver::NativeLinearEquationSolverMethod const& m) {nsenv.setMethod(m);}) + .def_property("maximum_iterations", &storm::NativeSolverEnvironment::getMaximalNumberOfIterations, [](storm::NativeSolverEnvironment& nsenv, uint64_t iters) {nsenv.setMaximalNumberOfIterations(iters);} ) ; py::class_(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers")