sharing(共有)

代数演算子

interleaving の例において、MIKEとRISAはコインを別々に入れるが、二人で乾杯して同時に飲み始めるような場合はsharing（共有）を使う。
P[|{event}|]Q　のように記述すると指定されたイベントで同期し、それ以外のイベントについては interleavingと同じく別々に起こす。

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

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

PEOPLE = MIKE |[{drink}]| RISA

 --    PEOPLEの実行例
 -- < coin(RISA),lemonade,coin(MIKE),cider,drink(RISA&MIKE) >

プロセスPEOPLE はMIKE と RISA のどちらが先にコインを入れてジュースを買うかはわからないが、drinkのイベントでは必ず同期する。イベントcoin はMIKEとRISAが別々に起こすので2度起きるが、drink は2人で同期するので１度しか起こらない。

sharingの同期するイベントを空とすると、interleaving に等しい。

P[|{}|]Q ＝ P|||Q