модель 1 отсутсиве голодания

#define N 5

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

int queue_index;

int entered;

#define p_e P[0]@entry
#define p_c P[0]@crit

// TODO проверить свойство
ltl obligingness { [] ((p_e && [] (entered == 0) -> <> p_c))}
ltl lockout_freedom { [] (p_e -> <>p_c}

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

                enter_queue[queue_index] = n;
                queue_index = (queue_index + 1) % N;
        }
}

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

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

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

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

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

active proctype coordinator()
{
        byte iter; // Итератор по enter_queue
end: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
}