|Summary:||segfault when scalar-indexed processes used with priorities|
|Product:||UPPAAL||Reporter:||Marius Mikučionis <marius>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
|Attachments:||A sample model to demonstrate a disconnect (server segfault)|
Description Marius Mikučionis 2007-04-30 17:27:04 CEST
Something is wrong with priorities code, Uppaal does not like mixing scalars and priorities. Perhaps some wrong assumptions are made in counting the symmetric processes?
Comment 1 Marius Mikučionis 2007-04-30 17:29:11 CEST
Created attachment 152 [details] A sample model to demonstrate a disconnect (server segfault) Uppaal segfaults in a few steps of state exploration with the model attached.
Comment 2 Gerd Behrmann 2007-05-13 17:57:00 CEST
Comment 3 Marius Mikučionis 2008-04-25 12:19:55 CEST
I am not sure if it's the same problem, but the following declaration alone gives segfault: meta int i; chan c1, c2, c3; chan priority c1, c2 < c3; I looked at the coredump: it seems that system builder gets a reference to i when it tries to access c1, then it tries to evaluate this variable expression on null state and surely segfaults (value of i depends on state, whereas channel value is something else). Hairy stuff.