Формализация WF2M сети на примере алгоритма Кофе-машина и два ученых / Habr

Предлагается WF2M сеть (From workflow to mathematic) с формализмом, обеспечивающим расчет движения маркера по сети workflow [WF2M23]. WF2M сеть основана на ЕРС (Event-Driven Process Chain) – событийная цепочка процессов: последовательность операций, управляемых событиями.

Ранее [CCSWF24] был приведен сценарий «кофе-машина и ученый» - как демонстрация формализма алгебры процессов CCS. Текущий пример формализации WF2M сети дополнен взаимодействием второго учёного, т.е. реализует более сложный сценарий: Кофе-машина и два ученых. Настоящую статью можно считать, как апробацию [WF2M23] на сценарии [CCSWF24].

Сеть WF2M должна решать задачу, которую пыталась решить процессная алгебра (исчисление процессов / теория процессов): формализация алгоритмов workflow, в том числе параллельных и с конкуренцией за ресурс (синхронизация, распределённые, реактивные системы и т.п.). Показан механизм синхронизации в WF2M сети через «антимаркер» – принудительное завершение операции по внешнему сигналу (поглощение маркера антимаркером). Синхронизаторы, вкл. or\ and - join были приведены в [WF2M23] WF2M сеть. Формализм и математика workflow

Один из ключевых подходов в WF2M сети – это упрощение логики переходов вследствие отказа от сложных шлюзов (Exclusive, Inclusive, Parallel Gateway) в пользу вычисления логических условий (событий) в ветвях (дугах графа), т.е. «простая развилка на дуги» + «вычислитель логического выражения \ условия в каждой дуге» (фильтр с одним входом и выходом) вместо одного сложного шлюза (несколько входов \ выходов плюс сложно формализуемая логика их переходов).

1. Матрица смежности WF2M

Простые динамические системы (модели) можно формализовывать дискретной математикой, включая графы и их матрицы смежности\инцидентности\достижимости (переходов). Для формализации сложных динамических систем - workflow, в том числе требующих логику синхронизации потоков, включая or- join, and-join, требуется дополнительная надстройка в виде алгебр процессов, сетей Петри, WF2M и др. Таким образом, для формализации workflow систем (за исключением простейших) недостаточно ни стандартного матричного представления графов, ни булевой алгебры, ни иных элементов дискретной математики.

1.1 Стандартное представление

Матричное представление графов [XOM09]. Ориентированный граф (орграф) из N узлов (i = 1, … N) и M ребер (j = 1, … M). Рассматриваются графы без кратных ребер.

Матрица смежности: матрица NxN, где

a(i,j) = 1, если есть переход от i-го узла (строка матрицы) к j-тому (столбец матрицы), т.е. исходящие от i-го узла связи;

a(i,j) = 0, если i-ый (строка) узел не связан с j-ым (столбец).

Общее правило расчета шага алгоритма (следующего состояния). Смотрим текущую маркировку, например, начальную, см. рис. 2.1. Первая единица {1,0,0 …} говорит, что маркер находится в первом узле. Находим в матрице смежности строку, соответствующую этому узлу (первая строка матрицы). Считываем значения строки и определяем, что на следующем шаге маркер будет размножен и перемещен в узлы р1 и р1'.

1.2 "WF2M - расширение" матрицы смежности

Синхронизатор. a(i,j) может иметь дробное значение, определяющее «вес маркера», например, у оператора and – join для двух входящих ветвей каждая входящая дуга будет иметь вес 1/2. При достижении маркера узла оператора and – join веса узла (текущее значение синхронизатора) и реализованной дуги складываются, при получении после сложения значения «1» маркер («полноценный») переходит в синхронизатор (узел and – join).

Антимаркер. a(i,j) может принимать отрицательное значение. Отрицательные значения «-1» подставляются в вычисляемую ячейку. Если в ячейке была установлена «1» (маркер находится в узле), то 1 + (-1) = 0, т.е. происходит поглощение маркера антимаркером (анти-элемент при взаимодействии с элементом дает 0). Сравнить с типовой ситуацией: в узле нет маркера (значение 0) и на следующем шаге в узел приходит маркер (0 + 1 = 1).

