model1 первоначальная

#define N 5

int enter_queue[N] = N; // Запросы на вход
bool on[N];     // Разрешения на вход

int queue_index;

// Макрос для указания готовности КС
inline enter(n)
{
        /* Используется детерминированный шаг для того
         * чтобы избавиться от недерминизма: если процессы переключатся
         * перед сдвигом указателя - будет перетёрта запись от пред. процесса
         */
        d_step {
                enter_queue[queue_index] = n;
                queue_index = (queue_index + 1) % N;
        }
}

active [N] proctype P()
{
        do
        ::
                skip;

entry:          // Готовность зайти в критическуб зону
                enter(_pid);
                on[_pid] -> skip; // Вход в крит. зону

                // Критическая зона
crit:
                skip;

exit:
                // Освобождение критической зоны
                on[_pid] = false;

                // Цикл может прерваться
                if
                :: skip
                :: break
                fi
        od
}

active proctype coordinator()
{
        byte iter; // Итератор по enter_queue
        do
        ::
                /* Просмотр enter_queue можно реализовать по кольцу
                 * чтобы обеспечить FIFO справедливость
                 */

                // Ждём номер процесса в enter_queue
                enter_queue[iter] != N;

                // Получаем номер процесса
                int proc_num = enter_queue[iter];

                // Помечаем использованный элемент очереди
                enter_queue[iter] = N;

                // Допускаем процесс  и ждем, пока освободится
                on[proc_num] = true -> !on[proc_num];

                // Идем к след. запрос
                iter = (iter + 1) % N;
        od
}