8 / 10
clauses
transition(b11, [f(reqs,invite,uac,startuac)], b12).
transition(b12, [f(irps,invsucc,ackc,ack)], b13).
transition(b13, [f(brps,byersp,reqc,bye)], b14).
transition(b13, [f(irps,invfail,reqc,bye)], b13).
transition(b14, [f(reqs,bye,brpc,byersp)], b15).
transition(b15, [f(brps,byersp,uac,end)], b16).
transition(b21, [f(reqs,invite,uas,startuas)], b22).
transition(b22, [f(irps,invsucc,ackc,ack)], b23).
transition(b23, [f(brps,byersp,reqc,bye)], b24).
transition(b24, [f(irps,invfail,reqc,bye)], b23).
transition(b24, [f(reqs,bye,brpc,byersp)], b25).
transition(b25, [f(brps,byersp,uas,end)], b26).
accessible(B1, [X], B2) : – transition(B1, [X], B2).
accessible(B1, [X|Rest], B2) : – transition(B1, [X], B3), accessible(B3, Rest, B2).
goal
accessible(b11,[ f(_,invite,_,_), f(_,invsucc,_,_) , f(_,byersp,_,_), f(_,bye,_,_),
f(_,byersp,_,_)], b16),
accessible(b21,[ f(_,invite,_,_), f(_,invsucc,_,_) , f(_,byersp,_,_), f(_,bye,_,_),
f(_,byersp,_,_)], b26) .
Раздел
goal
содержит задачу нахождения двух путей, ведущих
из начального состояния
b11
в финальное состояние
b16
графа на
рис. 3 и из начального состояния
b21
в финальное состояние
b26
гра-
фа на рис. 4, содержащих одинаковые последовательности реакций и
восприятий. Результатом работы данной программы является ответ
“yes”, означающий наличие на графе (см. рис. 3) пути
!invite, !invsucc,
!byersp, !bye, !byersp
, а на графе (см. рис. 4) пути
?invite, ?invsucc,
?byersp, ?bye, ?byersp
, ведущих из начального состояния в конечное
на соответствующих графах.
Заключение.
1. Рассмотрена проверка правильности SIP-специ-
фикаций, представленных моделями последовательностных взаимо-
действующих агентов. В отличие от других в настоящей работе для
описания агентов используется хорошо структурированный и разви-
тый вариант языка, основанный на моделях взаимодействующих по-
следовательностных процессов (
π
-исчислении), язык временн´ой мо-
дальной логики для описания требований к спецификациям и язык
логического программирования VISUAL PROLOG для проверки пра-
вильности спецификаций.
2. Изложены принципы перехода от процессных моделей SIP-
спецификаций к логической программе и от требований на языке
модальной логики к формулировке цели на языке VISUAL PROLOG.
3. Приведен пример логической программы и результаты ее ра-
боты.
114 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 2