1.3 Вычисления условия в дуге

Для передачи маркера от узла к узлу он осуществляет переход через дугу. Дуга может иметь условие (условный переход), а может не иметь (безусловный). При безусловном переходе условие s равно «1». При условном переходе, если условие s выполняется, то s=1 (маркер передается), если условие s не выполняется, то s=0 и маркер поглощается, подробнее см. [WF2M23].

2. Сценарий Без ограничений на ресурс

2.1 Цикличная процедура. Вариант 1

Состав системы: одна кофе машина и два ученых. Ученые бросают монеты не по очереди, а на конкурентной основе (случайно). Ученые не могут бросать монету одновременно, т.к. кто-то из них на мгновение будет первым, исключение «одномоментности» решается уменьшением шага дискретизации.

Когда один из них бросил (опустил) монету, машина начинает готовить кофе, после чего ученый, оплативший кофе, забирает его. Ученый пьет кофе публикует теорему и снова идет за кофе (бросает монету), т.е. следующую монету кофе машина может приять только после того, как ученый заберет оплаченное кофе. При этом второй ученый может параллельно опускать монету: машина пример монету и начнет параллельно готовить вторую порцию, даже если в это время готовит кофе первому ученому. Это обозначено как «Без ограничений на ресурс», т.е. кофе машина может готовить две порции одновременно.

На рис. 2.1 приведен упрощенный вариант, когда оба ученых пользуются машиной, которая принимает монеты, даже когда готовит кофе, при этом нет конкуренции на опускание монеты и взятие чашки кофе (кто оплатил, тот и берет оплаченный кофе).

Рис. 2.1 Вариант 1

На рис. 2.1 показан сценарий на примере первых трех шагов: t = 0-3. Фактически на схеме через два элемента EPC «event» показан парный XOR, однако формально на схеме про него упоминаний нет, т.е. это мог быть и OR. Логика алгоритма отрабатывается через выражения, заданные в каждом событии [WF2M23]. При необходимости соответствующие ветви алгоритмы и ячейки матрицы могут быть снабжены комментарием «XOR», который может дать указание: дополнительно проверь, что указанные события взаимно исключающиеся или убедись, что сработал только один фильтр (или не сработал никакой).

Иными словами, алгоритм движения маркера не связан с комментарием, но при анализе \ верификации сети мы можем дополнительно проверить обозначенные XOR события на предмет их альтернативности (положительное \ отрицательное число) или события (EPC event) образую «полную группу событий» (по аналогии из теории вероятности, формула полной вероятности), т.е. непременно произойдет одно и только одно из них (число положительное \ отрицательное \ ноль).

2.2 Разовая процедура. Вариант 2

Чтобы показать процесс «с финалом» (классическая WF-net) введем ограничение: когда оба ученых выпили по чашке кофе (т.е. опубликовали по теореме) они направляются обсуждать эти опубликованные теоремы и на этом процесс завершается (событие sEnd). Также в Варианте 2 продемонстрирована формализация синхронизатора and-join: в знаменатель записывается общее число входящих дуг, требующих синхронизацию, например, если в узел «&» входит три дуги, то в знаменателе будет значение 3, а вес входящей дуги: «&»=1/3. Числитель оператора «синхронизатор» and-join суммирует число реализованных переходов в узел синхронизации и при достижении значения 1 переводит маркер последнего реализованного перехода (дуги) в узел синхронизации. Увеличение значения знаменателя производится простым арифметическим сложением текущего нулевого или дробного (если хоть одна ветвь уже была реализована) значения синхронизатора со значением веса вновь реализованной ветви.

Рис. 2.2 Вариант 2

На рис. с Вариантом 2 показан расчет маркировки сети - как продолжение сценария Варианта 1, начиная с шага 4, t=4.

При использовании синхронизатора типа or-join требуется вычисление знаменателя дроби в зависимости от реализации событий, фактически представленных or-split [WF2M23].

2.3 От формализации к формальной верификации workflow

Формализация workflow алгебраическими (не алгоритмическими) методами позволяет дальнейший анализ на базе формальной (математической) верификации.

