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

Bug 555 - Incorrect expression for invariants in compiled time-based model
Summary: Incorrect expression for invariants 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-26 23:14 CEST by Wouter Geraedts
Modified: 2013-06-26 23:14 CEST (History)
0 users

See Also:
Architecture:

Attachments
Simple timed UPPAAL model containing an invariant (779 bytes, text/xml)
2013-06-26 23:14 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-26 23:14:28 CEST 
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