Bug 485

Summary: operator precedence is inconsistent with C++
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: libutapAssignee: Alexandre David <adavid>
Severity: normal    
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: All   
Attachments: model for testing some operator precedence
queries for testing some operator precedence (both modeling and properties)

Description Marius Mikučionis 2010-03-26 10:11:30 CET
I take this page as C++ reference:

In particular the problem is with operator "not" (also "and" and "or") which has very low precedence in Uppaal (see Help and UTAP library source).

For example the following expressions evaluates differently in Uppaal than in C++:
"not(true) && false" is true in Uppaal and false in C++.
The same holds for "not true && false".

We propose to change the precedence of "not" to be the same as "!".
Similarly "and" should have precedence the same as "&&" and "or" like "||".

Also bitwise not "~" would be nice to include for the sake of completeness.
Comment 1 Marius Mikučionis 2010-03-26 12:46:02 CET
Created attachment 230 [details]
model for testing some operator precedence

model for testing some operator precedence
Comment 2 Marius Mikučionis 2010-03-26 12:47:06 CET
Created attachment 231 [details]
queries for testing some operator precedence (both modeling and properties)
Comment 3 Marius Mikučionis 2010-03-26 12:55:18 CET
Fixed precedence of "not", "and" and "or" on trunk in revision 4508.
I suspect there will be more issues, in particular with pre-increment and post-increment (they are treated differently in C++), but I don't see any difference between them in the parser.
Also cannot think of an example for now...

The bitwise not "~" is possible but it creates a mess with ranges and how many bits are used to encode a particular variable, thus it is not going to be implemented. Better use bitwise xor with explicit number of bits.
Comment 4 Alexandre David 2010-05-25 17:03:06 CEST
The fix looks reasonable :).
We can have bit inversion but we would need to check that the range is compatible with the operation, basically lower == -(upper+1).