Алгоритм побудови дерева досяжності
1. Нехай S = (P1. Pn) гранична вершина дерева (стан мережі Петрі), яка не є тупиковою або дублюючої. Тоді для кожного переходу tj, активованого в S, створюється нова вершина S '= (Pi'. Pn '), в якій стан позицій Рi', i = 1. n, визначається наступним чином:
2. ЯКЩО Pi = So, ТО Р, '= # 969;
3. ЯКЩО на шляху від кореневої вершини до S існує вершина S "= (Р1". Рn "), така що S '> S" (Рi'> Рi "), ТО Рi '= # 969;
4. В іншому випадку значення Рi 'визначається на основі спрацьовування переходу tj зі стану S
5. Вершина S переопределяется як внутрішня, вершина S 'стає граничної. Алгоритм закінчує роботу, коли всі вершини дерева тупикові, дублюючі або внутрішні.
Перевірка властивостей мережі Петрі по дереву досяжності
- Мережа Петрі є обмеженою тоді і тільки тоді, коли в її дереві досяжності відсутня символ # 969 ;. Якщо мережа Петрі обмежена, то по її дереву можна визначити ємність кожної позиції як максимальне значення відповідної компоненти стану мережі. Навіть якщо мережа Петрі не обмежена, то ємність можна визначити для позицій, в яких відсутня # 969 ;.
- Перевірка мережі Петрі на тупикові стану по дереву досяжності не вимагає пояснень (неконечную стану не повинні бути тупиковими).
- Мережа Петрі містить "пастку" тоді, і тільки тоді, коли на її дереві є простий шлях (ланцюжок вершин, в якій з кожної вершини виходить тільки одна дуга), що починається і закінчується дублюючими вершинами і не містить кореневу вершину.
Застосування мереж Петрі для перевірки коректності абстрактного сценарію
Мережа Петрі використовується для виявлення помилок абстрактного сценарію технічних і бізнес-систем. З цією метою сценарій трансформуємо в мережу Петрі і далі перевіряємо властивості мережі. Стосовно до сценарію перевіряються три властивості:
1. Мережа Петрі повинна бути обмеженою;
2. при роботі мережі Петрі не повинні з'являтися неконечную тупикові стану, в яких не активовано жоден перехід;
2. при роботі мережі Петрі не повинно виникати "пасток" - циклів без виходу (об'єкт може потрапити в "пастку", циклічно циркулювати в ній, але не може вийти з "пастки").
Застосування мереж Петрі для перевірки коректності абстрактного сценарію
Перевірка коректності сценарію бізнес-сістемиможет бути
організовано 2 способами:
Сценарій бізнес-сістемибудем вважати коректним. якщо:
- коректні все що утворюють його сценарні модулі
- модулі коректно узгоджені