CWB

CWB(Concurrency Work Bench)をつかって、色々作業。

• 交換性をcongruenceとからめて定義しなおす
• 連動性の性質を、合成したLTSを射影すると、（たぶん）weak congruenceがなり立つことに書き直す
• 縦・横チェーンを本物（バッファ長1のoverflowも辞さず型の▽演算なのに、上書きされないというパターン）に置き換えて、連動性とか、確かに上書きされないとかをCWBをつかって確かめる

CWBを使うのはやむを得ないですねえ、結果を信じることができるか？というのはあります。

CWBで充足系の話をするときに学んだこと

• 模倣性関係で、SysとSpecの間の模倣性で充足性を示すのははまる
  • その心：充足を示すため、よほどちゃんとSpecを書かないとだめ
• したがってNG遷移のプロセスとの並行結合をとってNGに到達しないことを示す
  • まあこれって、充足Gameと同じようなのりになります

いろいろ学んだが、予備審査のための草稿提出まであと5日、、、

というところで時間切れ。