Тривиальный анализ (примитивная формальная верификация workflow) на примере рис. 2.1 и 2.2 включает: в отличие от Варианта 1, Вариант 2 (sEnd) содержит пустую строку – значит имеется финальное (терминальное типа «end») состояние. Две пустые строки говорят о двух финальных состояниях, если узел одновременно представлен пустой строкой и пустым столбцом, то он не имеет связности (в него ничто не входит и не выходит).

Классическая формальная верификация для workflow хорошо показана на примере сетей Петри (WF-сетей): зацикливания, мертвые точки, свойства безопасности сети, ее живучести (live), бездефектности (soundness) и т.п., см. [Aal97], [Aal10], [BASH13], [BASH09], [Lomaz21], [Deadlock].

Например, о мертвой точке [Fedor13]:

Мертвой точкой модели процесса будем называть логический оператор, который не может сработать ни при каких сочетаниях значений данных процесса, потому что условие никогда не может быть выполнено. Если поток управления достигнет мертвой точки, он остановится и не сможет продвинуться дальше.

Бездефектность сети [BASH14]:

Применяется формальный критерий бездефектности — говорят, что исполнение процесса завершается корректно, если от любой разметки, достижимой от начальной (одна фишка в начальной позиции), достижима финальная (одна фишка в финальной позиции), и при этом в сети по завершении работы не остаётся лишних управляющих фишек.

Ссылки приведены применительно к сетям Петри, но смысл верификации workflow в WF2M тот же: «выявление дефектов логики сети», а сама концепция таких «правильных сетей» имеет длинную историю [Oley82].

3. Сценарий с ограничением на ресурс

3.1 Вариант 3 (без антимаркера)

Если один ученый бросил монету, то ни он ни второй не смогут бросить следующую, пока машина кофе не станет свободна (не разблокируется монетоприемник после завершения приготовления кофе), т.е. снова не войдет в состояние СМ.ready.

На рис. 3.1а показан вариант с конкуренцией за бросок монеты и блокировки монетоприемника машины на время приготовления кофе: пока готовится кофе бросать монету невозможно, т.е. машина не даст сигнал «готов», пока не выдаст чашку с кофе. Как и в примерах ранее: ученому нельзя одновременно бросать монету и пить кофе (рука занята), когда ученый «допил кофе» (опубликовал теорему \ pub), то если активен сигнал (состояние) машины «готов», то может снова бросать монету.

Вариант 3: в функцию броска монеты (p1, p1’) включен механизм контроля состояния внешних систем (состояния СМ, т.е. СМ.ready), вкл. прием соответствующих сигналов от них, поэтому сама функция в зависимости от внешних факторов формирует результирующие события функции, синхронизируемые с внешними факторами (внешними функциями). Механизмы синхронизации реализованы внутри функции p1 и p1’, т.е. синхронизатор представлен неявно. Это один из подходов (упрощений, т.е. сравни Вариант 3 и Вариант 4) в формализации бизнес-процессов, когда механизмы синхронизации «подразумеваются» внутри «черного ящика» под названием «функция», поэтому скрыты от анализа.

Рис. 3.1 Вариант 3 (а) и Вариант 4 (б)

3.2 Вариант 4 (антимаркер)

В варианте 4 показано как реализовать синхронизатор явно. Если убрать дуги «cancel», то реализуется сценарий, когда ученый бросает монету, не глядя на индикатор «готов», однако монета будет принята только когда машина будет в состоянии «СМ свободна». Дуги «cancel» выводят ученого из состояния броска, т.е. говорят, что пока не будет сигнал «готов» бросать монету не нужно.

Анти-маркер

Реализация механизмов синхронизации \ параллелизма кроме синхронных развилок split (fork) и слияний join (merge) [WF2M23] требует операторы принудительного останова уже исполняемых операций. Поэтому вводится специальный маркер «анти-маркер» (cancel), который при передаче в функцию поглощает имеющийся в ней маркер в составе того же хода (расчета сети на текущем шаге дискретизации). При этом вместо стандартного события «p.out» формируется «p.outAnti»:

