| Summary: | Incorrect expression for invariants 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 | ||
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) Greetings, Wouter Geraedts