13 / 23
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
77
Логическая программа проверки свойства обязательной реакции
для рассматриваемого примера может выглядеть следующим образом
(здесь названия секвентов, конфигураций, каналов и сообщений пред-
ставлены на английском языке):
domains
rlp = rlp(receive, put)
plr = plr(put, receive)
receive = receive(p1l, p2l)
p1l = p1l(symbol)
p2l = p2l(symbol)
put = put(lp1, lp2)
lp1 = lp1(symbol)
lp2 = lp2(symbol)
rp1p = rp1p(p1receive, p1put)
pp1r = pp1r(p1put, p1receive)
p1receive = p1receive(lp11)
p1put = p1put(p1l1)
lp11 = lp11(symbol)
p1l1 = p1l1(symbol)
rp2p = rp2p(p2receive, p2put)
pp2r = pp2r(p2put, p2receive)
p2receive = p2receive(lp22)
p2put = p2put(p2l2)
lp22 = lp22(symbol)
p2l2 = p2l2(symbol)
predicates
nondeterm sequentRlp (symbol, symbol, rlp, symbol)
nondeterm sequentPlr (symbol, symbol, plr, symbol)
nondeterm sequentRp1p (symbol, symbol, rp1p, symbol)
nondeterm sequentPp1r (symbol, symbol, pp1r, symbol)
nondeterm sequentRp2p (symbol, symbol, rp2p, symbol)
nondeterm sequentPp2r (symbol, symbol, pp2r, symbol)
nondeterm execute(symbol,symbol,symbol,symbol,symbol,symbol)
clauses
sequentRlp(preparation, readiness, rlp(receive(p1l(opened),
p2l (opened)), put(lp1(invitation), lp2(invitation))), invit-
ing).
sequentRlp(notification, accepting, rlp(receive(p1l(invited),
p2l (invited)), put(lp1(quest), lp2(quest))), controlling).
sequentRlp(completion, implementing, rlp(receive(p1l(agreed),
p2l (agreed)), put(lp1(expectation), lp2(expectation))),
ending).
sequentRlp(cessation, terminating,
rlp(receive(p1l(completed), p2l (completed)),
put(lp1(closed), lp2(closed))), closing).
sequentPlr(reaction, inviting, plr(put(lp1(invitation),
lp2(invitation)), receive(p1l(invited), p2l (invited))),
accepting).
sequentPlr(information, controlling, plr(put(lp1(quest),
lp2(quest)), receive(p1l(agreed), p2l (agreed))),
implementing).