parallel(並行)

代数演算子
アルファベット

プロセスのアルファベットを定義しておく。プロセスP のアルファベットαP とは P の持つべきイベントの集合である。例えば、

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

aVMS = {coin, coke, lemonade}  -- VMSのアルファベット

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

aPERSON = {coin, coke, lemonade, drink}
parallel（並行）

P[αP||αQ]Q *1でプロセスP,Qの並行動作を表す。αPとαQの共通のイベントでPとQは同期する。

これまで購入者(PERSON)と自販機(VMS)を記述してきたので、これらが互いに作用しながら動作するシステムの記述を行おう。PERSONとVMSはそれぞれの共通イベントcoin,coke,lemonadeで同期する。drinkはPERSONのみが行うので自販機と同期しない。

 SYSTEM = VMS[{coin,coke,lemonade}||{coin,coke,lemonade,drink}]PERSON
 
 -- 次のように書いても同じ。
 aVMS = {coin, coke, lemonade}
 aPERSON = {coin, coke, lemonade, drink} 
 SYSTEM = VMS [aVMS||aPERSON] PERSON

プロセスSYSTEMは１〜４を繰り返す。

  1. VMS,PERSONともにイベントcoin が起こせる（ready）状態にあるので、coinのイベントが起こりVMS、PERSONともに次のプロセスに移る。
  2. PERSONはcoke->drink->PERSON または lemonade->drink->PERSON のどちらかのプロセスを選択している。
  3. 前者[後者] の場合、イベントcoke[lemonade] で同期しPERSONは次のプロセスに移り、VMSは自身に戻る。
  4. PERSONはイベントdrinkを起こし、最初の状態に戻る。
外部選択と環境

上記のSYSTEMは PERSONが内部選択で coke,lemonade どちらのイベントを起こすかを選択していると言えるが、ここでPERSONも外部選択を行うような場合を考えてみよう。例えば、購入者がcoke,lemonade 両方のボタンを同時に押して決定を自販機に任せるような場合である。

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

PERSON = coin -> ( coke -> drink -> PERSON
                   []
                   lemonade -> drink -> PERSON )

SYSTEM = VMS [aVMS||aPERSON] PERSON

このように PERSON（またはVMS)の外部選択のどちらのイベントも実行可能な場合、この選択は非決定的（内部選択）になる。つまり、coke, lemonade のどちらのイベントが起こるかは分からないが、どちらかのイベントは起こる。実際に自販機のボタンを２つ同時に押したとき、どのような決定のされ方をするのかは自販機によるだろう。

 --イベント a,b が共に起こり得る（ready）状態ならば、
 ( a->P [] b->Q ) ≡ ( a->P |~| b->Q )

このことから、選択に関するイベントが同じ場合は常に非決定的になる。

( a->P [] a->Q ) ≡ ( a->P |~| a->Q )

*1:よく P||Q で省略表記する。