LTL-спецификация

Спецификация состоит из двух наборов LTL-формул: для обходов препятствий по часовой стрелке и против часовой стрелки. Агент удовлетворяет спецификации, если он удовлетворяет хотя бы одному набору формул.

Отметим, что создать модель, полностью соответствующую задаче, не удалось. Этому есть несколько причин. Во-первых, поле, по которому передвигается агент, может быть бесконечным. Во-вторых, сохранение даже части поля размером более O(1)в памяти модели делает её слишком большого размера для верификации. Построенная модель не хранит в себе всё поле, и каждый раз, когда агент делает шаг вперёд, недетерминированно генерирует часть поля вокруг агента. Из этого следует, что помимо всех вариантов поля,

которые бывают, верификатор создаёт ещё невозможные случаи. Основными случаями, невозможными в исходной задаче, но встречающимися в модели, являются следующие:

• Изменяющееся поле - если агент сделал шаг вперёд, то информация о трёх клетках, которые были сзади агента, не будет сохранена. При возвращении агента эти клетки будут сгенерированы заново.

• Бесконечно большие препятствия.

• Бесконечно далёкая цель. Для экономии размера модели не хранятся ни координаты агента, ни координаты цели, ни даже расстояние до цели. Хранится только направление на цель и два флага: «находится ли агент в сохранённой клетке» и «ближе ли агент к цели, чем сохранённая клетка». Эти значения каждый ход пересчитываются. В случаях, когда информации не хватает для пересчёта, значения выбираются недетерминированно. Поэтому цель может быть впереди агента на протяжении бесконечного числа шагов.

• «Блуждающая цель».

• «Блуждающая сохранённая клетка». Местоположение сохранённой клетки в модели не хранится. Поэтому оно может измениться так же, как и поле.

Таким образом, LTL-формулы должны быть не только такими, что алгоритм, который им удовлетворяет, является корректным алгоритмом поиска пути, но и такими, чтобы корректные алгоритмы удовлетворяли этим формулам и в невозможных для задачи поиска пути, но возможных для построенной модели, случаях.

Приведём набор LTL-формул для спецификации обходов против часовой стрелки.

Формулы f0 - f3

Группа формул, утверждающих, что в случае, как на рисунке 5.5.1, агент должен сделать шаг вперёд (сонаправленно с текущим направлением), возможно несколько раз повернувшись.

Рисунок 5.5.1. Обход № 1

В листингах 5.5.1 - 5.5.4 приведены формулы из этой группы, смысл которых описывается ниже. Все формулы группы используют макрос o2:

#define o2 ((p.brick[4] == 1) &&(p.brick[2] == 0))

Листинг 5.5.1. Формула f0

#define dt_pos_base_up (o2 && (p.direction == DirUp) &&detourWall &&p.moving)

#define dt_pos_act_up (( ((p.action == Forward && p.direction == DirUp) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable))) && p.moving ) || breakaway)

#define detour_pos_up (dt pos base up -> (dt rot2 U dt pos act up))

ltl f0 {[] detour_pos_up}

Листинг 5.5.2. Формула fl

#define dt_pos_base_right (o2 && (p.direction == DirRight) && detourWall && p.moving)

#define dt_pos_act_right (( ((p.action == Forward && p.direction == DirRight)

|| ((p.action == TargetAchieved) || (p.action == TargetUnreachable))) && p.moving ) || breakaway)

#define detour_pos_right (dt pos base right -> (dt rot2 U dt pos act right))

ltl f1 {[] detour_pos_right}

Листинг 5.5.3.

#define dt_pos_base_down (o2 && (p.direction == DirDown) && detourWall && p.moving)

#define dt_pos_act_down (( ((p.action == Forward && p.direction == DirDown) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable))) && p.moving ) || breakaway)

#define detour_pos_down (dt pos base down -> (dt rot2 U dt pos act down))

ltl f2 {[] detour pos down}

Листинг 5.5.4. Формула f3

#define dt_pos_base_left (o2 && (p.direction == DirLeft) && detourWall && p.moving)

#define dt_pos_act_left (( ((p.action == Forward && p.direction == DirLeft) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable))) && p.moving ) || breakaway)

