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

Bug 386 - segfault when querying for shortest trace
Summary: segfault when querying for shortest trace
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.4
Hardware: PC Linux
: P1 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2007-01-24 17:47 CET by Marius Mikučionis
Modified: 2007-02-04 12:08 CET (History)
0 users

See Also:
Architecture:


Attachments
model with deadlock (21.93 KB, text/xml)
2007-01-24 17:48 CET, 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-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.