This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 556 - Incorrect layout for invariants with functions in compiled time-based model
Summary: Incorrect layout for invariants with functions in compiled time-based model
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.15
Hardware: PC Linux
: P5 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2013-06-27 00:05 CEST by Wouter Geraedts
Modified: 2013-06-27 00:06 CEST (History)
0 users

See Also:
Architecture:

Attachments
Simple timed UPPAAL model containing an invariant with a function (778 bytes, text/xml)
2013-06-27 00:05 CEST, Wouter Geraedts 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Wouter Geraedts 2013-06-27 00:05:56 CEST 
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