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.
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.