moves-rwth / storm

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

Add warning in API concerning properties containing model variables #557

Closed AlexBork closed 1 month ago

AlexBork commented 1 month ago

The parseProperties function taking only a string as input is not able to parse properties containing model variables as these are not registered with the created ExpressionManager. This is expected behaviour, however, the resulting error message of the form

ERROR (SpiritErrorHandler.h:27): Parsing error at 1:2:  expecting <basic path formula>, here:
    X (var = 0)]
     ^

does not point to the actual problem, making debugging the issue difficult, in particular for inexperienced users. This PR adds a warning to the function that makes the issue more apparent.

Thanks to @SvStein for bringing this to my attention.

AlexBork commented 1 month ago

If you think the warning should only come up when in DEBUG mode, please let me know.

I also considered making the parser error message more meaningful, though that seems to require a lot more changes for a use cases I don't expect to come up too often.

volkm commented 1 month ago

The current version would always output a warning. I imagine this could be quite confusing for users who input a string without model parameters, because they have to ignore the warning. Would it be possible to provide the warning/error somewhere in the Spirit parser such that the output only occurs when really needed? (From your comment I guess that this would be too work though?

sjunges commented 1 month ago

Isnt that exactly iff the error is thrown?

AlexBork commented 1 month ago

The error can also occur when there is a different issue with the input, so it's not an iff. I'd like to give a hint if parsing fails in the specific context of the API call as someone who is not fully aware of how the parser works (i.e. someone like me) would assume that giving a syntactically valid formula should parse. So the error message/warning/hint should not come up in all contexts as it might also be confusing.

Would adding an error handler to the API fucntion be an option? That way, we can give the additional hint only if the specific error occurs in the context of the API call.

volkm commented 1 month ago

Does the Spirit parser throw an exception which we could catch in the API call and then output the additional information?

volkm commented 1 month ago

The updated version looks good to me. Thanks for improving the usability.

sjunges commented 1 month ago

@linusheck this was what we discussed last week!