MaudeでCCS 拡張編 - keigoiの日記

ここで書いた abort 演算子を Maudeで実装した。 CCSの構文と意味は先ほどのエントリのものをつかった(ちょっと変えたけど)。

http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude

演算子を追加

  op _:_abort_ : Act Process Process -> Process [frozen prec 27] .

parsingがうまくいかなかったので_._abort_ をやめて _:_abort_ にした。

操作的意味の変更

補助的な関数

abort 動作後のプロセスを返す関数 Abt を定義した。

  *** `aborting' function (added)
  op Abt : Process -> Process .
  eq Abt (A . P) = 0 .
  eq Abt (A : P abort Q) = Q .
  eq Abt (P + Q) = Abt(P) | Abt (Q) .
  *** and more...

振る舞いの変更

abort 演算子の振る舞いを追加した。

  *** Abort (added)
  rl A : P abort Q => {A}P .
  *** Summation (modified)
  crl P + Q => {A}(P' | Abt (Q)) if P => {A}P' .

ここで {A}P とはアクションAでPに遷移したことを表す。

試してみる

search [10] [ ('a : 'b . 0 abort 'fail_a . 0  + 'c . 0 | ~ 'c . 0) \ 'c ] =>+ P:ActProcess .

$(a:b.0 \mbox{\bf abort} fail_a .0 + c.0 \quad | \quad \overline{c}.0) \setminus \{c\}$ というプロセスの遷移先を探す。
(演算子 [_] は遷移関係の反射推移閉包を作ってくれる。)

期待したいのは τ遷移した(選択でcが選ばれた)場合にはアクション a が選ばれなかったという意図の fail_a という遷移をすること。

search in CCS : [(~ 'c . 0 | 'c . 0 + 'a : 'b . 0 abort 'fail_a . 0) \ 'c] =>+ P:ActProcess .

Solution 1 (state 1)
states: 2  rewrites: 8 in 0ms cpu (0ms real) (37209 rewrites/second)
P:ActProcess --> {'a}(0 | 'b . 0 | ~ 'c . 0) \ 'c

Solution 2 (state 2)
states: 3  rewrites: 30 in 0ms cpu (0ms real) (66079 rewrites/second)
P:ActProcess --> {tau}(0 | 0 | 'fail_a . 0) \ 'c

Solution 3 (state 3)
states: 4  rewrites: 45 in 0ms cpu (0ms real) (64935 rewrites/second)
P:ActProcess --> {'a}[(0 | 'b . 0 | ~ 'c . 0) \ 'c]

Solution 4 (state 4)
states: 5  rewrites: 58 in 0ms cpu (0ms real) (68235 rewrites/second)
P:ActProcess --> {'a}{'b}(0 | 0 | ~ 'c . 0) \ 'c

Solution 5 (state 5)
states: 6  rewrites: 125 in 2ms cpu (2ms real) (62250 rewrites/second)
P:ActProcess --> {'a}{'b}[(0 | 0 | ~ 'c . 0) \ 'c]

Solution 6 (state 6)
states: 7  rewrites: 231 in 4ms cpu (4ms real) (56994 rewrites/second)
P:ActProcess --> {tau}[(0 | 0 | 'fail_a . 0) \ 'c]

Solution 7 (state 7)
states: 8  rewrites: 239 in 4ms cpu (4ms real) (57341 rewrites/second)
P:ActProcess --> {tau}{'fail_a}(0 | 0 | 0) \ 'c

Solution 8 (state 8)
states: 9  rewrites: 257 in 4ms cpu (4ms real) (55126 rewrites/second)
P:ActProcess --> {tau}{'fail_a}[(0 | 0 | 0) \ 'c]

No more solutions.
states: 9  rewrites: 274 in 5ms cpu (5ms real) (49827 rewrites/second)
Maude>

できてるねー
ついでなので HMLの論理式も試したい…