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
Add an attachment (proposed patch, testcase, etc.)

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.