A debug configuration with 2 producers, 1 consumer, and buffer capacity 1.

What Changed

Upstream v04 adds an interactive debugger using TLCExt!PickSuccessor in BlockingQueueDebug.tla. Its debug configuration is p2c1b1. The playground uses those same constants with the base BlockingQueue spec, without the desktop-only interactive action constraint.

The upstream debugger lets us explore both deadlock states for p2c1b1:

To reproduce the debugger rather than the browser run, use the linked upstream revision's BlockingQueueDebug.tla/.cfg and the CommunityModules library containing TLCExt.

Expected Result

The browser reports Deadlock reached and stops at the first deadlock. Unlike the recording, it does not prompt you to choose a successor. Try returning to p1c1b1 to see the deadlock disappear.