Input/Output(入出力)
CSPではプロセス間の様々なデータの受け渡しをチャネルを用いたメッセージパッシング方式で行う。
channel ch:{0..7} -- チャネルchの型を{0,1,・・,6,7}とする。 P = ch!5 -> SKIP -- '!'は送信を意味する。 Q = ch?x -> SKIP -- '?'は受信を意味する。 SYSTEM = P[|{|ch|}|]Q -- {|ch|} = {ch.0,ch.1,・・ch.6,ch.7}
プロセスPはチャンネルchに５を出力するだけのプロセスである。また、このプロセスの起こすイベントはch.5である。
プロセスQはチャンネルchから値を変数x*1で受け取るだけのプロセスである。
SYSTEMはPとQがチャンネルchで同期する*2プロセスでありイベントch.5を起こした後、正常終了する。
これまで自販機の例では入金をイベントcoinで抽象化してきたが、もう少し詳しくチャネルinを通して小銭を入れることにすると
channel juice Coin = {10,50,100,500} --小銭は10円以上の４種類 channel in:Coin VM(n) = if n<120 then in?x -> VM(n+x) --入金 x を保持している金額に加算 else juice -> VM(n-120) --ジュース1本120円
自販機はチャネルinで受け取った値xを変数nに加算する。120円以上入金されるとジュースを出す。
PERSON = juice -> SKIP [] |~|i:Coin@ in!i -> PERSON {- 次のように書いても同じ。 PERSON = juice -> SKIP [] ( in!10 -> PERSON |~| in!50 -> PERSON |~| in!100 -> PERSON |~| in!500 -> PERSON ) -} SYSTEM = PERSON[|{|in,juice|}|]VM(0)
プロセスPERSONはjuiceボタンを押すか、小銭を適当に入れる。
PERSONとVMはチャネルin およびイベントjuice で同期しながら動作するので、結果的に120円以上になるまで小銭が入れられた後ジュースが出て終了する。なお、釣銭は出ないので注意。
例題１
昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう１本もらえるというものである。今回はそれを単純化しモデリングする。
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自身の問題である。
conditional choice(条件選択)
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(10)
n で残数を表わしているつもりであるが、このままでは、VMCNT(10),VMCNT(9), ･･ ,VMCNT(1),VMCNT(0),VMCNT(-1)・・・と変化してしまう。そこで、残数n によりプロセスを選択することにする。
VMCNT(n) = if (n>0) then --(n>0)の括弧は省略可 coin -> juice -> VMCNT(n-1) -- n>0 の場合は先と同じ else SKIP -- n<=0 の場合は終了
プロセスcoin->juice->VMCNT(n-1) と SKIP の選択が n の値により行われる。
VMCNT(10)は10回販売すると、VMCNT(0) = SKIP となる。
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を使って定義する方が計算量を減らすことができる。
interrupt(割り込み)
interrupt '/\' は P/\Q でプロセスPの実行中に Q が割り込む可能性を表す。プロセスP 実行中にプロセス Q のイベントが起こると Q に実行が移る。その後 P に実行は戻らない。
親子が自販機でジュースを買うときに、親がコインを入れボタンを押そうとすると急に子供がボタンを押したがったので子供に任すような場合を考えよう。
channel coin, coke, lemonade PARENT = coin -> lemonade -> SKIP CHILD = coke -> SKIP FAMILY = PARENT /\ CHILD VMS = coin -> ( coke -> VMS [] lemonade -> VMS ) SYSTEM = FAMILY [{coin,coke,lemonade}||{coin,coke,lemonade}] VMS
プロセスPARENT に対して CHILDが割り込むのは CHILDのイベントcoke が起きたときである。cokeはVMSと同期して起こるのでコインを入れるまで CHILD が割り込むことはない。SYSTEMは最初、かならず coinイベントが起きる。
coinイベントの後、親がレモネードを買うか、子供がコーラを欲しがり割り込むかは分からない。SYSTEM は両方の可能性を持ったプロセスとなる。
例題２
購入者、自動販売機をそれぞれCSPでモデリングし、正しく動作するシステムを検証しながら設計してみよう。まず、下記のような購入者3人と自動販売機をモデリングする。
購入者の動作はコインを入れ、ジュースのボタンを押す。
channel coin, juice PERSON = coin -> juice -> PERSON
プロセスPEOPLE は3人のPERSON から成り、個別に自販機でジュースを購入する。
PEOPLE = |||i:{1..3}@ PERSON -- = PERSON ||| PERSON ||| PERSON と同じ。
自動販売機はジュースの残数 m 、入れられたコインの枚数 n を保持する。ジュースが買えるのは m>0 かつ n>0 のときであり、コインをいれれるのは n<5 かつ m>0 のときとする
VM(m,n) = (n<5)and(m>0)&coin -> VM(m,n+1) [] (n>0)and(m>0)&juice -> VM(m-1,n-1)
自販機にジュースが5本残っている状態として、3人の購入者それぞれと自販機はイベントcoin,juice で同期する。
SYSTEM = PEOPLE[{coin,juice}||{coin,juice}]VM(5,0)
この SYSTEM は人々がジュースを買うごとに残数 m が減っていき、０になると自販機が juiceイベントを起こせなくなるので止まってしまう。
FDR2のデッドロックのデバック画面からもわかる。
プロセスSYSTEMはcoin,juiceを５回繰り返すとAcceptの欄が空になり、起こせるイベントがなくなっている。
そこで、ジュースを補充する業者(VENDOR)も考えることにする。
業者は自販機にジュースを補充(fill)する。いつ補充するかは決まっていないが、補充は自販機に入っているコインの枚数が０であることを確認してから行う。
channel fill VENDOR = fill -> VENDOR VM(m,n) = (n<5)and(m>0)&coin -> VM(m,n+1) [] (n>0)and(m>0)&juice -> VM(m-1,n-1) [] (n==0)&fill -> VM(10,0) --残数を10本にする。 SYSTEM = PEOPLE [{coin,juice}||{coin,juice}] ( VM(5,0) [{coin,juice,fill}||{fill}] VENDOR \ {fill} )
人々がジュースを買うごとに残数が減っていくが、たとえ０になっても業者がときどき補充してくれるので、今度は止まることなく動き続ける。だろうか？
FDR2で検証すると、まだデッドロックになるケースがあることがわかる。
デバック画面を見ると確かにプロセスVMの起こせるイベントがなくなっている。
原因は、プロセスPERSONがそれぞれ独立に動くので１人がコインを入れた後ジュースを買う前に別のもう１人がコインを入れることができる。
プロセスVMも連続してコインを入れることは可能としているが、ジュースの残数を超えてコインを入れてしまうと、残数が０(m=0)になったときにコインが残っており(n>0)、補充できなくなって止まってしまうのである。
そこで返却レバーを加えることにすると、止まることなく動作するシステムが設計できる。
channel coin, juice, fill, return PEOPLE = |||i:{1..3}@ PERSON PERSON = coin -> ( juice -> PERSON [] return -> PERSON ) --returnを入れる。 VM(m,n) = (n<5)and(m>0)&coin -> VM(m,n+1) [] (n>0)and(m>0)&juice -> VM(m-1,n-1) [] (n==0)&fill -> VM(10,0) [] return -> VM(m,0) --コインを0にする。 VENDOR = fill -> VENDOR SYSTEM = PEOPLE --アルファベットに注意。 [{coin,juice,return}||{coin,juice,return}] ( VM(5,0) [{coin,juice,fill,return}||{fill}] VENDOR \ {fill} )
