moves-rwth / storm

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

storm-pars: revised region refinement #518

Open tquatmann opened 2 months ago

tquatmann commented 2 months ago

This PR refactors the code for the region model checking in storm-pars:

What still needs to be done is a (re-)implementation of the actual splitting strategies in RegionRefinementChecker::getSplittingVariables, most likely using obtainRegionSplitEstimates. Previously, this was done in a method called splitSmart.

Also, some more extensive testing would be helpful.

tquatmann commented 2 months ago

Thanks! Indeed, there are some API-related improvements to be made in region.h. This will probably also affect the command line interface. However, I suggest to do these in a separate PR as this one is already big enough.