Bug 60 - Problem with arrays of booleans
Summary: Problem with arrays of booleans
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.0
Hardware: All All
: P2 critical
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2003-09-17 08:39 CEST by Gerd Behrmann
Modified: 2003-09-22 16:32 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments
Model used in the bug report (1.08 KB, application/octet-stream)
2003-09-17 08:39 CEST, Gerd Behrmann
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Gerd Behrmann 2003-09-17 08:39:01 CEST
I think we've found a bug in uppal version 3.4.0.

It seems that this version of Uppaal doesn't correctly handle arrays of
boolean. 
Passing array elements as parameter of a template result that
each reference to an array element is equivalent to a refenrence
to the first element, i.e. using v[0] or v[1] is the same as using v[0].

It seems that this bug involves both simulator and verifier.

The attached project models four identical concurrent activities
executing a critical section. Each process tries to acquire a lock by
testing the value of a boolean variable and setting it to true and, in a
subsequent step, sets it to false releasing the lock. Each couple of
processes share a boolean varable representing the lock.

The model works well if two distinct global boolean variables are used
as
parameters of the template. If one uses (as in the attached project) an
array of two booleans  both simulator and verifier don't work correctly.
Comment 1 Gerd Behrmann 2003-09-17 08:39:43 CEST
Created attachment 7 [details]
Model used in the bug report
Comment 2 Gerd Behrmann 2003-09-17 09:07:03 CEST
A fix has been checked into CVS. 

The problem was that the type checker didn't know about the size of a boolean
and thus computed it as zero. Since the offset into the array is computed as idx
* element_size, and element_size due to the bug was 0, this would always result
in the first element of the array being addressed.