CCS in maude

研究 主テーマ

久しぶりに、みなおす。最近 Acetoのamazon:Reactive Systemsにはまっていて
CCSってどうやって実装されていたっけということ

CCS case study

  • Maude2.0をつかって遷移ルールがかかれている
  • 再帰方程式を素直にrewriteするととまらないのでfrozen指示子をつかう
  • そうすると書き換えがすすまないので、動いた気がしない
  • なのでＣＣＳ遷移のtransitive closureを計算するdummy opeを定義する
  • HMLの実装は結構「直線」ではあるが[]演算が全てのなのが、書き換えシステムが全探索できなのでこまる
  • なのでmetaSearchでがんばる（書き換えシステムの、Ｎ番目の解をえるというような指示が出来る）
  • そうするとHMLもきわめて素直に書ける。

ということのようだ、ACPの\nabla演算の実現は遠いぞ！


今朝のmusicはradio headのコンサートRadiohead: Live In Concert : NPR、
56分あたりから No Surprizeだ