Open
Description
In the DRN format, you can have state labels that include special characters and even whitespaces. These are parsed without problem in model parser. For example if you generate DRN from PRISM which used some prism formula to denote goal state you can see a label that looks something like this: "((x = 2) & (y = 0))".
If you try to parse property containing label "((x = 2) & (y = 0))" you will get the following error:
ERROR (SpiritErrorHandler.h:26): Parsing error at 1:2: expecting <basic path formula>, here:
F "((x = 2) & (y = 0))"]
^
ERROR (properties.cpp:53): WrongFormatException: Parsing error at 1:2: expecting <basic path formula>, here:
F "((x = 2) & (y = 0))"]
^
Note that the used API function does not have access to model variables. If the property you tried to parse contains model variables, it will not be parsed correctly.
ERROR (storm-cli.cpp:63): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: WrongFormatException: Parsing error at 1:2: expecting <basic path formula>, here:
F "((x = 2) & (y = 0))"]
This is because in the property grammar the label can only contain alphanumeric symbols and underscore.
Metadata
Metadata
Assignees
Labels
No labels