Add synthesis for exact POMDPs #56
Conversation
paynt/verification/property.py
Outdated
| # se.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration | ||
| # se.minmax_solver_environment.method = stormpy.MinMaxMethod.sound_value_iteration | ||
| # se.minmax_solver_environment.method = stormpy.MinMaxMethod.interval_iteration | ||
| se.minmax_solver_environment.method = stormpy.MinMaxMethod.optimistic_value_iteration |
There was a problem hiding this comment.
We prefer to use OVI by default. If you need other methods, should we introduce a CLI option?
There was a problem hiding this comment.
When using PAYNT from the outside, it would probably be cool if you can set the environment from the outside!
Other than that, exact solving needs policy iteration as OVI will not converge to the precise solution if there is a cycle.
There was a problem hiding this comment.
Can we keep OVi as a default but use policy iteration if --exact option has been used?
| # se.set_linear_equation_solver_type(stormpy.EquationSolverType.gmmxx) | ||
| # se.set_linear_equation_solver_type(stormpy.EquationSolverType.eigen) | ||
| se.set_linear_equation_solver_type(stormpy.EquationSolverType.eigen) |
There was a problem hiding this comment.
I am not familiar with these settings, so I don't have a preference, but if this change is intentional, I am curious why.
There was a problem hiding this comment.
Eigen has a much better exact solution engine than our native solver.
This pull request contains a first implementation to get PAYNT to do exact calculations.
It only works for POMDPs (not sure if only memoryless). I tested it for several of the pomdp examples, and they all work. However, I thus only tested happy paths.
I also allowed the prism and drn parser to build models as exact. This can be used by calling
paynt.pyusing the--exactflag.