BlockingQueuePoisonPill.cfg

CONSTANTS
    BufCapacity = 7
    Producers = {p1,p2,p3}
    Consumers = {c1,c2,c3}
    Poison = Poison

SPECIFICATION Spec

INVARIANT TypeInv

INVARIANT NoDeadlock

INVARIANT QueueEmpty

PROPERTIES GlobalTermination

\* BQSpec no longer holds with BQPP rewritten with a poor-mans ConstInit.
\* PROPERTIES BQSpec