- фиксируется завершение функции (для вычисления времени выполнения), при этом вычисляется время выполнения операции как разница от момента получения антимаркера до старта операции (р.start);

- маркер поглощается (удален до подхода к выходу из узла, т.е. не попадает в исходящую дугу, как при событии «p.out»).

В таблице переходов «анти-маркер» обозначается знаком «минус», т.е. как требование поглотить маркер (вычесть 1) из узла, где маркер присутствует (=1). На схеме - более тонкой линией и подписью «Cancel». В BPMN по смыслу схож с обработчиком прерывающих Событий со значением атрибута cancelActivity = «true».

Пример ситуации: Не нужно далее собирать заказ клиента (нужно прекратить операцию сбора), если клиент отказался от заказа (при условии, что заказ уже начали собирать, т.е. был реализован p.start).

Применительно к Workflow Patterns это видимо: Шаблон 19 «Отмена задачи» (вариант 2 паттерна). «Видимо» - т.к. странная анимация к этому (wcp19) паттерну.

Считается, что кроме штатного WF-порта каждый WF-узел имеет специальный порт управления (WFs), который принимает \ выдает специальные «управляющие» маркеры. В общем случае, возможны следующие вариации спец-маркера «отмены» применительно к блоку «операция» (EPC function):

прекращение действия: спец-маркер «вышибает» текущий маркер в «конец» (завершение) функции (операции), текущий маркер (обычный) переходит через границу узла и формируется событие «p.out», т.е. маркер выходит из функции через «парадный выход» (т.е. с штатной регистрацией такого выхода);
анти-маркер условный: при попадании в узел при наличии текущего маркера в узле, удаляет его, формируется событие «p.outAnti», т.е. маркер выходит из функции через «черный ход». Если текущего маркера в узле не оказалось (нечего поглощать), то формируется исключение (ошибка, exception);
анти-маркер безусловный: действует, как и «анти-маркер условный», но не формирует сигнал исключения.

Целевые и виртуальные состояния

Обычно в схемах показываются только «целевые действия» (наиболее важные), а «неважные» скрыты. Вариант 4 (рис. 3.1б) содержит такое «неважное» - как виртуальное состояние (узел с пунктирным контуром): ожидания ученых пока готовится кофе.

В бизнес-процессах важен именно приносящий пользу шаг (value, например, идея VAD-диаграмм), в то время как в сетях Петри обычно фиксируются все состояния моделируемого объекта, т.к. без этого не сработает синхронизация (переходы), поэтому необходимо предусматривать различные состояния ожидания. Таким образом, в отличие от сети Петри, WF2M сеть может содержать только «полезные» (важные) пользователю процедуры (состояния), а при необходимости низкоуровневая логика может быть показана через «зашитые» в правила обработки специальных операторов, указанных в матрице переходов. Например, низкоуровневая логика алгоритма также может быть реализована (формализована) на эквивалентном преобразовании в сеть Петри [WF2M23]. Смысл в том, что только часть формализма функционирования системы отображена аналитиком бизнес-процесса на схеме workflow.

Состояния модели

Состояния кофе машины (СМ, Coffee Machine):

ждет и принимает монету (coin), СМ.ready (готов);
готовит и выдает кофе (coffee), СМ.busy (занят).

Состояния (действия, activity) ученого (CS, Computer Scientist, математик):

CS (CS’) бросает монету (СМ вроде освободилась): Попытка опустить монету в машину;
CS (CS’) пьет кофе и публикует: Прием чашки кофе из машины и «Переработка кофе в теоремы» (выпить кофе и опубликовать);
Виртуальное: если не пью кофе (не публикую) - ожидать готовность машины (СМ).

3.3 Синхронность и одновременность

Событие \ условие «Успех. CS» (рис. 3.1, оба варианта) говорит о том, что ученый CS увидел на кофе машине сигнал «готов» бросил монету первым. Этот успешный переход из состояния (операции) p1 (р1’) в р2 можно записать как выполнение условия s, выраженного s1/2:= p1.out and СМ.ready,

