iMC changes outside of storm-pars #627
Conversation
|
Does this depend on #588? That PR is still not ready for merging, is it? |
It doesn’t depend on that PR I‘m pretty sure, because that PR (mainly) changes things in storm-pars. The open discussion was about the behavior of the CLI flag but that is definitely in storm-pars. |
|
Ok, I see that there are indeed some changes outside of storm-pars in there, but those are not under discussion :D |
| @@ -166,6 +166,9 @@ storm::expressions::Expression Z3ExpressionAdapter::translateExpression(z3::expr | |||
| return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); | |||
| } | |||
| } | |||
| case Z3_OP_AGNUM: | |||
| return manager.rational(storm::utility::convertNumber<storm::RationalNumber>( | |||
| std::string(Z3_get_numeral_string(expr.ctx(), Z3_get_algebraic_number_lower(expr.ctx(), expr, 16))))); | |||
There was a problem hiding this comment.
A brief comment would help. In particular, what is the 16? z3 docs say "The interval isolating the number is smaller than 1/10^precision."
There was a problem hiding this comment.
I agree that the hardcoded precision is bad, but I'm not sure how to make this configurable in a way that makes sense.
There was a problem hiding this comment.
Imo, just a small comment would already help to make it obvious that some rounding happens here.
Also, the Z3ExpressionAdapter could have a flag bool AllowRoundingAlgebraicNumbers that one has to set to true in contexts where algebraic numbers should be expected and where rounding would be fine. Otherwise, I can see that this could become a somewhat unexpected source of approximation error.
| namespace storm::storage { | ||
|
|
||
| /*! | ||
| * This class represents the decomposition of a nondeterministic model into its maximal end components. |
There was a problem hiding this comment.
The RobustMaximalEndComponent[Decomposition] introduce some code duplications with the non-robust versions. Is it possible to merge the two? Maybe one can simply add a bool robust flag somewhere?
If that is not possible, please add some comment (why does this need to be a separate class, what's the difference between robust vs. non-robust MECs, ...)
There was a problem hiding this comment.
I deleted the RobustMaximalEndComponent :)
The RobustMaximalEndComponentDecomposition has almost entirely different code to the MaximalEndComponentDecomposition right now, but I totally see that we should merge them to support models like iMDPs in the future. It might be a bit fiddly to implement Haddad-Monmege's algorithm for iMDPs while not regressing performance on standard MDPs.
For now, it should be possible to add a bool robust and switch between the different algorithms. I'll attempt that next week :)
There was a problem hiding this comment.
the robust flag can be a compile-time constant (set to std::is_same_v<ValueType, storm::Interval> or as extra template parameter). Then, this should be possible without runtime penalities for standard MDPs
There was a problem hiding this comment.
the
robustflag can be a compile-time constant (set tostd::is_same_v<ValueType, storm::Interval>or as extra template parameter). Then, this should be possible without runtime penalities for standard MDPs
It's a bit more difficult:
- the robust maximal end component decomposition needs the vector as well, not just the matrix, so the method signatures are different
- the current end component decomposition is based on
MaximalEndComponent, but that class has a bunch of methods that are nonsensical for robust end components, like the choices per state
There was a problem hiding this comment.
Ahh, I did not notice the vector. What is this representing? It is probably helpful to add documentation for that :)
I propose to merge the PR with a RobustMaximalEndComponentDecomposition and we can try to reduce the code duplications in a separate PR. I believe C++20 concepts and requires expressions could handle this quite elegantly.
Draft PR containing all changes I made for iMC algorithms that are outside of
storm-pars. Tests in the storm-pars part (no PR for this yet) cover most lines in this PR.In more detail, this PR contains:
FlexibleSparseMatrixthat adds new rowsSchedulerTrackingHelperfor iMCs and a interval (=robust) scheduler index in the minmax solvers for warm-starting(Iterative)MinMaxLinearEquationSolveraddNotCurrentModelfunction for SMT solvers that adds the constraint that the current model is not a solutionRobustMaximalEndComponentDecomposition,RobustMaximalEndComponent)ValueIterationOperatorfor iMCsstorm::Interval