internal choice(内部選択) - CSP(Communicating Sequential Processes)

internal choice '|~|'はプロセスの内部選択を表す。外部選択との違いを購入者の例を使って説明する。

購入者はコインを入れ、コーラかレモネードを購入した後にそれを飲む。コーラとレモネードの選択は購入者自身の好みや気分によって決定されるとする。

channel coin, coke, lemonade, drink
PERSON = coin -> ( coke -> drink -> SKIP
                   |~|
                   lemonade -> drink -> SKIP )

ここでは、プロセスcoke->drink->SKIP, lemonade->drink->SKIPの選択を内部選択とした。'内部'の意味はその選択が外部（自販機）によらず PERSON自身によって決定されるということである。もしコーディングする際は、この選択は交互でもランダムでも常にどちらか片方のみを選ぶとしてもよい。*1

また、この選択がいつ行われているのかはPERSONの外部からは分からない。コインを入れる前にすでに決まっていても、コインを入れた後に選択していても、外部にとっては同じである。つまり、次のように PERSON を記述してもまったく先と同様なプロセスとなる。

 PERSON = coin -> coke -> drink -> SKIP
          |~|
          coin -> lemonade -> drink -> SKIP

一方で、下記の自販機VMSはプロセスcoke->VMS, lemonade->VMSを外部選択としている。この選択はVMS自身だけで決定するのではなく coke, lemonade どちらのイベントが起きるかは外部（購入者）によるということである。

channel coin, coke, lemonade
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

プロセスPERSONにdrinkという動作（イベント）を定義したが、これはVMSとは関係がないイベントである。drinkは単なる動作としても良いが、例えば二人で乾杯するときなどは相互作用となるだろう。これは後の例で。

*1:内部選択で記述されたプロセスはこれらすべての可能性を考え検証している。