例題１
昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう１本もらえるというものである。今回はそれを単純化しモデリングする。
channel coin, juice VMB(n) = coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2) )
プロセスVMB はｎでジュースの残数を保持する。コインを入れるとジュースが出てきて、その後は最初に戻るか、当たりが出てさらにジュースが出るかは内部選択とする。（通常低確率だが、０％〜１００％で考えてよい）
さらにコインを入れれるのはジュースがある時のみで、０になると補充(fill)され残数が１０本になるとする。それ以外の場合は停止(STOP)する。
channel coin, juice, fill VMB(n) = if (n>0) then coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2) ) else if (n==0) then fill -> VMB(10) else STOP
同様に購入者もモデリングする。コインを入れジュースが出た後、さらにジュースが出るかどうかは自販機次第なので外部選択とする。
PERSON = coin -> juice -> ( PERSON [] juice -> PERSON ) -- この外部選択 ↑ はVMBの可能(ready)な -- イベントcoin or juice で決定する。 SYSTEM = VMB(5) [{coin,juice,fill}||{coin,juice}] PERSON
さて、このシステムは停止することなく動き続けるだろうか？少し考えてみてほしい。
もちろん、止まらぬようにするつもりで n=0 のときは補充するようにした。これを試しにFDR2でチェックしてみよう。
上の記述をテキストとして保存し、そのファイルをFDR2に読み込ませると、次のような画面が出てくる。
もし、下段部分のリストにプロセスが何も表示されていない場合は、CSPの記述に間違いがある。その場合は、optionのShow statusを選べばエラーの内容を教えてくれるので修正する。
今回は検証として、SYSTEMのデッドロックフリー*1を確かめる。検証項目からDeadlockを選択し、'↓'ボタンを押しimplementationにSYSTEMを入力する。
Checkボタンをクリックすると検証リストに結果が表示される。×SYSTEMと表示されたはずだ。
同じ要領でプロセスPERSONも検証してみると、こちらは✔の印が付く。
プロセスPERSONはデッドロックフリーであるが、プロセスSYSTEMはデッドロックになる可能性があることがこれよりわかる。
もし、× or ✔ ではなく、！のマークが出たら実行時のエラーである。このときもShow statusの画面でエラーの内容がわかる。
FDR2はどのような場合にデッドロックになるかを教えてくれる。検証リストのSYSTEMの部分をダブルクリックすると、新たにデバック画面が開く。
Performsにはプロセスが実行したイベント列が、Acceptsにはその時点で実行可能(ready)なイベントが表示されている。
今回の場合、Performsに表示されているように実行したとき次に実行可能なイベントがないことがわかる。
tauは内部イベントを表す。内部イベントとは外部のプロセスからは観測されない内部のイベントである。
今回は、VMBの内部選択|~| がtauにより行われていると見る。つまり、内部選択とはプロセス自身が内部イベントtauを起こし、実行するプロセスを選択しているのである。
SYSTEMの箇所をダブルクリックすることで、構成しているプロセスにも着目できる。
プロセスPERSONはイベントcoinを実行可能であるが、VMBの方が何も実行できなくなっていることがわかる。
結局、Performsのイベント列を考えると、残り本数が１本(n=1)のときに当たりが出ると、ジュースが２本出てしまい ｎ=-1 になり停止(STOP)してしまうようだ。
実際はこのような最後の１本の場合にどうなるのか気になるが、おそらく当たっても何も選べないまま時間切れで無効になっていたのでは・・。ある意味ちょっとした設計ミスか？
ここでは、n=1のときは絶対に当たらないようにしておけば、とりあえず良さそうである。
VMB(n) = if (n>1) then coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2) ) else if (n==1) then coin -> juice -> VMB(n-1) else if (n==0) then fill -> VMB(10) else STOP
ちなみに今回の例は、プロセス間の相互作用において特に問題があるというよりは、単にVMB自身の問題である。
