модель 1 глобальный ассерт

#define N 5

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

int queue_index;

byte counter;

// Макрос для указания готовности КС
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:	counter++;
		// assert(counter == 1);
		counter--;

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
}

active proctype invariant()
{
	d_step {
		!(counter <= 1) -> assert(counter <= 1)
	}
}