search

hlsyounes / ymer

Probabilistic model checker
GNU General Public License v2.0
4 stars 1 forks source link

Fails to compile property that references label #26

Closed hlsyounes closed 9 years ago

hlsyounes commented 9 years ago

Example property:

P<=0.56 [ F !"knowA" & "knowB" ]

hlsyounes commented 9 years ago

This happens when the label is in a sub expression. For example, for !"knowA", the property compiler sees that the negand compiles to a simple expression, so it just stores !"knowA" as the result. However, this later gets processed by the expression compiler, which does not support label expressions.

The language specification states that labels are only to appear in properties, so the expression compiler should not support them. I may have to duplicate code in the property compiler to compile expression properties, or find a way to conditionally accept labels in the expression compiler.