moves-rwth / storm

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

State labels in explicit-drn are parsed incorrectly #49

Closed jjguijt closed 5 years ago

jjguijt commented 5 years ago

When using storm-pomdp to transform a POMDP to a pMC without (user created) labels, states in the resulting explicit-drn file will be labeled with the expression from the property (e.g. when using [F a = b] as a prop, a state in the resulting file may be labeled with (a = b).

When the resulting file is parsed by storm-pars, the parentheses are not taken into account. Alternatively, this could be considered a bug in storm-pomdp (since it introduces the spaces) or it can be considered bad practice not to use labels.

For example (is used a = s1 in the prop):

$ storm-pars --explicit-drn shields-warehouse/storm-pmc-g-no-crash.drn
Storm-pars 1.3.1 (dev)

Date: Thu Jul 18 17:33:53 2019
Command line arguments: --explicit-drn shields-warehouse/storm-pmc-g-no-crash.drn
Current working directory: /home/jeremy/study/internship

Time for model construction: 1.946s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     441
Transitions:    2457
Reward Models:  none
State Labels:   4 labels
   * s1) -> 420 item(s)
   * init -> 1 item(s)
   * (a -> 420 item(s)
   * != -> 420 item(s)
Choice Labels:  none
--------------------------------------------------------------

I can add more info/source files if it's needed.

sjunges commented 5 years ago

In short, we do recommend to use labels here, however, we have fixed the issue by putting quotation marks around labels with spaces. The parser should also adhere to this.

jjguijt commented 5 years ago

Thanks!