что в переводе: маркер покинул узел р1 (монета брошена CS) и машина свободна (готова принять монету), т.е. в нее не попала монета второго ученого (тогда был бы статус СМ.busy), если он тоже бросал монету.

Напомним, что это в CCS (для единственного ученого) [CCSWF24]:

SC1:= coin.SC2 (выдача монеты ученым);

СМ0:= coin.CM1 (прием монеты машиной).

Событие «out» является условием «по умолчанию», поэтому его в блок (надпись) «событие \ условие» не включаем. Таким образом, событие \ условие s1/2 (s1’/2) будет true при завершении операции «p1» (p1.out = true, т.е. маркер на выходе из p1) и (как логическое «И») что машина СМ находится в состоянии ready, т.е. СМ.ready = true.

Таким образом, на низком уровне будет реализована операция XOR, т.к. первый маркер (монета бросившего первым ученого), переключит состояние машины СМ и для следующего маркера (монеты опоздавшего ученого), рассчитываемого в том же такте дискретизации, будет уже СМ.ready = false, т.е. будет реализован первый переход (s1/2) и маркер будет передан на вход операции р2 «Работа СМ», т.е. станет СМ.busy = true.

Физику параллелизма процесса можно представить
следующим образом. После того, как машина выдала кофе, она зажигает индикатор
«готов». Ученые видят сигнал и могут начать кидать монету в соответствии с
функцией распределения (например, один сразу кидает, второй долго думает).

Если один быстро пьет кофе (р3), а второй долго размышляет кидать ли монету (р1’), то получится конкурентная ситуация за бросок монеты.

В таком случае: увидев сигнал готовности (Вариант 4), каждый ученый войдет в состояние «Бросает монету» (Попытка опустить монету, т.к. СМ вроде свободна), т.е. в каждом таком состоянии (р1 и р1’) окажется по маркеру. Далее только один из них окажется удачным, а другой, следовательно, неудачным (опоздавшим). Неудачный исход реализуется Анти-маркером. Время нахождения (пусть и мизерное) в операции с негативным результатом (Бросает монету, т.к. машина вроде бы свободна, но в итоге опоздал) будет учтено моделью, т.е. время нахождения в этом состоянии (например, p1.start) будет учтено, как время начала операции и время получения антимаркера (p1.outAnti).

Заключение

Формализация workflow алгебраическими методами остается на сегодня нерешенной задачей.

Выше был показан формализм workflow матричным способом на примере «разборки» алгоритма «Кофе машина и двое ученых» в сеть WF2M. Этот и подобные сценарии (например, ученый и бедный студент) рассмотрены в [GOL4_18] в контексте функционального программирования и CCS.

Предложенный подход позволяет построение расширенной (WF2M - расширение) матрицы смежности сети WF2M и вычисление по ней маркировки сети на следующем шаге алгоритма.

Формализация WF2M сети предполагает кроме построения по эквивалентному графу матрицы смежности именование узлов и событий и формальное представление условий переходов (дуг с условными переходами, фильтров-событий). Расчет следующего шага алгоритма по текущей маркировке предполагает простые арифметические и логические операции с использованием матрицы смежности (вкл. ее WF2M - расширение).

Ссылки (не все)

[CCSWF24] Алгебры процессов для бизнес-процессов на примере CCS: кофе-машина-теорема

[WF2M23] WF2M сеть. Формализм и математика workflow

[XOM09] Хоменко А.П. Дискретная математика. Часть 3. Элементы теории графов

[GOL4_18] Golovach Courses Smart Contract formal verification: Process Calculus and Modal Logics, on 4 July 2018

Верификация в сетях Петри:

[Aal97] Wil Van der Aalst Verification of Workflow nets

[Aal10] Wil Van der Aalst и др. Soundness of Workflow Nets: Classification, Decidability, and Analysis

springer + References

[BASH13] В. А. Башкин, И. А. Ломазова, О разрешимости бездефектности для сетей потоков работ с неограниченным ресурсом

[BASH14] Башкин В.А. Некоторые методы ресурсного анализа сетей Петри (диссертация дфмн)

[BASH09] Башкин В. А. Модели потоков работ