8000 Selection of model checking algorithm in stormvogel · Issue #277 · moves-rwth/stormvogel · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Selection of model checking algorithm in stormvogel #277

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
AlexBork opened this issue Apr 15, 2025 · 0 comments
Open

Selection of model checking algorithm in stormvogel #277

AlexBork opened this issue Apr 15, 2025 · 0 comments
Labels
nice-to-have

Comments

@AlexBork
Copy link

Currently, the setting of specific model checking algorithms (Value Iteration, Sound Value Iteration, ...) and parameters is only possible via stormpy and the setting of environments, e.g. for DTMCs

env = stormpy.Environment()
env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
env.solver_environment.native_solver_environment.precision = pycarl.gmp.gmp.Rational(1/1000)
env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration

While this works, I think it would be nice to have an abstraction layer here that allows a more convenient selection of the method and some basic parameters like the precision directly in stormvogel. In particular, this could help reduce some of the clunkiness that Storm has with respect to selecting the algorithms for different model types (setting the EquationSolver for DTMCs, the MinMaxEquationSolver for MDPs, etc.).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
nice-to-have
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@AlexBork
0