interleaving

interleaving P|||Q はプロセスP,Q がイベントで同期せずに、完全に独立して動作することを表す。例えば、以下のようなMIKEとRISAの動作を考える。

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

RISA = coin -> lemonade -> drink -> SKIP

MIKEはコーラかサイダーを飲み、RISAはレモネードしか飲まないとする。MIKEとRISAは共通のイベントcoin, drink を持つが、このイベントで２人が同期するわけではない。２人で一緒にコインを入れるわけではないし、２人で同時に飲むとは限らないだろう。このような場合はinterleavingで記述する。

 PEOPLE = MIKE ||| RISA
 
 aPEOPLE = {coin,coke,cider,lemonade,drink}
 --      = aMIKE ∪ aRISA

この記述ではMIKEとRISAはすべてのイベントをそれぞれ別々に起こす。
さらにVMSとの関係を記述してみよう。

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

aVMS = {coin,coke,lemonade,cider}

SYSTEM = VMS [aVMS||aPEOPLE] PEOPLE

 -- SYSTEMの実行例
 -- <coin(MIKE),coke,coin(RISA),drink(MIKE),lemonade,drink(RISA)>

MIKEが先に coin のイベントを起こした後は MIKEがジュースを選びVMSが再び最初の状態に戻るまで、RISAはイベントcoinを起こすことはできない。（VMSのcoinと同期する必要があるので。）
VMSはMIKEとRISAの起こすイベントcoin,coke,lemonade,ciderで同期しているが、これらを起こしたのが MIKE であるか RISA であるかは考慮していない。プロセスPEOPLE とイベント同期しているだけである。