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

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