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

Bug 60

Summary: Problem with arrays of booleans
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: critical CC: furang
Priority: P2    
Version: 3.4.0   
Hardware: All   
OS: All   
Architecture:
Attachments: Model used in the bug report

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.