連動性

D論みなおしていて、連動性の検証をCWBでやっていたのだがどうも変だ

  • X=a.b.X, Y=c.d.Yのとき
  • Z=X|Yに対して
  • ZはXあるいはYに対する連動性がありません
    • ずっとX(Y)が占有する可能性があるから

というのをCWBで占めそうとおもったのですが
obseqオプションは弱模倣性の検証で、期待値はfalseだったのに。。

CWBで連動性を検証すること自体がだめっとけと?

*Zは直積です
proc Z = (X | Y)

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

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

*cwb-nc> eq -S obseq Proj_ab X
*..略..
*TRUE