#define detour_pos_left (dt pos base left -> (dt rot2 U dt pos act left))

ltl f3 {[] detour pos left}

Объясним смысл формулы f0.

o2 == ((p.brick[4] == 1) && (p.brick[2] == 0)): препятствие слева имеется, а спереди нет.

dt_pos_base_up == (o2 && (p.direction == DirUp) &&detourWall &&p.moving) :

выполняется o2, у агента направление вверх, он обходит препятствие, и все действия по пересчёту шага завершены.

dt_rot2 == ( ((p.action == RotLeft) || (p.action == RotRight) || (p.action ==

SavePosition) || (p.action == NoAction)) || !p.moving) : если все действия по

пересчёту шага завершены, то агент либо крутится, либо сохраняет позицию, либо ничего не делает.

dt_pos_act_up == (( ((p.action == Forward &&p.direction == DirUp) ||

((p.action == TargetAchieved) || (p.action == TargetUnreachable))) &&p.moving

) || breakaway) : агент движется вперёд и направлен вверх, либо сообщил, что цель достигнута или не достигнута, либо агент оторвался от препятствия и все действия по пересчёту шага завершены.

detour pos up == (dt pos base up -> (dt rot2 U dt pos act up)): если случилось

dt_pos_base_up, то когда-нибудь выполнится dt_pos_act_up, а до тех пор будет верно dt_rot2.

Таким образом, всегда верно следующее: если слева есть препятствие, а спереди нет, агент направлен вверх и находится в состоянии обхода препятствия и все действия по пересчёту шага завершены, то когда-нибудь

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

Формулы f1- f3аналогичны f0,но утверждают про направления в другие стороны.

Формулы f4 - f7

Данная группа формул утверждает, что в ситуации, как на рисунке 5.5.2, агент должен повернуться направо.

Рисунок 5.5.2. Обход № 2

Формулы из этой группы приведены в листингах 5.5.5 - 5.5.8. Все формулы группы используют макрос o3:

#define o3 ((p.brick[4] == 1) &&(p.brick[2] == 1))

Смысл этих формул описан ниже.

Листинг 5.5.5. Формула f4

#define dt2_pos_base_up (o3 && (p.action != Forward) &&(p.direction == DirUp)

&&detourWall &&p.moving)

#define dt2_pos_act_up ( (p.direction == DirRight) || ((p.action ==

TargetAchieved) || (p.action == TargetUnreachable)) )

#define detour2_pos_up (dt2 pos base up -> (dt rot2 U dt2 pos act up))

ltl f4 {[] detour2_pos_up}

Листинг 5.5.6. Формула f5

#define dt2_pos_base_right (o3 && (p.action != Forward) && (p.direction == DirRight) && detourWall && p.moving)

#define dt2_pos_act_right ( (p.direction == DirDown) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable)) )

#define detour2_pos_right (dt2 pos base right -> (dt rot2 U dt2 pos act right)) ltl f5 {[] detour2 pos right}

Листинг 5.5.7. Формула f6

#define dt2_pos_base_down (o3 && (p.action != Forward) && (p.direction == DirDown) && detourWall && p.moving)

#define dt2_pos_act_down ( (p.direction == DirLeft) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable)) )

#define detour2_pos_down (dt2 pos base down -> (dt rot2 U dt2 pos act down))

ltl f6 {[] detour2 pos down}

Листинг 5.5.8.

#define dt2_pos_base_left (o3 && (p.action != Forward) && (p.direction == DirLeft) && detourWall && p.moving)

#define dt2_pos_act_left ( (p.direction == DirUp) || ((p.action == TargetAchieved) || (p.action == TargetUnreachable)) )

#define detour2_pos_left (dt2 pos base left -> (dt rot2 U dt2 pos act left))

ltl f7 {[] detour2 pos left}

Объясним значение формулы f4.

o3 == ((p.brick[4] == 1) && (p.brick[2] == 1)) : слева и спереди есть

препятствие.

dt2_pos_base_up == (o3 && (p.action != Forward) && (p.direction == DirUp) &&

detourWall && p.moving) : выполняется o3, текущее действие - любое другое действие, отличное от движения вперёд, направление вверх, агент находится в состоянии обхода и все действия по пересчёту шага завершены.

