Think Stitch
PRINCIPIA  最近の更新


イベントとチャネルの改名

プロセスが発生させるイベントや通信に使うチャネルは定義の中に記述されています。この定義を変えずに、外からの指定でイベントやチャネルを差し替えることのできる改名 rename というオペレータについて説明します。

改名 rename の構文は次の通りです。

(rename rename-map process)

改名の対象にするプロセスを process に指定します。 rename-map には、どのイベントまたはチャネルを何に変えるのかという対応付けを指定します。これはイベントまたはチャネルのペアのリストで指定します。いわゆる連想リストです。

改名がどのように行われるのかを言葉で説明すると少しわかりにくいので、例で示すことにします。

まずはじめにプロセスの定義で使うイベントとチャネルを定義します。

(define-event a)
(define-event b)
(define-event c)

(define-channel ch (x) '((0) (1) (2)))

上記のイベントやチャネルに対応する部分が実行されたことを確認するために、さらに補助となるイベントとチャネルを定義します。これらもプロセス定義の中で使います。

(define-event xa)
(define-event xb)
(define-event xc)

(define-channel xch (x) '((0) (1) (2)))

改名の対象となるプロセスを次のように定義します。それぞれの節で2番目に発生するイベントは、1番目のイベントが改名されても、その節が選ばれたことがわかるようにするためのものです。

(define-process P
  (alt
    (! a (! xa STOP))
    (! b (! xb STOP))
    (! c (! xc STOP))
    (? ch (x) (! xch (x) STOP))))

計算木は次のようになります。

次に改名先となるイベントとチャネルを定義します。チャネル wch だけ定義域を少し小さくしてあります。2 が含まれていません。

(define-event d)
(define-event e)

(define-channel uch (x) '((0) (1) (2)))
(define-channel wch (x) '((0) (1)))

イベントの改名

いちばん簡単なのは、イベントを別のイベントに改名する場合です。プロセス P を改名したプロセス R を次のように定義します。ここではイベント a を e に改名することにします。

(define-process R
  (rename `((,a . ,e))
    P))

バッククォート記法に慣れていない方は、以下の部分:

  (rename `((,a . ,e))

を次のように書くこともできます。

  (rename (list (cons a e))

rename-map は評価されるので、イベントまたはチャネルの連想リストになる式であれば、どのようなものでも指定できます。もちろん関数を使ってもかまいません。

プロセス R の計算木は次のようになります。イベント a の遷移がなくなって、代わりにイベント e の遷移が現れています。これがイベント a の遷移に対応する節であったことは、イベント e の後に発生するイベントが xa であることからわかります。

複数のイベントを同時に改名することもできます。

(define-process R
  (rename `((,a . ,e) (,b . ,d))
    P))

チャネルの改名

イベントと同様、チャネルも改名することができます。 rename-map でチャネルのペアを指定します。

(define-process R
  (rename `((,ch . ,uch))
    P))

チャネル ch の各遷移が uch の遷移に代わります。

チャネルを改名する場合は、改名先チャネルの定義域が元のチャネルの定義域を含んでいなければなりません。以下の例ではチャネル ch を wch に改名しようとしていますが、wch の定義域は ch のものよりも狭いのでエラーになります。

(define-process R
  (rename `((,ch . ,wch))
    P))

イベントからチャネルへの改名

rename-map でイベントとチャネルのペアを指定すると、1つの遷移が複数の遷移になります。各遷移は、チャネルに属する各チャネルイベントに対応します。

(define-process R
  (rename `((,a . ,uch))
    P))

イベント a の遷移が消えて、代わりにチャネル uch に属する3つのチャネルイベント uch.0, uch.1, uch.2 の遷移が現れていることがわかります。

チャネルからイベントへの改名

今度は逆に、rename-map でチャネルとイベントのペアを指定すると、 そのチャネルに対応するすべての遷移が、同じイベントの遷移になります。イベント e が発生したとき、どの遷移が選ばれるかは非決定的になります。

(define-process R
  (rename `((,ch . ,e))
    P))

チャネルイベントの改名

チャネルイベントを使うと、チャネルの遷移の中の一部分だけを改名することができます。チャネルイベントは関数 $ で得ることができます。次の例では、チャネル ch の遷移のうち、引数 1 に対応する遷移だけをイベント e に改名しています。

(define-process R
  (rename `((,($ ch 1) . ,e))
    P))

アトミックイベントと同じように、チャネルイベントもチャネルへと改名することができます。

(define-process R
  (rename `((,($ ch 1) . ,wch))
    P))
2013/08/06
© 2013,2014,2015 PRINCIPIA Limited