14.4.4 表示法

协议状态机

协议状态机的图示与行为状态机的很类似。«protocol»关键字放置于靠近名称的地方以区分这是协议状态机图。

图14.44 ProtocolStateMachine example

协议状态机中与一个状态关联的不变量的文本表示是通过将它置于该状态的名称之后或之下，并封闭在方括号内（图14.45）。

图14.45 Notation for a State with an invariant

协议转变

一般的状态机图示是适用的。区别在于协议转变没有effect行为，有后置条件。后置条件与guard条件有相同的语法，但出现在转变语法的末尾。

图14.46 ProtocolTransition notation