Поведение. Помимо не учитываемых нами процессов размышления и еды, жизнь каждого философа представляет собой повторение цикла из шести событий:

Помимо не учитываемых нами процессов размышления и еды, жизнь каждого философа представляет собой повторение цикла из шести событий:

ФИЛ_i = (i.садится i.берет вил.i i.берет вил.(i +₅ 1)

i.кладет вил.i i.кладет вил.(i +₅ 1) → i.встаёт ФИЛ_i).

Вилку циклически берёт и кладёт на место кто-нибудь из соседних с ней философов:

ВИЛКА_i = (i.берет вил.i, i.кладёт вил.i ВИЛКА_i | (i -₅ 1).берет вил.i

(i -₅ 1).кладёт вил.i ВИЛКА_i).

Поведение всего пансиона можно описать как параллельную комбинацию поведения компонент:

ФИЛОСОФЫ = (ФИЛ₀ || ФИЛ₁ || ФИЛ₂ || ФИЛ₃ || ФИЛ₄ )

ВИЛКИ = (ВИЛКА₀ || ВИЛКА₁ || ВИЛКА₂ || ВИЛКА₃ || ВИЛКА₄ )

ПАНСИОН = (ФИЛОСОФЫ || ВИЛКИ).

В одном из интересных вариантов этой историй философы могут брать и класть обе вилки в любом порядке. Рассмотрим поведение каждой руки философа в отдельности.

aЛЕВАЯ_i = {i.садится, i.встаёт, i.берет вил.i, i.кладёт вил.i}.

aФИЛ_i = {i.садится, i.встаёт, i.берет вил.(i +₅ 1), i.кладёт вил.(i +₅ 1)}.

ЛЕВАЯ_i = (i.садится i.берет вил.i i.кладет вил.i i.встаёт ЛЕВАЯ_i).

ПРАВАЯ_i = (i.садится i.берет вил.(i +₅ 1) i.кладет вил.(i +₅ 1)

i.встаёт ПРАВАЯ_i).

ФИЛ_i = (ЛЕВАЯ_i || ПРАВАЯ_i ).

Синхронизацией процессов ЛЕВАЯ_i и ПРАВАЯ_i в момент, когда i-тый философ садится или встаёт, достигается то, что он не может поднять вилку, если не сидит за столом, и не может встать из-за стола, пока не положит вилку. Помимо этого, операции с обеими вилками произвольно чередуются.

Тупик!

Построенная математическая модель позволяет обнаружить опасность возникновения тупиковой ситуации, когда каждый из философов, сев за стол, возьмёт вилку в левую руку и потянется за второй – которой уже нет на месте. Несмотря на то, что каждый из участников способен к дальнейшим действиям, ни одна пара участников не в состоянии договориться о том, какое действие совершить следующим.

Одним из решений этой проблемы явилось введение в систему слуги. Слуге даётся указание следить за тем, чтобы за столом никогда не оказывалось больше четырех философов одновременно. Алфавит его определяется как C B, где

C = {0.садится, … , 4.садится }, B = {0.встаёт, … , 4.встаёт}.

Поведение слуги проще всего описать с помощью взаимной рекурсии. Пусть СЛУГА_j определяет поведение слуги, когда за столом сидят jфилософов:

СЛУГА₀ =(x: C СЛУГА₁),

СЛУГА_j =(x: C СЛУГА_j+1) | y: B СЛУГА_j-1), для j {1,2.3}.

СЛУГА₄ =(y: B СЛУГА₃).

Пансион, свободный от тупика, определяется как

НОВПАНСИОН = ((ПАНСИОН || СЛУГА₀).