Comment 2 for bug 1339221

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

Fixed,

In short, the bug occurred because the deadlock-check code did not check the invariant of P2 and therefor saw the transition T0 as enabled (even though it was not). The deadlock check was used for the trace-generation.