storm icon indicating copy to clipboard operation
storm copied to clipboard

storm-pars: revised region refinement

Open tquatmann opened this issue 10 months ago • 5 comments

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 the RegionRefinementChecker. 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

tquatmann avatar Apr 10 '24 14:04 tquatmann

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.

tquatmann avatar Apr 11 '24 13:04 tquatmann