昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう１本もらえるというものである。今回はそれを単純化しモデリングする。 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(…