dt2_pos_act_up == ( (p.direction == DirRight) || ((p.action == TargetAchieved)

|| (p.action == TargetUnreachable)) ) : агент направлен вправо или сообщил,

что цель достигнута или недостижима.

detour2_pos_up == (dt2_pos_base_up -> (dt_rot2 U dt2_pos_act_up)) : если случилось dt2_pos_base_up, то когда-нибудь выполнится dt2_pos_act_up, и до тех пор будет верно dt_rot2.

Таким образом, всегда верно следующее: если система (автомат и поле) пришла в такое состояние, что есть препятствие и слева, и спереди, агент

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

Формулы f5- f7аналогичны f4,но утверждают про направления в другие стороны.

Формулы f8 - f11

Данная группа формул утверждает, что если профиль агента как на рисунке 5.5.3 и цель спереди от агента и агент не находится в состоянии обхода, то агент повернёт направо.

Рисунок 5.5.3.

В листингах 5.5.9 -5.5.12 приведены формулы f8- f11.Все формулы группы используют макросы o0 и no obs)

#define o0 ((p.brick[2] == 1) &&IS MOVE FORWARD COOL && (detourWall == false))

#define no_obs (IS_MOVE_FORWARD_COOL && CAN_MOVE_FORWARD)

Листинг 5.5.9. Формула f8

#define dt_begin_base_up (o0 && (p.direction == DirUp) && p.afterMoving)

#define dt_begin_act_up ((p.direction == DirRight) || \

(p.action == TargetUnreachable) || no obs)

#define detour_begin_up (dt begin base up -> (dt rot2 U dt begin act up))

ltl f8 {[] detour begin up}

Листинг 5.1.3.10. Формула f9

#define dt_begin_base_right (o0 && (p.direction == DirRight) && p.afterMoving) #define dt_begin_act_right ((p.direction == DirDown) || \

(p.action == TargetUnreachable) || no_obs)

#define detour_begin_right (dt begin base right -> \

(dt_rot2 U dt_begin_act_right))

ltl f9 {[] detour begin right}

Листинг 5.5.11. Формула f10

#define dt_begin_base_down (o0 && (p.direction == DirDown) && p.afterMoving) #define dt_begin_act_down ((p.direction == DirLeft) || (p.action == TargetUnreachable) || no_obs)

#define detour_begin_down (dt begin base down -> (dt rot2 U dt begin act down)) ltl f10 {[] detour_begin_down}

Листинг 5.5.12. Формула f11

#define dt_begin_base_left (o0 && (p.direction == DirLeft) && p.afterMoving) #define dt_begin_act_left ((p.direction == DirUp) || (p.action == TargetUnreachable) || no_obs)

#define detour_begin_left (dt begin base left -> (dt rot2 U dt begin act left)) ltl f11 {[] detour_begin_left}

Объясним значение формулы f8:

o0 - прямо перед агентом препятствие (нельзя идти вперёд) и движение вперёд приближает к цели и агент не находится в состоянии обхода.

no_obs - движение вперёд приближает к цели и можно двигаться вперёд (перед агентом нет препятствия).

dt_begin_base_up - верно o0 и агент направлен вверх и все действия по пересчёту шага завершены.

dt_begin_act_up - агент направлен вправо или агент сообщает, что цель недостижима или no_obs.

detour_begin_up - если случилось dt_begin_base_up, то в будущем случится dt_begin_act_up, а до тех пор будет верно dt_rot2 (см. описание формулы f0).

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

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

Из изложенного следует, что если агент упирается в препятствие, и цель где-то спереди, то либо он начинает обход, либо он находит направление, которое тоже приближает к цели, либо сообщает о том, что цель недостижима.

Формулы f9- f11аналогичны f8,но утверждают про направления в другие стороны.

Формулы f12- f15

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

Рисунок 5.5.4. Обход № 4

В листингах 5.5.13 - 5.5.16 приведены формулы f12- f15.Все формулы

группы используют макрос o4:

