Implementing CCS in Maude2

やっぱりπ計算の前にCCSだよねーということで Implementing CCS in Maude2 (著者による.ps) を軽く読んだ。
ラベル付き遷移を書き換えでやるのは案外面倒らしく、せっかくの | や + がfrozenになってしまっている(前回のπ計算ではラベル無しのreduction(τ遷移に相当)だったので問題なかった)。 まあ 別に規則を書けば済む話なんですが。 あとsubsortって案外きもちわるい subsort Process < ActProcess のあたりが特に。 Hennessy-Milner logic の実装もある。ここで 演算子 [a]F で必要な 「aで遷移する先の全てのプロセス」という探索が普通のMaudeのsearch(書き換えの候補を最初の一つだけ提示) ではできないので、リフレクション(みたいなもの)な探索 metaSearchを使って遷移先を全て列挙するということをやっている。こういうメタなこともできるのがMaude

動かしてみる

http://maude.cs.uiuc.edu/maude1/casestudies/ccs/ より、論文で使われている maudeのソースが得られる。
そのままだと MachineInt が解決できないと言われたので protecting RENAMED-INT でインポートした。
MachineInt は Nat で代用できたのでそのように書き換えた。

diff

-  var N : MachineInt .
+  var N : Nat .
:
-  op allOneStep : Term MachineInt Term -> TermSet .
+  op allOneStep : Term Nat Term -> TermSet .
:
-  var N : MachineInt .
+  var N : Nat .

あとMODAL-LOGICモジュールはうまく読み込めなかったので省いた。 (追記) MachineIntをNatにしたら読み込めた。

実行

手元のmaude (Darwin) では 一緒に付いてくる machine-int.maude を引数に指定したらいけた。 標準では読み込まれないものなのか？ Darwin版だから？ Maude1.0 にしかない？

$ maudeccs2.maude
:
:
Maude> rew 'Proc .
rewrite in EXAMPLE : 'Proc .

rewrites: 64 in 0ms cpu (382ms real) (89887 rewrites/second)
result ActProcess: {'a}'b . 'Proc
Maude> 

ふむ 'a.'b.'Proc が ラベル 'a で プロセス 'b.'Proc に遷移していることが確認できる。

またこんど 以前定義した abort を実装する。眠いのでここまで。