search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
135 stars 74 forks source link

Missing check for optimization direction in SparseParametricMdpSimplifier #516

Open volkm opened 6 months ago

volkm commented 6 months ago

The following execution results in an assertion violation:

/bin/storm-pars --prism ../resources/examples/testfiles/pmdp/brp16_2.nm --prop "P<=0.01 [F s=5]" --mode feasibility --feasibility:method pla --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"

The issue is that no optimization direction is specified in the property and accessing the corresponding variable then fails in https://github.com/moves-rwth/storm/blob/master/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp#L178.

I could add a check for each simplification function in the class but I was wondering if there is a better place where to check it?

linusheck commented 3 months ago

This might depend on https://github.com/moves-rwth/storm/issues/528, but we can also just add a check everywhere for now