Bug 555

Summary: Incorrect expression for invariants in compiled time-based model
Product: UPPAAL Reporter: Wouter Geraedts <w.geraedts>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: normal    
Priority: P5    
Version: 4.1.15   
Hardware: PC   
OS: Linux   
Attachments: Simple timed UPPAAL model containing an invariant

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)

Wouter Geraedts