#define o4 ((p.brick[2] == 0) &&(p.brick[1] == 0) &&(p.brick[4] == 1))

Листинг 5.5.13. Формула f12

#define dt3_base_up (o4 &&(p.target != 0) &&(p.direction == DirUp) &&

p.afterMoving &&detourWall && (!(IS MOVE FORWARD COOL && ((InSavedCell &&

!leftSaved) || IS_BETTER_THAN_SAVED))))

#define dt3_act1_up (((p.direction == DirUp) && (p.action == Forward)) | | breakaway)

#define dt3_act2_up (((p.direction == DirLeft) && (p.action == Forward)) || breakaway)

#define detour3_up (dt3_base_up -> ((dt_rot2 U dt3_act1_up) &&(dt3_act1_up -> (dt_rot2 U dt3_act2_up))))

ltl f12 {[] detour3_up}

Листинг 5.5.14. Формула f13

#define dt3_base_right (o4 && (p.target != 0) && (p.direction == DirRight) && p.afterMoving && detourWall && (!(IS_MOVE_FORWARD_COOL && ((InSavedCell && !leftSaved) || IS_BETTER_THAN_SAVED))))

#define dt3_act1_right (((p.direction == DirRight) &&(p.action == Forward)) || breakaway)

#define dt3_act2_right (((p.direction == DirUp) && (p.action == Forward)) || breakaway)

#define detour3_right (dt3_base_right -> ((dt_rot2 U dt3_act1_right) && (dt3_act1_right -> (dt_rot2 U dt3_act2_right)))) ltl f13 {[] detour3 right}

Листинг 5.5.15. Формула f14

#define dt3_base_down (o4 && (p.target != 0) && (p.direction == DirDown) &&

p.afterMoving && detourWall && (!(IS MOVE FORWARD COOL && ((InSavedCell &&

!leftSaved) || IS_BETTER_THAN_SAVED))))

#define dt3_act1_down (((p.direction == DirDown) && (p.action == Forward)) || breakaway)

#define dt3_act2_down (((p.direction == DirRight) && (p.action == Forward)) || breakaway)

#define detour3_down (dt3 base down -> ((dt rot2 U dt3 act1 down) &&

(dt3 act1 down -> (dt rot2 U dt3 act2 down))))

ltl f14 {[] detour3 down}

Листинг 5.5.16. Формула f15

#define dt3_base_left (o4 && (p.target != 0) && (p.direction == DirLeft) &&

p.afterMoving && detourWall && (!(IS MOVE FORWARD COOL && ((InSavedCell &&

!leftSaved) || IS_BETTER_THAN_SAVED))))

#define dt3_act1_left (((p.direction == DirLeft) && (p.action == Forward)) || breakaway)

#define dt3_act2_left (((p.direction == DirDown) && (p.action == Forward)) || breakaway)

#define detour3_left (dt3 base left -> ((dt rot2 U dt3 act1 left) && (dt3_act1_left -> (dt_rot2 U dt3_act2_left))))

ltl f15 {[] detour3 left}

Объясним значение формулы f12:

o4 - слева есть препятствие, а спереди и слева-спереди препятствия нет.

dt3 base up - верно o4, агент не находится в клетке с целью, и направлен вверх, ход завершён, агент находится в состоянии обхода, неверно, что движение вперёд не приближает к цели и либо агент находится ближе к цели, чем сохранённая клетка, либо агент находится в сохранённой клетке и не покидал её с момента сохранения.

dt3_act1_up - агент оторвался от препятствия, либо он направлен вверх и совершает ход вперёд.

dt3_act2_up - агент оторвался от препятствия, либо он направлен влево и совершает ход вперёд.

detour3_up - если условие dt3_base_up выполнено, то в будущем случится dt3_act1_up, а до тех пор будет верно dt_rot2, а затем выполнится dt3_act2_up, а между dt3_act1_up и dt3_act2_up будет верно dt_rot2.

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

Формулы f13- f15аналогичны f12,но утверждают про направления в другие стороны.

Формула f16

Формула f16приведена в листинге 5.5.17.

Листинг 5.5.17. Формула f16

#define notF ((IS AT FINISH == false) &&p.moving)

