Embed Notice

I guess I'll have to have a separate pair of queues for each client, and have the server non-deterministically choose which one it receives from. That's closer to reality, too.

The nice thing about that is that each queue has its own bound, so checking for 2 empty slots makes sense.

The problem with that is that each queue has its own bound, so state space goes to the mooooon!