Created attachment 263 [details]
Simple timed UPPAAL model containing an invariant with a function
Invariants with functions result in an incorrect layout in the compiled version of a time-based model.
When compiling a model with:
$ UPPAAL_COMPILE_ONLY=1 ./verifyta <model>.xml
The resulting compiled model incorrectly represents the relevant location with such an invariant as a static element.
I have attached a simple time-based model with a single process with a single state with the invariant "c <= f()", where "c" is a clock and "f" a function returning a constant.
In the compiled model the location is listed with id "7", which references to the layout element "7:static:-32767:32767:return return value". This layout element should be something like "7:location::_id0".
Tested with UPPAAL versions 4.1.13, 4.1.14 and 4.1.15. (x86 & amd64 on Linux)