Skip to content
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.

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

Properties containing rationals with either the denominator or numerator containing a number >= $2^63$ causes the property not to be recognized #652

Open
lukovdm opened this issue Jan 10, 2025 · 0 comments

Comments

@lukovdm
Copy link

lukovdm commented Jan 10, 2025

When calling storm on any model with a property such as: "P>9223372036854775808/9223372036854775808 [F \"goal\"]" You get the following error:

ERROR (SpiritErrorHandler.h:26): Parsing error at 1:3:  expecting <expression>, here:
        P>9223372036854775808/9223372036854775808 [F "goal"]
          ^

ERROR (properties.cpp:54): WrongFormatException: Parsing error at 1:3:  expecting <expression>, here:
        P>9223372036854775808/9223372036854775808 [F "goal"]
          ^
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:3:  expecting <expression>, here:
        P>9223372036854775808/9223372036854775808 [F "goal"]
          ^
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.

This can for example be obtained using the command:
storm -drn storm/resources/examples/testfiles/dtmc/crowds-5-5.drn --prop "P>9223372036854775808/9223372036854775808 [F \"goal\"]"

I would expect either the error to say that a too large number was found or for it to be accepted.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant