В.В. Девятков, Д.В. Ошкало
12
% описание процессов изменения моделей
% списки используются для сохранения информации о текущем
состоянии моделей
btrans(X,Y,List) :- r(Y,Z), append([Z],[],List).
merge(X,Y,Z,List) :- (X == Z -> append([Y],[],List) ;
append([Z],[],List) ).
ftrans(X,Y,List) :- r(X,Z), append([Z],[],List).
% процедура синхронизации
% X1, Y1 — состояние моделей до изменения
% X2, Y2 — состояние моделей после изменения
snc(X1, X2, Y1, Y2, List, List2) :- btrans(X1, Y2, [H]),
merge(H,X1,X2,[List]),
ftrans(List,Y2,[List2]),
r([List],[List2]).
% свойства процесса синхронизации
% симметричность
symmetric(X1,X2,Y1,Y2) :- snc(X1,X2,Y1,Y2,List,List2),
writef("1:"),nl,
write(List),nl,write(List2),nl,
writef("2:"),nl,
snc(Y1,Y2,X1,X2,List3,List4),
write(List3),nl,write(List4),
List == List3,
List2 == List4.
% стабильность
stable(X1,X2,Y1,Y2) :- r(X1,Y1),
snc(X1,X2,Y1,Y2,List,List2),
writef("Результат:"),nl,
write(List),nl,write(List2),nl,
X1==List,
Y1==List2.
Проверим, удовлетворяет ли построенный таким образом процесс
синхронизации требованию стабильности:
?— stable(a, a, x, x), stable(b, b, x, x), stable(a,a,y,y).
Результат:
a
x
