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

Bug 386

Summary: segfault when querying for shortest trace
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: major    
Priority: P1    
Version: 4.0.4   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: model with deadlock

Description Marius Mikučionis 2007-01-24 17:47:32 CET 
I have a model. It has a deadlock. Uppaal can find it with "some trace".
However GUI says "connection lost" and verifyta gives segfault when asked 
for the shortest trace to deadlock.
See my model attached.
Comment 1 Marius Mikučionis 2007-01-24 17:48:28 CET 
Created attachment 136 [details]
model with deadlock
Comment 2 Gerd Behrmann 2007-01-25 20:55:30 CET 
Confirmed.
Comment 3 Gerd Behrmann 2007-02-03 14:43:31 CET 
It should be noted, that this is a regression from 4.0.3.
Comment 4 Gerd Behrmann 2007-02-04 11:46:35 CET 
This is a consequence of fixing bug 376. Shortest trace generation adds an expression '#depth += 1' as a post-assignment to the system. Previously, these were ignored in System::stepBack(), but after fixing bug 376, these are included. However, the IncrementMeta expression assumes direct access to the SymbolicState (bypassing the PublicState interface), which obviously fails with stepBack.
Comment 5 Gerd Behrmann 2007-02-04 11:48:30 CET 
BTW: As a consequence of the above mentioned problem, this bug is not limited to deadlock checking. The liveness checker, concrete trace generation, and symbolic pre- and post-stable trace generation are affected as well.
Comment 6 Gerd Behrmann 2007-02-04 12:02:48 CET 
Fixed on the 4.0 branch from rev. 2944.
Comment 7 Gerd Behrmann 2007-02-04 12:08:26 CET 
Was fixed on the trunk in rev. 2837.