Bug 416

Summary: segfault when scalar-indexed processes used with priorities
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: normal    
Priority: P1    
Version: 4.0.6   
Hardware: All   
OS: All   
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.
Comment 4 Marius Mikučionis 2019-10-21 10:15:36 CEST
taking over