Построение модели

Второй шаг состоит в построении модели и спецификации.

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

• текущее действие;

• последнее совершённое действие;

• направление;

• соседние клетки;

• направление на цель;

• флаг, который определяет, обходит ли агент в данный момент препятствие;

• специальные флаги для обеспечения атомарности перехода из одного состояния всей системы в другое.

В листинге 5.4.1 приведена реализация профиля на языке Promela.

Листинг 5.4.1. Профиль агента

typedef Profile

{

unsigned action : 3;//текущее действие

unsigned lastAction : 3;//последнее действие unsigned direction : 2;//направление bit brick[9];//соседние клетки

unsigned target : 4; //направление на цель bool moving;

bool afterMoving;

Предикат moving означает, что все действия по пересчёту хода агента завершены. Мы считаем, что пока moving = true и action ≠ NoAction, агент совершает свой ход.

Предикат afterMoving означает, что ход агента закончен. При этом action = NoAction.

В модели хранится текущий профиль и профиль последнего сохранения агентом своего состояния.

Также в модель входят конечный автомат системы управления агентом и внешняя среда, в которой находится агент. Профиль, внешняя среда и LTL-формулы были написаны вручную. Во всех моделях эти части являются одинаковыми. Модели различаются только той частью, которая эквивалентна конечному автомату. В дальнейшем, слово «модель» будет относиться ко всем построенным моделям, если это не оговорено иначе. Эта часть была сгенерирована при помощи инструментального средства Stater.

5.5.