Bug 416 - segfault when scalar-indexed processes used with priorities
Summary: segfault when scalar-indexed processes used with priorities
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.6
Hardware: All All
: P1 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2007-04-30 17:27 CEST by Marius Mikučionis
Modified: 2008-04-25 12:19 CEST (History)
0 users

See Also:
Architecture:


Attachments
A sample model to demonstrate a disconnect (server segfault) (1.65 KB, text/xml)
2007-04-30 17:29 CEST, Marius Mikučionis
Details

Note You need to log in before you can comment on or make changes to this bug.
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
Confirmed.
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.