WYSLIJ_DOWOLNY = [(j:1..M) qbuf(j) != 0 -> { jakość != 0 -> element jest w buforze }
                    ile(qbuf(j))--;
                    K(i) ! pbuf(j);
                    (pbuf(j), qbuf(j)) = (0,0)
                 ]

WYSLIJ_JEDEN = [(j:1..M) qbuf(j) == 1 ->
                    ile(1)--;
                    K(i) ! pbuf(j);
                    (pbuf(j), qbuf(j)) = (0,0)
               ]

[MAG :: ile(1..2) :integer; pbuf(1..M) :porcja; qbuf(1..M) :jakosc; czeka :integer
    ile = {0};
    pbuf = {0};
    qbuf = {0};
    czeka = 0;
    *[ile(1) + ile(2) == M -> { bufor pełny }
        [(i:1..K) K(i) ? jakosc(2) ->  {Klient chce 2 i jest w buforze}
            WYSLIJ_DOWOLNY;
        |(i:1..K) ile(1) > 0; K(i) ? jakosc(1) -> { Klient chce 1 i 1 jest w buforze }
            WYSLIJ_JEDEN;
        |(i:1..K) ile(1) == 0; czeka == 0; K(i) ? jakosc(1) ->
            { nie ma 1 w buf i nikt nie czeka }
            czeka = i;
        |(i:1..P) ile(1) == 0; czeka != 0; P(i) ? jakosc(1) ->
            { Ktoś czeka na 1 i jest producent. Połącz ich }
            P(i) ! czeka;
            P(czeka) ! producent(i);
        ]
    |ile(1) + ile(2) < M -> { bufor niepełny }
        [(i:1..P) jak :jakosc; P(i) ? jak -> { Producent pcha towar }
            P(i) ! Ładuj();
            P(i) ? p
            [(k:1..M) qbuf(j) == 0 -> (pbuf(j), qbuf(j)) = (p, jak)]
        |(i:1..K) ile(1) > 0; K(i) ? jakosc(1) ->
            { Klient chce 1 i jest 1 w buforze }
            WYSLIJ_JEDEN;
        |(i:1..K) ile(1) + ile(2) > 0; K(i) ? jakosc(2) ->
            { Klient chce 2 i coś jest }
            WYSLIJ_DOWOLNY;
        ]
    ]
]