Created attachment 262 [details]
Simple timed UPPAAL model containing an invariant
Invariants are not included correctly 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 reports the invariants in the "expressions"-section.
I have attached a simple time-based model with a single process with a single state with the invariant "c <= period", where "c" is a clock and "period" a constant.
In the compiled model the invariant is listed with id "15", which references to the expression "15:2::c". This expression should be something like "15:2,3::c <= period".
Tested with UPPAAL versions 4.1.13, 4.1.14 and 4.1.15. (x86 & amd64 on Linux)