例題２
購入者、自動販売機をそれぞれ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} )
