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.
Created attachment 136 [details]
model with deadlock
It should be noted, that this is a regression from 4.0.3.
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.
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.
Fixed on the 4.0 branch from rev. 2944.
Was fixed on the trunk in rev. 2837.