Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
11
thread([put(reqs,bye),put(brpc,byersp)]).
thread([put(irps,invsucc), put(ackc,ack)]).
thread([put(reqc,bye)]).
thread([put(reqs,bye),put(brpc,byersp)]).
thread([put(brps,byersp)]).
thread([put(end,enduac)]).
uac([put(start,startuac)]):-thread([put(start,startuac)]).
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)]).
confirming([put(irps,incsuc),put(ackc,ack)]):-
inviting([put(reqc,invite)]),thread([put(irps,incsuc),put(ackc,ack)]).
confirming([put(irps,incsuc),put(ackc,ack)]):-
inviting([put(brps,byersp),put(invalid,assertf)]),thread([put(irps,incsuc),
put(ackc,ack)]).
confirming([put(irps,invfail),put(invalid,assertf)]):-
confirming([put(irps,invfail),put(invalid,assertf)]),thread([put(irps,invfail),
put(invalid,assertf)]).
confirming([put(irps,invsucc),put(invalid,assertf)]):-
confirming([put(irps,invfail),put(invalid,assertf)]),thread([put(irps,invsucc),
put(invalid,assertf)]).
confirming([put(brps,byersp),put(invalid,assertf)]):-
confirming([put(irps,invfail),put(invalid,assertf)]),thread([put(brps,byersp),
put(invalid,assertf)]).
confirming([put(irps,invfail),put(invalid,assertf)]):-
confirming([put(irps,invsucc),put(invalid,assertf)]),thread([put(irps,invfail),
put(invalid,assertf)]).
confirming([put(irps,invsucc),put(invalid,assertf)]):-
confirming([put(irps,invsucc),put(invalid,assertf)]),thread([put(irps,invsucc),
put(invalid,assertf)]).
confirming([put(brps,byersp),put(invalid,assertf)]):-
confirming([put(irps,invsucc),put(invalid,assertf)]),thread([put(brps,byersp),
put(invalid,assertf)]).
confirming([put(irps,invfail),put(invalid,assertf)]):-
confirming([put(brps,byersp),put(invalid,assertf)]),thread([put(irps,invfail),
put(invalid,assertf)]).
