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を使って定義する方が計算量を減らすことができる。