moves-rwth / storm

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

Fix always introducing the unexplored label. Fixes #559. #560

Closed tquatmann closed 4 months ago

tquatmann commented 4 months ago
./bin/storm --prism ../resources/examples/testfiles/dtmc/die.pm --state-limit 5

now introduces the unexplored label

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     5
Transitions:    7
Reward Models:  none
State Labels:   3 labels
   * unexplored -> 3 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

while the invocation without a state limit does not:

 ./bin/storm --prism ../resources/examples/testfiles/dtmc/die.pm                
-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     13
Transitions:    20
Reward Models:  none
State Labels:   2 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 
volkm commented 4 months ago

Thanks for the quick fix! LGTM