renaming(変更)

renaming P[ [e<-e'] ] は、プロセスPの持つあるイベントe を別のイベントe' に変更したプロセスを表す。例えば、

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

MIKE = PERSON[[ lemonade<-cider ]]
-- このプロセスは次のようになる。

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

複数のイベントを変更することもできる。

channel bill -- お札
RISA = PERSON[[ coin<-bill,coke<-cider ]]
-- このプロセスは次のようになる。

RISA = bill -> ( cider -> drink -> SKIP
                 |~|
                 leomonade -> drink -> SKIP )

検証ツールにFDR2を使う場合、同じ構造のプロセスを複数定義するときは renamingを使って定義する方が計算量を減らすことができる。