I have a model of dining cryptographers.
Currently it is hopeless that verification could scale with many cryptographers
in the system (due to unexploited ring symmetry), however UPPAAL claims to
verify the problem with 1000 cryptographers in a few seconds, that is something
I did not expect.
The closer look revealed serious correctness problems, like some trivial states
are not reachable when many processes are instantiated, but they are reached
when only a handful is used.
My guess is that there is some kind of buffer overflow problem either with
transition filter (many broadcast synchronization combinations) or template
instantiation.
The UPPAAL version from the trunk suffers the same problems, and in addition it
reports 0 time and 0 memory used, which hints that there are some stability
issues.

Created an attachment (id=200) [details]
dining cryptographers model

Created an attachment (id=201) [details]
queries for dining cryptographers protocol

The bug was caused by an overflow. This is detected in rev. 3350.