連動性２ - henjin1goの日記

いろいろ考えたら無限の内部遷移( $\tau$ )のループに陥る可能性があることを
プロパティでかけばよいではないか。

prop can_livelock =
   min X = livelock_now \/ <->X
prop livelock_now = 
   max X = <t>X

最大不動点と最小不動点の組み合わせたプロパティになる。

proc X = a.b.X
proc Y = c.d.Y
*Zは直積です
proc Z = (X | Y)

set Internals_cd = {c, d}
*ab,cdをそれぞれ隠蔽するためのものです
proc Hide_cd = 'c.Hide_cd + 'd.Hide_cd

*Zからcdを隠蔽した遷移系を得ます
proc Proj_ab = (Z | Hide_cd) \ Internals_cd

これでsearchコマンドによりlivelockを判断します

 cwb-nc> search Proj_ab can_livelock

これで大丈夫そうだ！