Логический вывод на графе реконсиляции
Обсудим метод, использующий графическую нотацию для графа реконсиляции на Рис. 5. Вершины графа изображены окружностями и помечены символами операций. Каждая вершина располагается в одной из областей, соответствующих исходным транзакциям и, возможно, применяемой корректирующей транзакции. На диаграмме области исходных транзакций располагаются на противоположных сторонах и отделяются от центральной области корректирующей транзакции двумя вертикальными линиями. В случаях, если коррекция отсутствует, на диаграмме размещаются лишь области исходных транзакций, отделенные друг от друга одной вертикальной линией.
Бинарные отношения зависимости между операциями изображаются дугами, помеченными упорядоченными парами черных и/или белых кружков, бинарные отношения предшествования - стрелками. Строгие отношения зависимости представляются сплошными дугами, а нестрогие отношения - пунктирными дугами. Строгие отношения предшествования заканчиваются темными стрелками, а нестрогие отношения предшествования заканчиваются светлыми стрелками. При использовании некоторых визуальных элементов метода полисиллогистического вывода [] графическая нотация обеспечивает прозрачную и непротиворечивую интерпретацию обсуждаемой задачи. Для представления множественных отношений зависимости и порядка могут быть добавлены необходимые визуальные элементы, соответствующие ребрам соответствующего гиперграфа реконсиляции. На Рис. 6 приведен пример графа реконсиляции для рассмотренных выше транзакций.
Рис. 5.Графическая нотация элементов графа реконсиляции.
Опишем предлагаемый метод логического вывода, используя представленную графическую нотацию. Для выделения цепей зависимости и определения того, какие вершины могут зависеть от заданной вершины, удобно использовать следующее визуальное правило. Заметим, что цепями зависимости в графе реконсиляции являются только те цепи, ребра которых инцидентны общим вершинам с чередующимися цветами кружков. Это объясняется тем, что пара цветов, присваиваемая отношению импликации, соответствует запрещенной комбинации статусов операций, при этом черный цвет обозначает статус включения, а белый - исключения.
Таким образом, чередование цветов в инцидентных ребрах порождает цепочки логического вывода и соответствующие зависимости.
Рис. 6. Пример графа реконсиляции.
Общая схема метода вывода представляется следующими этапами.
На первом этапе все операции исходных транзакций объединяются в один временный журнал.
На втором этапе проводится поиск циклов прямой зависимости. Вершины найденных циклов формируют классы эквивалентности для операций, или, другими словами, множества операций, которые включаются в итоговую транзакцию только совместно. Таким образом, осуществляется декомпозиция транзакций на семантически связанные группы операций. В конечном итоге это приводит к снижению числа независимых переменных в решаемой логической системе, поскольку статус любой из вершин цикла однозначно определяет состояния всех остальных вершин.
На третьем этапе выявляются подобные цепи - логически эквивалентные цепи зависимости, начинающиеся и заканчивающиеся в одних и тех же вершинах графа. В результате проводимой редукции логической системы из анализа исключаются избыточные отношения и зависимые переменные, связанные с внутренними вершинами подобных цепей.
На заключительном этапе проводится поиск вершин, порождающих конфликты. Это вершины, инцидентные ребрам обратной зависимости, а также вершины, образующие циклы предшествования. Согласно применяемым политикам реконсиляции и решениям пользователя, операции, соответствующие конфликтным вершинам, последовательно удаляются из журнала. Вместе с удаляемой операцией из журнала исключаются все зависимые операции с вершинами, располагающимися вдоль цепей прямой зависимости от исходной вершины. Для оставшихся вершин пересматривается их возможность порождать конфликты. Например, если удалить некоторую вершину из цикла предшествования, то оставшиеся вершины становятся неконфликтными относительно данной группы отношений. После разрешения конфликтов, оставшиеся в журнале операции упорядочиваются согласно отношениям предшествования. Полученная в результате транзакция удовлетворяет всем наложенным семантическим ограничениям и предусловиям, необходимым для корректного воспроизведения журнала.
Представленный метод был изложен в предположении строгих необходимых отношений зависимости и порядка между операциями транзакций. Он естественным образом обобщается на нестрогий случай в результате инициирования процесса семантической реконсиляции с наиболее полной системой ограничений и ее последовательного ослабления. Однако полученные результаты нуждаются в дополнительной валидации, а при выявленных нарушениях - и в возможной дополнительной коррекции. Поскольку коррекция вносит новые изменения, которые могут конфликтовать с операциями исходных транзакций, процесс должен быть повторен, начиная с этапа семантического анализа.
Организация более сложного итерационного процесса сама по себе не гарантирует нахождение решения. Однако решения, полученные таким образом, являются более значимыми, поскольку обеспечивают полноту представления результирующей транзакции. В случае неудачи метод допускает возвращение к предыдущим стадиям решения, учитывающим большее количество ограничений. Заметим, что тривиальные решения задачи всегда существуют, и применение метода в результате возврата к ее строгой исходной постановке гарантирует их нахождение.
