Формальный логический анализ корректности спецификаций сетевых SIP-протоколов - page 10

В.В. Девятков, Т.Н. Мьё
10
ния процесса
uac.
Аналогично
для процесса
inviting
(см. рис. 4) вво-
дим два правила:
inviting([put(reqc,invite)]):
uac([put(start,startuac)]), thread([put(reqc,invite)])
и
inviting([put(brps,byersp),put(invalid,assertf)]):
inviting([put(reqc,invite)]),thread([put(brps,byersp),put(invalid,assertf)]).
Число этих правил совпадет с числом нитей, после выполнения
которых и при условии, что агент находится в состоянии выполнения
процесса
uac
, начинает выполняться процесс
inviting.
Аналогично
вводятся правила для всех остальных процессов (
confirming
,
byeing,
preending, ending
). В дополнение к этому вводим факты с предикат-
ным символом
thread
, соответствующие всем нитям на рис. 4. В раз-
делах
domains
и
predicates
описываем все используемые в разделе
clauses
типы аргументов и предикатов.
domains
channel=symbol
message=symbol
put=put(channel,message)
list =put*
predicates
nondeterm uac(list)
nondeterm inviting(list)
nondeterm confirming(list)
nondeterm byeing(list)
nondeterm preending(list)
nondeterm ending(list)
nondeterm thread(list)
clauses
thread([put(start,startuac)]).
thread([put(reqc,invite)]).
thread([put(irps,invfail)]).
thread([put(reqs,bye),put(brpc,byersp)]).
thread([put(brps,byersp),put(invalid,assertf)]).
thread([put(irps,incsuc),put(ackc,ack)]).
thread([put(irps,invfail),put(invalid,assertf)]).
thread([put(irps,invsucc),put(invalid,assertf)]).
thread([put(brps,byersp),put(invalid,assertf)]).
1,2,3,4,5,6,7,8,9 11,12,13,14,15
Powered by FlippingBook