Описание автоматной модели

В методе используется параллельная система взаимодействующих иерархических конечных автоматов [41 -45]. Под иерархическим автоматом в данной работе понимается система вложенных автоматов.

3.1.1. Математическая модель управляющего автомата

Каждый автомат - это кортежгде:

• S - конечное множество состояний;

• s₀- начальное состояние;

• - множество допускающих состояний (возможно, пустое);

• E - множество входных воздействий (событий);

• X- множество переменных;

• Z - множество выходных воздействий;

• B- множество логических функций от переменных из множества X

(условий на переменные из множества X);

• δ: S ? E ? B→ S - отношение переходов;

• - отношение выходных воздействий.

Каждое множество одинаковых автоматов назовём автоматным типом.

Множество Zсостоит из двух множеств Z₁и Z₂. Первое из них - это множество выходных воздействий, которые состоят из имён вызываемых подпрограмм. Множество Z2 состоит из выходных воздействий, которые состоят из произвольного программного кода. В модель на языке Promelaэтот код переносится без изменений.

Переходы автоматов выполняются по событиям. На переходах могут быть также и охранные условия [77]. Однако что делать, если в автомат пришло событие, по которому нет перехода? Традиционно в теории языков и вычислений детерминированный конечный автомат в таком случае переходит в недопускающее состояние, но такое поведение не всегда удобно.

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

• при появлении события, по которому нет перехода, автомат переходит в недопускающее состояние;

• при появлении события, по которому нет перехода, оно игнорируется (добавляются пустые петли по всем таким событиям).

Автомат может иметь конечное число переменных целочисленных типов (включая массивы). Эти переменные могут иметь следующие модификаторы:

• volatile - переменная может быть использована в любом месте программы.

• external - переменная может быть использована другим автоматом.

• param - переменная является параметром автомата.

По умолчанию считается, что переменная не используется нигде, кроме как на диаграмме переходов автомата.

Все события являются общими для всей системы автоматов.

Выходные воздействия автомата бывают двух типов:

1. На переходах и в состояниях может быть выполнен любой код.

2. Запуск на переходе, а также при входе в состояние и при выходе из него, функций на целевом языке программирования, определяемых пользователем после того, как сгенерирован код.

3.1.2. Математическая модель вложенных автоматов

Рассмотрим автомат типа A_i.Пусть S_a- множество его состояний. Пусть M- множество автоматов в системе. Определим отношение вложенности как множество отношений V: {v_l| v_l: S_a. → M}.

Отметим, что автомат может иметь вложенные автоматы любого типа, кроме собственного, так как иначе будет бесконечная рекурсия. Циклическая рекурсия также запрещена.

3.1.3. Математическая модель параллельно работающих автоматов

Модель для параллельно работающих автоматов - это тройка , где

• множество отношений, описывающих запуск автоматов;

• - множество отношений, описывающих коммуникацию между автоматами;

• - множество отношений, описывающих совместно используемые переменные.

При реализации параллельных автоматов каждый автомат будем реализовывать в своём потоке.

Автомат может запускать поток с новым автоматом любого типа. Задаётся тип автомата и имя . Нельзя запускать несколько автоматов с одним именем, а также запускать автоматы своего типа.

Автомат может взаимодействовать с другим автоматом, выступая источником событий для него. События отправляются асинхронно.

Автомат может также использовать отмеченные специальным модификатором переменные другого автомата.

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

3.2.