やっぱりπ計算の前にCCSだよねーということで Implementing CCS in Maude2 (著者による.ps) を軽く読んだ。 ラベル付き遷移を書き換えでやるのは案外面倒らしく、せっかくの | や + がfrozenになってしまっている(前回のπ計算ではラベル無しのreduction(τ遷…

ここ で書いた abort 演算子を Maudeで実装した。 CCSの構文と意味は先ほどのエントリのものをつかった(ちょっと変えたけど)。http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude 演算子を追加 op _:_abort_ : Act Process Process -> Pro…

http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude ←今日のエントリで使っているMaudeのソースコードものぐさなので ちゃんと解説を書くのがめんどいのです… 問題 abort 演算子のチェックのために eq context = ('AbtTest =def (('a : 'b…