Разработка процессов синхронизации моделей и принципов проверки их корректности - page 10

В.В. Девятков, Д.В. Ошкало
10
Листинг 1
Пример процессной программы синхронизации на языке SWI PROLOG
% a1, a2, a3 — состояния процесса обработки модели A
% y1, y2 — воздействия, обусловливающие переход между
состояниями процесса обработки модели А
% b1, b2, b3, b4 - состояния процесса обработки модели B
% x1, x2 — воздействия, обусловливающие переход между
состояниями процесса обработки модели B
% правила переходов для процесса, работающего с моделью A
transform(a1, y1, a2).
transform(a2, y2, a3).
% правила переходов для процесса, работающего с моделью B
transform(b1, x1, b2).
transform(b2, x1, b3).
transform(b2, x2, b4).
% отношение консистентности
r(b4, a3).
r(b1, a3).
r(X,Y) :- r(Y,X).
% правила достижимости
accessible(B1, [H], B2) :- transform(B1, H, B2).
accessible(B1, [H|T], B2) :- transform(B1, H, B3),
accessible(B3, T, B2).
% процесс синхронизации; XN, XY — начальные состояния
моделей A и B
sync(XN, YN, X,Y) :- accessible(XN,[H1|T1], X),
accessible(YN,[H2|T2],Y), r(X,Y).
Используя правила достижимости, проверим, возможна ли кор-
ректная синхронизация моделей
A
и
B
с применением данных про-
цессов. Для этих целей составим запрос
? — sync(b1, a1, b4, a3)
true
На запрос получен положительный ответ. Таким образом, для
выбранных начальных и конечных состояний возможна синхрониза-
ция, в основе которой находится изображенный на рис. 3 процесс.
Далее рассмотрим пример алгоритма синхронизации, предло-
женного в [6]. Даны две модели
A
и
B
, каждая из которых имеет по
два состояния:
{ , }
a b A
,
{ , }
x y B
. На некотором подмножестве со-
1,2,3,4,5,6,7,8,9 11,12,13,14,15
Powered by FlippingBook