Buffer.cfg

(download)

SPECIFICATION Prog
CONSTANTS     Producers = {p1,p2,p3}
              Consumers = {c1,c2}
              BufCapacity = 2
              Data = {m1}
INVARIANT     TypeInv
PROPERTY      NoDeadlock