Expose state sorting option in prism.Prism #102
Conversation
Although it is possible to enable or disable state sorting in an explicit ModelGenerator directly, it is not possible to do so via the prism.Prism class, which is the more common way to interact with the PRISM API. Create a new setting PRISM_SORT_STATES to control this behaviour in underlying explicit ModelGenerators, and add methods for controlling its value in prism.Prism.
|
I think there is not much of a difference between having it as a setting in PrismSettings (exposed via the GUI) or having it on the command-line, as both are user facing. But I'd really like to get this exposed to the user, as it can lead to significant speed-ups. From the old PR, there was a question whether it makes sense to have other-than-lexicographic ordering for the symbolic engines, and I think there is no easy way to achieve that. So, it's mainly a question for the explicit engine. One option would be just to provide a "sort=yes/no" switch (similar to the one proposed here, in the sense of "ensure that the states are sorted lexicographically"). Other option would be to go with a "sort=lexicographic|dfs|bfs" switch, which gives a bit more extendability (and where some variants would just not apply to the symbolic engines, perhaps resulting in a warning). |
Includes one patch for configuring state sorting that isn't currently merged into PRISM: prismmodelchecker/prism#102
davexparker
force-pushed
the
master
branch
2 times, most recently
from
ca12ca0 to
6bf73df
Compare
I should've included this as part of PR #94, but it had been merged by the time I realised I left it out.
PR #94 makes it possible to enable or disable state sorting in an explicit
ModelGeneratordirectly, but the more common way of interacting with aModelGeneratoris indirectly viaprism.Prism, which doesn't expose access to the underlyingModelGenerator. This PR creates a new settingPRISM_SORT_STATESthat makes it possible to control state sorting viaprism.Prism. (The ability to control the value ofPRISM_SORT_STATESin turn via the command line is deliberately omitted from this PR, for all the reasons discussed in #94.)