В начальной маркировке (1, 0, 0) разрешены два перехода t1 и t2. Первый шаг построения дерева достижимости показан на рис (б). Из маркировки (1, 1, 0) можно снова запустить t1 (получая (1, 2, 0)) и t2 (получая (0, 2, 1)); из (0, 1, 1) можно запустить t3 (получая (0, 0, 1)). Второй шаг построения дерева достижимости показан на рис (в).
Продолжая три маркировки (рис (в)) на третьем шаге маркировки (рис (г)). Маркировка (0, 0, 1) пассивная: никакой переход в ней не разрешен. Маркировка (0, 1, 1), порождаемая запуском t3 в (0, 2, 1) была уже порождена непосредственно из начальной маркировки запуском t2.
Если эту процедуру повторять снова и снова, каждая достижимая маркировка окажется порожденной, а полученное дерево может оказаться бесконечным.
Всякий путь в дереве, начинающийся в корне соответствует допустимой последовательности переходов.
Для превращения дерева в полезный инструмент анализа необходимо найти средства ограничения его до конечного размера. Приведение к конечному представлению осуществляется двумя операциями.
Первая из них – это использование пассивных маркировок, именуемых терминальными вершинами, и маркировок, ранее встречавшихся в дереве, именуемых дублирующими вершинами. В нашем примере маркировка (0, 0, 1) – терминальная, а (0, 1, 1) – дублирующая.
Вторая операция. Рассмотрим последовательность запусков переходов s, начинающуюся в начальной маркировке М0 и концом M’, M’>M0. Маркировка M’ совпадает с маркировкой М0, за исключением того, что имеет некоторые «дополнительные» метки в некоторых позициях, то есть M’=M0+(M’-M0) и (M’-M0)>0. Поскольку на запуски переходов дополнительные метки не влияют, последовательность s можно запустить снова, начиная в M’, приходя к маркировке M”. Так как действие последовательности переходов s добавило M’-M0 меток к маркировке M0, она добавит также M’-M0 меток к маркировке M’, поэтому M”=M’+(M’-M0) или M”=M0+2(M’-M0). В общем случае последовательность s можно запустить n раз, получив в результате маркировку M0+n(M’-M0).
В нашем примере можно запустить переход t1 столько раз сколько необходимо для того, чтобы получить произвольное число меток в P2. Это бесконечное число маркировок обозначим символом w. Для любого a определим
w+а=w, w-а=w, а<w, w£w
Эти операции с символом w достаточны для построения дерева.
Алгоритм построения дерева.Каждая вершина i дерева связывается с расширенной маркировкой M(i). В этой маркировке число меток в позиции может быть либо неотрицательным целым, либо w. Каждая вершина классифицируется как граничная или терминальная или дублирующая или внутренняя.
Граничными являются вершины, которые не обработаны алгоритмом. Алгоритм превратит их в терминальные, дублирующие, внутренние.
Алгоритм начинает с начальной маркировки М0, принимая ее в качестве граничной вершины.
Пусть х – граничная вершина.
1. Если в дереве имеется другая вершина у, не являющаяся граничной, и с ней связана также маркировка М(х)=М(у), то вершина х – дублирующая.
2. Если для маркировки М(х) ни один из переходов не разрешен для всех tjÎT, то х – терминальная вершина.
3. Для всякого перехода tjÎT, разрешенного в М(х), создать новую вершину z дерева. Маркировка М(z) определяется для каждой позиции Pi следующим образом:
а) если М(х)i=w, то М(z)i=w.
б) если на пути от корневой вершины к х существует вершина у с М(у)<d(M(x), tj) и М(у)i<d(M(x), tj)i, то М(z)i=w, d - функция следующего состояния.
в) в противном случае М(z)i=d(M(x), tj)i,
Функция d(M(x), tj) не определена, если tj не разрешен в маркировке М(х). Если tj разрешен, то d(M(x), tj)=M’(x), где M’(x) – маркировка, полученная после срабатывания tj. Дуга, помеченная tj, направлена от вершины х к вершине z. Вершина х переопределяется как внутренняя, вершина z становится граничной.
Когда все вершины дерева – терминальные, дублирующие или внутренние, алгоритм останавливается.
Для нашего примера дерево достижимости имеет вид:
Имеется доказательство того, что алгоритм конечный и не может создавать новые граничные вершины бесконечно.
Ниже на рис. 5.15 приведем еще один пример сети Петри и дерево достижимости для него.
Рис 5.15. Пример дерева достижимости
Анализ сетей Петри на основе дерева достижимости.Сеть Петри ограничена тогда и только тогда, когда символ w отсутствует в ее дереве достижимости. Если сеть ограничена и символ w отсутствует в дереве достижимости, то сеть представляет систему конечных состояний. Это позволяет решить вопросы анализа простым перебором и проверкой конечного множества всех достижимых маркировок.
Сеть Петри является сохраняющей, если она не теряет и не порождает метки, а просто передвигает их. Свойство сохранения проверяется по дереву достижимости вычислением для каждой маркировки суммы меток. Если метки взвешены, то вычисляется взвешенная сумма. Если сумма одинакова для каждой достижимой маркировки, сеть - сохраняющая.
Задача покрываемости маркировки М маркировкой М’ сводится к поиску на дереве такой вершины х, состояние которой покрывает состояние М. Если такой вершины М(х) не существует, маркировка М не покрывается никакой достижимой маркировкой.
Таким образом, дерево достижимости можно использовать для решения задач безопасности, ограниченности, сохранения и покрываемости. К сожалению, в общем случае его нельзя использовать для решения задач достижимости и активности, а также для определения возможной последовательности запусков. Решение этих задач ограничено существованием символа w. Символ w означает потерю информации, конкретные количества меток отбрасываются, учитывается только существование их большого числа. Вместе с тем, в отдельных конкретных случаях дерево достижимости позволяет судить о свойствах достижимости и активности. Например, сеть, дерево достижимости которой содержит терминальную вершину, не активна. Аналогично искомая маркировка M’ в задаче достижимости может встретиться в дереве достижимости, что означает ее достижимость. Кроме того, если маркировка не покрывается некоторой вершиной дерева достижимости, то она недостижима.
