Skip to content

Formula parser fails for formulas with labels that contain special characters and whitespaces #705

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
TheGreatfpmK opened this issue May 13, 2025 · 1 comment · May be fixed by #706
Open

Formula parser fails for formulas with labels that contain special characters and whitespaces #705

TheGreatfpmK opened this issue May 13, 2025 · 1 comment · May be fixed by #706

Comments

@TheGreatfpmK
Copy link
Contributor

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.
@TheGreatfpmK TheGreatfpmK linked a pull request May 13, 2025 that will close this issue
Open
@TheGreatfpmK
Copy link
Contributor Author

I'm including an example of DRN model with such labels.

maze-label-problem.zip

You can try for example the property: Pmax=? [F "((x = 2) & (y = 0))"]

@volkm volkm mentioned this issue May 15, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fixing formula parser TheGreatfpmK/storm
1 participant
@TheGreatfpmK