#define Reach (p.action == TargetAchieved)

#define Unreach (p.action == TargetUnreachable)

#define A ((p.brick[2] == 1))

#define C_up ((p.direction == DirUp) && (p.brick[2] == 0) && ( (p.target == 1)

|| (p.target == 2) || (p.target == 3) ))

#define C_right ((p.direction == DirRight) &&(p.brick[2] == 0) && ( (p.target

== 3) || (p.target == 5) || (p.target == 8) ))

#define C_down ((p.direction == DirDown) && (p.brick[2] == 0) && ( (p.target ==

6) || (p.target == 7) || (p.target == 8) ))

#define C_left ((p.direction == DirLeft) && (p.brick[2] == 0) && ( (p.target ==

1) || (p.target == 4) || (p.target == 6) ))

#define C (C_up || C_right || C_down || C_left)

ltl f16 {[] ((notF && !Reach && !Unreach) ->(((A || C) && p.moving)))}

Объясним формулу f16:

notF: агент еще не достиг цели.

Reach: агент сообщил, что он добрался до цели.

Unreach: агент сообщил, что цель недостижима.

A: впереди препятствие.

C_up: агент направлен вверх, впереди препятствия нет и цель сверху, слева- сверх или справа-сверху (вперёд идти "хорошо").

C_right: аналогично, но направо.

C_down: аналогично, но вниз.

C_left: аналогично, но налево.

c:перед агентом препятствия нет и вперёд идти "хорошо" (шаг вперёд приближает к цели).

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

Формула f17

Эта формула утверждает, что агент не сделает шаг внутрь препятствия. Она приведена в листинге 5.5.18.

Листинг 5.5.18. Формула f17

#define my_rot ( ((p.action == RotLeft) || (p.action == RotRight)) )

ltl f17 {[] ( ((p.brick[2] == 1) &&p.afterMoving) ->

(my_rot V (!(p.moving && (p.action == Forward)))))}

Объясним её значение: my_rot означает, что агент делает поворот направо или налево. Буквой «V» в Spinобозначается темпоральный оператор R (Release).

Таким образом, если прямо впереди агента находится препятствие, то всегда будет верно, что агент не сделает шаг вперёд до тех пор, пока не повернётся.

Формула f18

Эта формула, приведённая в листинге 5.5.19, утверждает, что если агент достиг цели, то он когда-нибудь выполнит действие «report reached».

Листинг 5.5.19. Формула f18

ltl f18 {[] (IS AT FINISH -> ((p.action == TargetAchieved)))}

Формулы f19 - f26

Эти формулы, приведённые в листинге 5.5.20, утверждают, что агент будет идти прямо к цели всегда, когда алгоритм BUG-2этого требует.

Листинг 5.5.20. Формулы f19 - f26

#define ActUp ((p.direction == DirUp) &&(p.action == Forward))

#define ActRight ((p.direction == DirRight) && (p.action == Forward))

#define ActDown ((p.direction == DirDown) && (p.action == Forward))

#define ActLeft ((p.direction == DirLeft) && (p.action == Forward))

#define NotGoUp ((!p.moving) || (!ActUp))

#define NotGoDown ((!p.moving) || (!ActDown))

#define NotGoLeft ((!p.moving) || (!ActLeft))

#define NotGoRight ((!p.moving) || (!ActRight))

ltl f19 {[] (((p.target == 1) &&(p.brick[2]\

!= 0) &&!ActDown &&!Reached &&\

p.afterMoving) -> ((NotGoDown && NotGoRight)\ U ((p. action == TargetUnreachable) || ActUp\

|| ActLeft || detourWall)))}

ltl f20 {[] (((p.target == 2) && (p.brick[2]\

!= 0) && !ActDown && !Reached &&\

p.afterMoving) -> (NotGoDown U ((p.action ==\ TargetUnreachable) || ActUp || detourWall)))}

ltl f21 {[] (((p.target == 3) && (p.brick[2]!=0)\

&& !ActDown && !Reached && p.afterMoving) ->\ ((NotGoDown && NotGoLeft) U ((p.action ==\ TargetUnreachable) || ActUp || ActRight ||\ detourWall)))}

