Added option to limit the number of explored states

[tquatmann]

Added option --build:state limit <number> which, if set, stops expanding new states once the given <number> of states has been found.

This is useful for, e.g., debugging models that normally would be too large. If there are unexplored states, a label "unexplored" is added and assigned to them. This even allows to calculate the probability to exit the fraction of the explored state space.

$ storm --prism resources/examples/testfiles/dtmc/crowds-5-5.pm --state-limit 8500 --prop 'P=? [F "unexplored"]' 
Storm 1.8.2 (dev)
DEBUG BUILD

Date: Fri Apr 12 13:51:26 2024
Command line arguments: --prism ../resources/examples/testfiles/dtmc/crowds-5-5.pm --state-limit 8500 --prop 'P=? [F "unexplored"]'
Current working directory: /Users/tim/storm/build

Time for model input parsing: 0.010s.

Time for model construction: 0.060s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     8500
Transitions:    15006
Reward Models:  none
State Labels:   3 labels
   * unexplored -> 140 item(s)
   * deadlock -> 1120 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": P=? [F "unexplored"] ...
Result (for initial states): 0.001353870181
Time for model checking: 0.016s.

Note: the "unexplored" label does not exist if all states are explored.

[sjunges]

LGTM. One nitpicky comment :-)