interrupt(割り込み)

interrupt '/\' は P/\Q でプロセスPの実行中に Q が割り込む可能性を表す。プロセスP 実行中にプロセス Q のイベントが起こると Q に実行が移る。その後 P に実行は戻らない。

親子が自販機でジュースを買うときに、親がコインを入れボタンを押そうとすると急に子供がボタンを押したがったので子供に任すような場合を考えよう。

channel coin, coke, lemonade
PARENT = coin -> lemonade -> SKIP
CHILD = coke -> SKIP

FAMILY = PARENT /\ CHILD

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

SYSTEM = FAMILY [{coin,coke,lemonade}||{coin,coke,lemonade}] VMS

プロセスPARENT に対して CHILDが割り込むのは CHILDのイベントcoke が起きたときである。cokeはVMSと同期して起こるのでコインを入れるまで CHILD が割り込むことはない。SYSTEMは最初、かならず coinイベントが起きる。

coinイベントの後、親がレモネードを買うか、子供がコーラを欲しがり割り込むかは分からない。SYSTEM は両方の可能性を持ったプロセスとなる。