昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう１本もらえるというものである。今回はそれを単純化しモデリングする。 channel coin, juice VMB(n) = coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2)…

conditional choice "if b then P else Q" は bがTRUEの場合プロセスPが、bがFALSEの場合はプロセスQが実行される。例えば、ジュースの残数を保持している自販機VMRの例を考える。 channel coin, juice VMCNT(n) = coin -> juice -> VMCNT(n-1) VMR = VMCNT(…

renaming P[ [e channel coin,coke,lemonade,cider,drink PERSON = coin -> ( coke -> drink -> SKIP |~| lemonade -> drink -> SKIP ) MIKE = PERSON[[ lemonade<-cider ]] -- このプロセスは次のようになる。 MIKE = coin -> ( coke -> drink -> SKIP |~| …