|Summary:||segfault when querying for shortest trace|
|Product:||UPPAAL||Reporter:||Marius Mikučionis <marius>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
|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
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.