ltl f22 {[] (((p.target == 4) && (p.brick[2]!=0)\

&& !ActRight && !Reached && p.afterMoving)->\ (NotGoRight U ((p.action==TargetUnreachable)\ || ActLeft || detourWall)) )}

ltl f23 {[] (((p.target == 5) && (p.brick[2]!=0)\

&& !ActLeft && !Reached && p.afterMoving) ->\ (NotGoLeft U ((p.action==TargetUnreachable)\ || ActRight || detourWall)) )}

ltl f24 {[] (((p.target == 6) && (p.brick[2]!=0)\

&& !ActUp && !ActRight && !Reached &&\ p.afterMoving) -> ((NotGoUp && NotGoRight) U\ ((p.action==TargetUnreachable) || ActDown ||\ ActLeft || detourWall)))}

ltl f25 {[] (((p.target==7) &&(p.brick[2]!=0)&&\

!ActUp&&!Reached&&p.afterMoving) -> (NotGoUp\

U ((p. action == TargetUnreachable)\

|| ActDown || detourWall)) )}

ltl f26 {[] (((p.target == 8) && (p.brick[2]\

!= 0) && !ActUp && !ActLeft && !Reached &&

p.afterMoving) -> ((NotGoUp && NotGoLeft) U\

((p.action == TargetUnreachable) || ActDown\

|| ActRight || detourWall)))}

Объясним формулу f19:

ActDown: агент направлен вниз и его текущее действие - движение вперёд (агент движется вниз).

NotGoDown: или действия по пересчёту хода агента не закончились, или он не движется вниз.

ActRight: агент движется направо.

NotGoRight: или действия по пересчёту хода агента не закончились, или он не движется направо.

Таким образом, всегда верно следующее: если цель сверху-слева, цель не достигнута и агент не движется вниз, то когда-нибудь или агент сообщит о недостижимости цели или входит наверх или сходит налево или начнёт обход, а до этого будет верно, что агент не движется вниз и не движется вправо.

Остальные формулы аналогичны f19,но про другие направления пеленга на цель.

Формула f27

Эта формула означает, что агент может сохранять свою позицию только если он находится в сохранённой клетке, либо ближе к цели, чем сохранённая клетка. Она приведена в листинге 5.5.21.

Листинг 5.5.21. Формула f27

ltl f27 {[] ((p.action == SavePosition) ->

(InSavedCell || IS_BETTER_THAN_SAVED))}

Формула f28

Эта формула означает, что всегда будет верно следующее: если агент никогда не достигнет цели, то обязательно случится один из вариантов:

• агент сообщит о том, что цель недостижима;

• агент будет бесконечно много раз сохранять позицию и бесконечно много раз выходить из сохранённой клетки (следовательно, будет идти в сторону бесконечно далёкой цели);

• всегда будет верно, что если он идёт вперёд, то это движение его приближает к цели;

• с некоторого места он будет бесконечно долго в состоянии обхода и никогда попадёт в ранее сохранённую клетку.

Она приведена в листинге 5.5.22.

Листинг 5.5.22. Формула f28

ltl f28 {[] ((!((p.target == 0))) ->((p.action == TargetUnreachable) ||\ (([] (p.action == SavePosition))&& ([] !InSavedCell)) || \

([]((p.action == Forward) -> IS_MOVE_FORWARD_COOL)) || \

([](detourWall &&!InSavedCell))))}

Формула f29

Формула f29означает, что если агент находится ближе к цели, чем сохранённая клетка, то он либо достигнет цели, либо сохранит позицию ближе, чем сохранённая клетка. Она приведена в листинге 5.5.23.

Листинг 5.5.23. Формула f29

ltl f29 {[] (IS_BETTER_THAN_SAVED ->

((p.action==TargetAchieved) || ((p.action

== SavePosition)&&(IS_BETTER_THAN_SAVED))))}

Формула f30

Эта формула означает, что если агент выполнил действие «report reached», то он действительно достиг цели. Она приведена в листинге 5.5.23. Листинг 5.5.23. Формула f30

ltl f30 {[] ((p.action == TargetAchieved) -> Reached)}

5.6.