| Summary: | Incorrect layout for invariants with functions in compiled time-based model | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Wouter Geraedts <w.geraedts> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | normal | ||
| Priority: | P5 | ||
| Version: | 4.1.15 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | Simple timed UPPAAL model containing an invariant with a function | ||
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) Greetings, Wouter Geraedts