каннибалы и миссионеры

Ответ от Ёерж Неизвесный[гуру]
•ml, mr – количество миссионеров на левом и правом берегу соответственно;
•cl, cr – количество каннибалов на левом и правом берегу соответственно;
•p – положение лодки.
Таким образом, пространство возможных состояний таково:
S = { (ml, mr, cl, cr, p) | ml, mr, cl, cr  {0,1,2,3}, p  { left, right} }
рассмотрим алгебраическую систему, содержащую три универсума:
RiverSide = {left, right} - множество берегов реки;
Number = {0,1,2,3} - возможное количество персонажей одного типа;
Boolean = {true, false, undef} - вспомогательные значения.
Сигнатура включает в себя константы для обозначения элементов универсума; статические функции + и OtherSide с очевидной интерпретацией; и динамические функции:
Cannibals : RiverSide  Number - количество каннибалов на каждом берегу;
Preachers : RiverSide  Number - количество миссионеров на каждом берегу;
BoatPosition : RiverSide - положение лодки.
Начальное состояние соответствует интерпретации:
Cannibals = {left0, right3}, Preachers = {left0, right3}, BoatPosition = right.
В этом случае программа функции перехода выглядит так:
RegularStep()
choose c,p in Numbers where c+p{1,2}
and c  Cannibals(BoatPosition)
and p  Preachers(BoatPosition)
do-in-parallel
BoatPosition := OtherSide(BoatPosition)
Cannibals(BoatPosition) := Cannibals(BoatPosition) – c
Preachers(BoatPosition) := Preachers(BoatPosition) – p
Cannibals(OtherSide(BoatPosition)) := Cannibals(OtherSide(BoatPosition)) + c
Preachers(OtherSide(BoatPosition)) := Preachers(OtherSide(BoatPosition)) + p
enddo
Эта программа соответствует обычному шагу задачи, когда один или два персонажа садятся в лодку и переплывают на противоположный берег. В задаче предусмотрен также и другой тип перехода, когда каннибалы съедают зазевавшихся миссионеров.
WildLunch()
choose side in Side where Cannibals(side)>Preachers(side)
and Preachers(side)>0
Preachers(side) := 0
Три основных этапа построения модели:
Этап 1. Описание пространства возможных состояний системы. Выбирается набор параметров (сигнатура) , значения которых однозначно характеризуют состояние системы.
Этап 2. Указание начального состояния, или, если таких состояний несколько, описание множества состояний, с которых может начинаться вычисление.
Этап 3. Описание функции перехода. Как правило, в модели есть несколько функций перехода, каждая из которых имеет свою область определения и свой набор параметров.
Тогда любое вычисление – это последовательность состояний S0, S1, …, Sn, …, в которой S0 – начальное состояние, а Si+1 получено из Si применением одной из функций перехода.