This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 432 - wrong verification results when many template instances are used
Summary: wrong verification results when many template instances are used
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.6
Hardware: PC Linux
: P2 major
Assignee: Gerd Behrmann
Depends on:
Reported: 2007-11-19 13:39 CET by Marius Mikučionis
Modified: 2007-11-29 18:13 CET (History)
0 users

See Also:

dining cryptographers model (7.23 KB, text/xml)
2007-11-19 13:39 CET, Marius Mikučionis
queries for dining cryptographers protocol (800 bytes, application/octet-stream)
2007-11-19 13:40 CET, Marius Mikučionis

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2007-11-19 13:39:17 CET
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.
Comment 1 Marius Mikučionis 2007-11-19 13:39:50 CET
Created attachment 200 [details]
dining cryptographers model
Comment 2 Marius Mikučionis 2007-11-19 13:40:23 CET
Created attachment 201 [details]
queries for dining cryptographers protocol
Comment 3 Alexandre David 2007-11-29 18:13:36 CET
The bug was caused by an overflow. This is detected in rev. 3350.