В.В. Девятков, Т.Н. Мьё
8
brpc?byeRsp
Ended
UAS
I ed nvit
reqc?invite
irps invFail
!
irps?invSucc. ack ! edF
ackc?ack. !assertF
|
|
F
F
reqc?bye.assert
brpc?byeRsp.assert
Сonfirmed
Bought
ackc?ack. acked !
T
|
!
F
brpc?byeR sp. assert
reqc?bye.brps!byeRsp
re q !b y e s
ackc?ack. acked !
T
|
reqc?bye.brps!byeRsp
PreEnded
!endUas
ackc?ack.!ackedT
|
|
s
!
F
reqc?bye.brp !byeRsp brpc?byeRsp. assert
?startUas
Рис. 3.
Граф переходов процесса
UAS
UAC start?startUac,
Inviting UAC.reqc!invite
Inviting.brps?byeRsp.invalid ! assertF ,
Confirmin g Inviting.
Confirmin g.irps?invFail.invalid ! assertF Confirmin g.irps
irps?invSu
?invSucc.invalid ! assert
cc.ackc!ack
F
Confirmin g.brps?byeRsp.inavalid ! assertF ,
Byeing Confirmin g.
Byeing. ps?invFail.invalid ! asseretF Byeing.irps?invSucc.invalid ! assertF
Byeing.reqs?bye.brpc!byeRsp
Pr eEnding Inviting.
reqc!bye
ir
irps?invFail Inviting.
Comfir min g.
Byeing.brps
Ending Pr eEnding !
Ending.irps?invFail ! assertT Ending.irps?invSuc
reqs?by
c! asser
e.brpc!byeRsp
r
tT
Ending.reqs?
eqs?bye.brpc!byeRsp
?by
bye.brpc!byeRsp Ending.b
eRsp,
end
rps?bye
U c
!
a
Rsp assertF .
Рис. 4.
Процессные выражения
UAС
