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.
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.