search

moves-rwth / storm

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

Over-restrictive syntax for property names #638

Open HubertGaravel opened 1 week ago

HubertGaravel commented 1 week ago

Although property names are enclosed between quotes (which logically means that they could accept any character), they cannot start with a digit. This goes against the intuition.

This is annoying when properties are referred to by numbers. The user is forced to insert a meaningless prefix such as prop1, prop2, etc.

Moreover, the error message emitted by Storm in such case is confusing, and lets the user think that the formula itself is incorrect, while the problem lies in the identifier of the formula.

Example:

ERROR (FormulaParser.cpp:97): Could not parse formula: "5min": LRAmin=? [ "avail" ];

"5max": LRAmax=? [ "avail" ];

ERROR (storm-cli.cpp:66): An unexpected exception occurred and caused Storm to terminate. The message of this exception is: std::exception

volkm commented 1 week ago

We follow the Prism syntax here (see documentation) which does not allow identifiers to start with a digit. This is also common in many programming languages. I agree that the error output could be improved here to better indicate the underlying issue.

HubertGaravel commented 1 week ago

Well, Storm already extends the Prism language in several ways, so it could generalize formula names.

It is true that many programming languages require identifiers to start with a letter, but surrounding identifiers by double quotes precisely suggests that this constraint is lifted, e.g. in Ada:

function F (S : String) return Integer; function "+" (Left, Right: Tree) return Tree; function "=" (X, Y: Node) return Boolean;

This is a minor point, but easily doable IMHO.