порядке, который был сформирован топологической сортировкой.
Такой порядок означает, что при обработке внешних автоматов будут
уже обработаны вложенные в них автоматы (для них будет
подготовлена модель Крипке).
Метод полного графа переходов
Метод, описанный в этом разделе, является наиболее выразительным
в том смысле, что с его помощью можно верифицировать свойства,
охватывающие все качественные аспекты поведения автоматных
программ. Он позволяет работать с автоматами, в которых в общем
случае переходы могут выполняться параллельно. Будем пока
предполагать этот общий случай.
В данном методе множество AP определяется следующим образом:
AP = {Y
1
, Y
2
, …} {e
1
, e
2
, …} {x
1
, x
2
, …} {z
1
, z
2
, …}
{InState, InEvent, InAction} Names.
Здесь {Y
1
, Y
2
, …} – множество наименований для всех состояний
автоматов, {e
1
, e
2
, …} – указанное множество для событий, {x
1
, x
2
, …}
– указанное множество для входных воздействий, {z
1
, z
2
, …} –
указанное множество для выходных воздействий. Names – множество
наименований самих автоматов, а InState, InEvent и InAction –
управляющие атомарные предложения, предназначенные для того,
чтобы было удобно различать вершины, построенные из состояний,
событий и выходных воздействий.
Модель Крипке будем строить по частям: вначале построим те части,
которые соответствуют состояниям автомата (необходимо будет
обработать выходные воздействия и автоматы, вложенные в эти
состояния). Потом добавим в модель информацию о переходах. На
первом шаге положим множество S равным множеству состояний
исходного автомата и для каждого состояния s добавим в отношение
Label две пометки: (s, s) и (s, InState).
После этого для каждого состояния s выполняем следующую
операцию. Пусть s содержит выходные воздействия z
s[1]
, …, z
s[u]
,
которые выполняются при входе в состояние s. Добавим в модель u
состояний {r
1
, …, r
u
} и u переходов r
1
r
2
, …, r
u–1
r
u
, r
u
s.
В отношение Label добавим пометки (r
k
, z
s[k]
), (r
k
, InAction) для всех k
от 1 до u. Далее, при добавлении ребер в модель на следующих
этапах, каждое ребро, которое идет в состояние s, будем
перенаправлять в состояние r
1
.
Пример такого преобразования проиллюстрирован на рис. 4.10.