In the attached system, the model can deadlock in P.bad, which is wrong.
Created attachment 10 [details] Test case
A fix has been checked into CVS.