why bounded queues don't play well

[stuarthalloway]

BlockingQueue/BlockingQueuePoisonApple.tla

Line 103 in a064863

\* on the same page that "Poison pills work reliably only with unbounded queues."

I think that this is because of an (unstated?) presumption that producers are unwilling to block forever, so with a bounded queue you would need a PutFail action that loses a poison pill.

Thanks for this tutorial, it has been great fun to work through!

[lemmy]

@stuarthalloway Thanks for the feedback.

Can you please explain your reasoning around a PutFail action? BQPA satisfies the stated liveness constraints. In other words, no producer has to block forever.