storm
storm copied to clipboard
storm-pars: revised region refinement
This PR refactors the code for the region model checking in storm-pars:
- Separate region model checking code (i.e. analyze a given region) from code concerning region refinement (partitioning of the parameter space into sub-regions). This is achieved by having a
RegionRefinementChecker
that is responsible for the latter. - Allow different strategies that decide how a region is split into subregions. This can be configured using a
RegionSplittingStrategy
in theRegionRefinementChecker
. The strategy potentially can make use of region split estimates, which assign to each parameter a numerical value indicating how useful splitting for that parameter is. - Make code concerning monotonicity more modular. There is now a
MonotonicityBackend
that manages the computation of relevant monotonicity information and the propagation to subregions.
Thanks @linusheck for (re-)implementing region splitting strategies
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.