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
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 or v is the same as using v.
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
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.
Created attachment 7 [details]
Model used in the bug report
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.