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.