search

moves-rwth / storm

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

"Unexplored" label is always added #559

Closed volkm closed 3 days ago

volkm commented 1 month ago

The "unexplored" label introduced in #521 seems to be added even if all states are explored.

For the command

./bin/storm --prism ../resources/examples/testfiles/dtmc/die.pm

the resulting model still has the "unexplored" label:

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

Or is the "unexplored" label supposed to always be present (like "init" and "deadlock")?

tquatmann commented 1 month ago

Thanks! This was indeed an oversight. I don't think the unexplored label should be present all the time. Fixed in #560

volkm commented 4 weeks ago

It is not completely fixed yet: ./bin/storm --prism ../resources/examples/testfiles/dtmc/die.pm --prop "P=? [F \"one\"]" still has the unexplored label present for the goal state

--------------------------------------------------------------
Model type:     DTMC (sparse)
States:     13
Transitions:    20
Reward Models:  none
State Labels:   4 labels
   * unexplored -> 1 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * one -> 1 item(s)
Choice Labels:  none
--------------------------------------------------------------