Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
13
byeing([put(reqs,bye),put(brpc,byersp)]),
thread([put(reqs,bye),put(brpc,byersp)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
confirming([put(irps,incsuc),put(ackc,ack)]),thread([put(reqs,bye),
put(brpc,byersp)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
confirming([put(irps,invfail),put(invalid,assertf)]),thread([put(reqs,bye),
put(brpc,byersp)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
confirming([put(irps,invfail),put(invalid,assertf)]),thread([put(reqs,bye),
put(brpc,byersp)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
confirming([put(brps,byersp),put(invalid,assertf)]),thread([put(reqs,bye),
put(brpc,byersp)]).
preending([put(irps,invfail)]):-
inviting([put(reqc,invite)]),thread([put(irps,invfail)]).
preending([put(irps,invfail)]):-
inviting([put(brps,byersp),put(invalid,assertf)]),thread([put(irps,invfail)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
inviting([put(reqc,invite)]),thread([put(reqs,bye),put(brpc,byersp)]).
preending([put(reqs,bye),put(brpc,byersp)]):-
inviting([put(brps,byersp),put(invalid,assertf)]),thread([put(reqs,bye),
put(brpc,byersp)]).
preending([put(brps,byersp)]):-
byeing([put(reqc,bye)]),thread([put(brps,byersp)]).
preending([put(brps,byersp)]):-
byeing([put(irps,invifail),put(invalid,assertf)]),thread([put(brps,byersp)]).
preending([put(brps,byersp)]):-
byeing([put(irps,invsucc),put(invalid,assertf)]),thread([put(brps,byersp)]).
preending([put(brps,byersp)]):-
byeing([put(reqs,bye),put(brpc,byersp)]),thread([put(brps,byersp)]).
ending([put(end,enduac)]):-
preending([put(reqs,bye),put(brpc,byersp)]),thread([put(end,enduac)]).
ending([put(end,enduac)]):-
preending([put(irps,invfail)]),thread([put(end,enduac)]).
ending([put(end,enduac)]):-
preending([put(reqs,bye),put(brpc,byersp)]),thread([put(end,enduac)]).
