model 2 исправленная invalid end states

#define N 5 // Количество процессов

/* N каналов для общения координатора с каждым процессом
 *  Можно было бы и сделать 1 канал, просто передавая как второй параметр
 *  номер процесса-получателя
 */
mtype = { OK, FINISH };
chan status[N] = [0] of { mtype };

// Очередь (FIFO) запросов на вход, содержит номер процесса
chan enter = [N] of { int };

active [N] proctype P()
{
        do
        ::
                skip;
entry:
                enter!_pid; // Готовность зайти в критическуб зону
                status[_pid]?OK -> // Вход в крит. зону

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

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

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

active proctype coordinator()
{
        int procN;
end:do
        ::
                enter?procN; // Получаем номер процесса, идущ. в  КС
                // Разрешаем процессу зайти в КС и ждем его завершения
                status[procN]!OK -> status[procN]?FINISH;
        od;
}