Too many enabled transitions in concrete simulator for Uppaal classic model with channel arrays

[magoorden]

Describe the bug A student has worked on a model for the Buzzing Boys / Gossiping Girls problem. With this model we found a discrepancy between the symbolic simulator/verifier and the concrete simulator. The concrete simulator is often enabling or disabling more transitions than the symbolic simulator/verifier, resulting in weird behavior.

The model and one problematic (short) trace can be downloaded here: BuzzingBoys-bug.zip (I have permission from the student to share this model here.)

The included trace results in a deadlock, while the verifier confirms that A[] deadlock imply forall (i:id_b) Boy(i).Idle and Boy(i).secrets == all_secrets holds, i.e., the system only deadlocks if all boys have shared all secrets.

To Reproduce Steps to reproduce the behavior:

1. Open the supplied model.
2. Open the concrete simulator trace and observe the deadlock. (Alternatively, run a random simulation, which will very likely run at some point into a deadlock.)
3. Redo the two steps in the symbolic simulator and observe that the system does not deadlock.

Expected behavior For this classic Uppaal model, the symbolic and concrete simulator should be in agreement with each other.

Version(s) of UPPAAL tested

• UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21
• UPPAAL 5.1.0-beta4 (rev. EB64CC30D74BA740), 2023-11-20
• UPPAAL 5.1.0-beta5 (rev. C7C01B0740E14075), 2023-12-11

Desktop (please complete the following information):

• Versions see above
• OS, Java version: macOS 14.4 (23E214) [and I think the student had a Windows machine, if I remember correctly]