FormulaParser: Weird error messages when Variable Names coincide with operators

[tquatmann]

If variables like R or C are used in the input model, formulas containing these letters as Operators cannot be parsed and yield error messages that are hard to understand.

Example:

storm --prism test.prism --prop 'R{"one"}=? [ C<4 ]'
[...]
ERROR (FormulaParserGrammar.cpp:294): Expected expression of boolean type.
ERROR (storm.cpp:23): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: Expected expression of boolean type.

With PRISM model

dtmc
const int R = 1;
const int C = 2;
module main
    x : [0..1];
    [] x<C -> (x'=R);
endmodule

rewards "one"
    true : 1;
endrewards

and cumulative reward formula R{"one"}=? [ C<4].

I'm actually not sure whether this input should be possible or not. If yes, what about e.g. this formula: R<R [ C<C ]? (first R would be the reward operator, second R would be the constant from the PRISM model, similar for the two C).

In any case, a better error message might be helpful.

[sjunges]

https://www.prismmodelchecker.org/manual/ThePRISMLanguage/ModulesAndVariables

Prism considers them as reserved keywords. I think that that is a fair assumption.

[tquatmann]

Yes, I agree. Only problem is that this is also problematic for JANI models. There actually are JANI models out there, that use e.g. C as a constant. So the combination of JANI input model and a property specification in PRISM-style might still not work.

I would propose to

• consider operators as reserved keywords for PRISM models and
• Issue a warning when a PRISM-style property specification is parsed and an operator appears as a variable name (e.g. in a JANI model).

[tquatmann]

With the (more or less) recent formula parser update, we now have this

Storm 1.6.4 (dev)

Date: Thu Nov 11 10:49:08 2021
Command line arguments: --prism test.prism --prop 'R{"one"}=? [ C<4]'
Current working directory: /Users/tim/Desktop

Time for model input parsing: 0.001s.

 WARN (FormulaParserGrammar.cpp:281): Identifier `C' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'C' will not be parsed correctly.
 WARN (FormulaParserGrammar.cpp:281): Identifier `R' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'R' will not be parsed correctly.
Time for model construction: 0.036s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     2
Transitions:    2
Reward Models:  one
State Labels:   2 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": R[exp]{"one"}=? [C<4] ...
Result (for initial states): 3
Time for model checking: 0.000s.

I would leave it like that to make sure that existing prism files using C, R, or whatever as a constant remain valid. IMO, the warning should be enough to make the user aware of this.

As a side note, storm has a couple of operators that are non-standard, like the T operator for expected time (which is afaik not available in PRISM). If those appear in the formula, we give a slightly softer warning

 WARN (FormulaParserGrammar.cpp:282): Identifier `T' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'T' might not be parsed correctly.

and still try to parse formulas containing T as a variable or constant. This is to ensure full compatibility with PRISM models.