Иерархический метод анализа функционирования программного обеспечения
7
последовательности переходов. Сеть Петри может иметь бесконечное
дерево достижимости. Для получения дерева, которое можно считать
полезным инструментом анализа, необходимо найти средства огра-
ничения его до конечного размера.
Особенностью алгоритма построения конечного дерева достижи-
мости является специальная классификация маркировок. Каждая вер-
шина дерева классифицируется как граничная, терминальная, дубли-
рующая или внутренняя вершина. Граничными являются вершины,
которые еще не обработаны алгоритмом. После обработки граничные
вершины становятся либо терминальными, либо дублирующими, либо
внутренними. Маркировки, в которых нет разрешенных переходов,
являются терминальными вершинами дерева достижимости. Другой
класс маркировок — это маркировки, ранее встречавшиеся в дереве.
Они называются дублирующими вершинами. Никакие последующие
маркировки рассматривать не нужно, так как все они будут порожде-
ны из места первого появления дублирующей маркировки в дереве.
Для сведения дерева достижимости к конечному представлению
используется еще одно средство. Для позиций, которые увеличивают
число фишек некоторой последовательностью запусков переходов,
можно создать произвольно большое число фишек, просто повторяя
данную последовательность столько раз, сколько это нужно. Беско-
нечное число маркировок, получающихся из циклов такого типа,
представляется с помощью специального символа
w
, который обо-
значает «бесконечность». Таким образом, в маркировке число фишек
может быть неотрицательным целым либо
w.
Первый шаг алгоритма определяет начальную маркировку кор-
нем дерева, т.е. граничной вершиной. Последующие шаги направле-
ны на обработку граничных вершин. До тех пор, пока имеются гра-
ничные вершины, они обрабатываются алгоритмом.
Пусть
х —
граничная вершина, которую необходимо обработать.
1. Если в дереве имеется другая вершина
у
, не являющаяся гра-
ничной, и с ней связана та же маркировка (
μ
[
х
] =
μ
[
у
]), то вершина
х
—
дублирующая.
2. Если для маркировки
μ
[
x
] ни один из переходов не разрешен
(т. е.
δ
(
μ
[
x
],
t
j
]) не определено для всех
t
j
∈
Т
,
δ
(
μ
[
x
],
t
j
]) —
функция
следующего состояния), то
х
— терминальная вершина.
3. Для всякого перехода
t
j
∈
T
, разрешенного в
μ
[
x
] (т.е.
δ
(
μ
[
x
],
t
j
)
определено), создать новую вершину
z
дерева достижимости. Марки-
ровка
μ
[
z
], связанная с этой вершиной, определяется для каждой по-
зиции
p
i
следующим образом:
– если
μ
[
x
]
i
=
w
, то
μ
[
z
]
i
=
w
;
– если на пути от корневой вершины к
х
существует вершина
у
с
μ
[
у
] <
δ
(
μ
[
x
],
t
j
) и
μ
[
y
]
i
<
δ
(
μ
[
x
],
t
j
)
i
, то
μ
[
z
]
i
=
w
;
– в противном случае
μ
[
z
]
i
=
δ
(
μ
[
х
],
t
j
)
i
.
